From 00b021654048aa26748c5ef45a39bcc29a0fa27b Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Wed, 14 Nov 2012 17:56:53 +0100
Subject: [PATCH] Testcase for integer equation. Doesn't work, for now.
---
testcases/synthesis/ChooseArith.scala | 6 ++++++
1 file changed, 6 insertions(+)
create mode 100644 testcases/synthesis/ChooseArith.scala
diff --git a/testcases/synthesis/ChooseArith.scala b/testcases/synthesis/ChooseArith.scala
new file mode 100644
index 000000000..b910cd4ea
--- /dev/null
+++ b/testcases/synthesis/ChooseArith.scala
@@ -0,0 +1,6 @@
+import leon.Utils._
+
+object ChooseArith {
+ def c1(a : Int) : (Int, Int) =
+ choose((x:Int,y:Int) => 2*x + 4*a == -y)
+}
--
GitLab