From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 11 May 2015 09:53:07 +0000 (+0200)
Subject: Add missing regression.
X-Git-Tag: cvc5-1.0.0~6331
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=870b29b0cce85941ed72d7e0ca75b61b0cfcf711;p=cvc5.git

Add missing regression.
---

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)
+