From e230f2b087e4c67a5ca2449890bd333f3c633dc8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Sat, 15 Dec 2012 15:59:59 +0100
Subject: [PATCH] testcase for finite sort, with 3 elements
---
testcases/synthesis/FiniteSort.scala | 18 ++++++++++++++++++
1 file changed, 18 insertions(+)
create mode 100644 testcases/synthesis/FiniteSort.scala
diff --git a/testcases/synthesis/FiniteSort.scala b/testcases/synthesis/FiniteSort.scala
new file mode 100644
index 000000000..249daa5b3
--- /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)
+ )
+ )
+ }
+
+}
--
GitLab