diff --git a/testcases/synthesis/FiniteSort.scala b/testcases/synthesis/FiniteSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..249daa5b3248179de21b76cf503f12019a0f960a
--- /dev/null
+++ b/testcases/synthesis/FiniteSort.scala
@@ -0,0 +1,18 @@
+import leon.Utils._
+
+object FiniteSort {
+
+  def sort3(x1: Int, x2: Int, x3: Int): (Int, Int, Int) = {
+    choose((z1: Int, z2: Int, z3: Int) => 
+      z1 <= z2 && z2 <= z3 && (
+        (z1 == x1 && z2 == x2 && z3 == x3) ||
+        (z1 == x1 && z2 == x3 && z3 == x2) ||
+        (z1 == x2 && z2 == x1 && z3 == x3) ||
+        (z1 == x2 && z2 == x3 && z3 == x1) ||
+        (z1 == x3 && z2 == x1 && z3 == x2) ||
+        (z1 == x3 && z2 == x2 && z3 == x1)
+      )
+    )
+  }
+
+}