diff --git a/testcases/synthesis/ChooseArith.scala b/testcases/synthesis/ChooseArith.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b910cd4ea699d51566f69f6b2aff3d43c6e6c2c8
--- /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)
+}