1 files changed, 28 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/twolets2-orig.sy b/test/regress/regress1/sygus/twolets2-orig.sy
new file mode 100644
index 000000000..50f7ad544
--- /dev/null
+++ b/test/regress/regress1/sygus/twolets2-orig.sy
@@ -0,0 +1,28 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+(set-logic LIA)
+(synth-fun f1 ((x Int)) Int
+     (
+     (Start Int (
+            (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z))
+            )
+     )
+     (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+
+     )
+)
+(synth-fun f2 ((x Int)) Int
+     (
+     (Start Int (x
+            (let ((y Int Start) (z Int CInt)) (+ (+ y x) z))
+            )
+     )
+     (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+
+     )
+)
+(declare-var x1 Int)
+(declare-var x2 Int)
+(constraint (= (+ (f1 x1)(f2 x2)) (+ (+ x2 x2) (+ x1 8))))
+(check-synth)
+