1 files changed, 33 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/max.sy b/test/regress/regress1/sygus/max.sy
new file mode 100644
index 000000000..37ed848ef
--- /dev/null
+++ b/test/regress/regress1/sygus/max.sy
@@ -0,0 +1,33 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+(set-logic LIA)
+
+(synth-fun max ((x Int) (y Int)) Int
+  ((Start Int (0 1 x y
+               (+ Start Start)
+               (- Start Start)
+               (ite StartBool Start Start)))
+   (StartBool Bool ((and StartBool StartBool)
+                    (not StartBool)
+                    (<= Start Start)))))
+
+;(synth-fun min ((x Int) (y Int)) Int
+;  ((Start Int ((Constant Int) (Variable Int)
+;               (+ Start Start)
+;               (- Start Start)
+;               (ite StartBool Start Start)))
+;   (StartBool Bool ((and StartBool StartBool)
+;                    (not StartBool)
+;                    (<= Start Start)))))
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (>= (max x y) x))
+(constraint (>= (max x y) y))
+(constraint (or (= x (max x y))
+                (= y (max x y))))
+;(constraint (= (+ (max x y) (min x y))
+;               (+ x y)))
+
+(check-synth)