1 files changed, 40 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/twolets1.sy b/test/regress/regress1/sygus/twolets1.sy
new file mode 100644
index 000000000..06d2ecb71
--- /dev/null
+++ b/test/regress/regress1/sygus/twolets1.sy
@@ -0,0 +1,40 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+(set-logic LIA)
+
+;; f1 is x plus 2 ;; f2 is 2x plus 5
+
+(define-fun let0 ((x Int) (y Int) (z Int)) Int (+ (+ y x) z))
+
+(synth-fun f1 ((x Int)) Int
+     (
+     (Start Int (
+            (let0 Intx CInt CInt)
+            )
+     )
+     (Intx Int (x))
+     (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
+            (let0 Intx Start CInt)
+            )
+     )
+     (Intx Int (x))
+     (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+
+     )
+)
+
+
+(declare-var x Int)
+
+(constraint (= (+ (f1 x)(f2 x)) (+ (+ x x) (+ x 8))))
+(constraint (= (- (f2 x)(f1 x)) (+ x 2)))
+
+(check-synth)
+