1 files changed, 27 insertions, 0 deletions
diff --git a/test/regress/regress2/sygus/mpg_guard1-dd.sy b/test/regress/regress2/sygus/mpg_guard1-dd.sy
new file mode 100644
index 000000000..31800a36f
--- /dev/null
+++ b/test/regress/regress2/sygus/mpg_guard1-dd.sy
@@ -0,0 +1,27 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic LIA)
+
+(synth-fun eq1 ( (x Int) (y Int) ) Int
+    ((Start Int (x
+                 y
+                 0
+                 (+ Start Start)
+                 (- Start Start)
+                 (ite StartBool Start Start)))
+     (StartBool Bool ((and StartBool StartBool)
+                      (<=  Start Start)
+                      (=   Start Start)))))
+
+(define-fun iteB (( b1 Bool ) (b2 Bool ) (b3 Bool )) Bool (or (and b1 b2) (and (not b1) b3)))
+
+(declare-var x Int) 
+(declare-var y Int) 
+
+(constraint (iteB (>= x 0) 
+                  (= (eq1 x y) (+ x x))
+		              (= (eq1 x y) x)
+))
+
+(check-synth)
+