1 files changed, 35 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/multi-fun-polynomial2.sy b/test/regress/regress1/sygus/multi-fun-polynomial2.sy
new file mode 100644
index 000000000..22a2e0a4b
--- /dev/null
+++ b/test/regress/regress1/sygus/multi-fun-polynomial2.sy
@@ -0,0 +1,35 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic LIA)
+
+(synth-fun addExpr1 ((x Int) (y Int)) Int
+    ((Start Int (x
+                 y
+     0
+     1
+                 (+ Start Start)
+                 (- Start Start)
+                 ))
+          ))
+
+(synth-fun addExpr2 ((x Int) (y Int)) Int
+    ((Start Int (x
+                 y
+     0
+     1
+                 (+ Start Start)
+                 (- Start Start)
+                 ))
+          ))
+
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (+ (addExpr1 x y) (addExpr2 y x)) (- x y)))
+
+
+(check-synth)
+
+; (x, y), (x-y, 0) ... are valid solutions