Robust strategy for single invocation LIA synthesis conjectures. Add regressions.

1 files changed, 40 insertions, 0 deletions

diff --git a/test/regress/regress0/sygus/twolets1.sy b/test/regress/regress0/sygus/twolets1.sy
new file mode 100644
index 000000000..24b0f2c09
--- /dev/null
+++ b/test/regress/regress0/sygus/twolets1.sy
@@ -0,0 +1,40 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+(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)
+