Add regressions, change defaults. (#1911)

1 files changed, 23 insertions, 0 deletions

diff --git a/test/regress/regress2/sygus/ex23.sy b/test/regress/regress2/sygus/ex23.sy
new file mode 100644
index 000000000..61b08a838
--- /dev/null
+++ b/test/regress/regress2/sygus/ex23.sy
@@ -0,0 +1,23 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic LIA)
+
+(synth-inv inv-f ((y Int) (z Int) (c Int)))
+
+(declare-primed-var y Int)
+(declare-primed-var z Int)
+(declare-primed-var c Int)
+
+(define-fun pre-f ((y Int) (z Int) (c Int)) Bool
+(and (and (= c 0) (>= y 0)) (and (>= 127 y) (= z (* 36 y)))))
+
+
+(define-fun trans-f ((y Int) (z Int) (c Int) (y! Int) (z! Int) (c! Int)) Bool
+(and (and (and (< c 36) (= z! (+ z 1))) (= c! (+ c 1))) (= y! y)))
+
+(define-fun post-f ((y Int) (z Int) (c Int)) Bool
+(not (and (< c 36) (or (< z 0) (>= z 4608)))))
+
+(inv-constraint inv-f pre-f trans-f post-f)
+
+(check-synth)