From c308c094548bcd9bee59e33334d147a9afe97018 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 14 May 2018 11:33:14 -0500 Subject: Add regressions, change defaults. (#1911) --- test/regress/regress2/sygus/ex23.sy | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 test/regress/regress2/sygus/ex23.sy (limited to 'test/regress/regress2') 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) -- cgit v1.2.3