1 files changed, 26 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/incremental-modify-ex.sy b/test/regress/regress0/sygus/incremental-modify-ex.sy
new file mode 100644
index 000000000..f453964b0
--- /dev/null
+++ b/test/regress/regress0/sygus/incremental-modify-ex.sy
@@ -0,0 +1,26 @@
+; COMMAND-LINE: -i --sygus-out=status
+;EXPECT: unsat
+;EXPECT: unsat
+(set-logic LIA)
+
+(synth-fun f ((x Int) (y Int)) Int
+  ((Start Int) (StartBool Bool))
+  ((Start Int (0 1 x y
+               (+ 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)
+
+(push 1)
+(constraint (>= (f x y) 0))
+(check-synth)
+(pop 1)
+
+(constraint (< (f x y) 0))
+(check-synth)