Add missing regression.

1 files changed, 26 insertions, 0 deletions

diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy
new file mode 100644
index 000000000..0d753bdf1
--- /dev/null
+++ b/test/regress/regress0/sygus/const-var-test.sy
@@ -0,0 +1,26 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si
+
+(set-logic LIA)
+
+(synth-fun max2 ((x Int) (y Int)) Int
+    ((Start Int ((Variable Int)
+                 (Constant Int)
+                 (+ Start Start)
+                 (- Start Start)
+                 (ite StartBool Start Start)))
+     (StartBool Bool ((and StartBool StartBool)
+                      (or  StartBool StartBool)
+                      (not StartBool)
+                      (<=  Start Start)
+                      (=   Start Start)
+                      (>=  Start Start)))))
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (max2 x y) (+ x y 500)))
+
+
+(check-synth)
+