Avoid naming conflicts in sygus, refactor. Add missing regression. Detect Start grammar. Add regression.

3 files changed, 24 insertions, 1 deletions

diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index 50f755fef..dbef0494a 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -37,7 +37,8 @@ TESTS = commutative.sy \
         let-ringer.sy \
         let-simp.sy \
         tl-type.sy \
-        dup-op.sy
+        dup-op.sy \
+        nflat-fwd.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress0/sygus/dup-op.sy b/test/regress/regress0/sygus/dup-op.sy
new file mode 100644
index 000000000..dbf415986
--- /dev/null
+++ b/test/regress/regress0/sygus/dup-op.sy
@@ -0,0 +1,11 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi --no-cegqi-si
+(set-logic LIA)
+(synth-fun f ((x Int)) Int
+    ((Start Int ((+ Con Con) (+ Start Start) x))
+     (Con Int (0 1))))
+
+(declare-var x Int)
+(constraint (= (f x) (* 2 x)))
+(check-synth)
+
diff --git a/test/regress/regress0/sygus/nflat-fwd.sy b/test/regress/regress0/sygus/nflat-fwd.sy
new file mode 100644
index 000000000..0f9d46215
--- /dev/null
+++ b/test/regress/regress0/sygus/nflat-fwd.sy
@@ -0,0 +1,11 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi
+(set-logic LIA)
+(synth-fun f ((x Int)) Int
+    ((Start Int ((+ Con Con) (+ (+ Start Start) Con) x))
+     (Con Int (0 1))))
+
+(declare-var x Int)
+(constraint (= (f x) (* 2 x)))
+(check-synth)
+