diff options
Diffstat (limited to 'test/regress/regress1/sygus/inv-example.sy')
-rw-r--r-- | test/regress/regress1/sygus/inv-example.sy | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/inv-example.sy b/test/regress/regress1/sygus/inv-example.sy new file mode 100644 index 000000000..ff68bc06c --- /dev/null +++ b/test/regress/regress1/sygus/inv-example.sy @@ -0,0 +1,12 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) +(synth-inv inv-f ((x Int) (y Int) (b Bool))) +(declare-primed-var x Int) +(declare-primed-var y Int) +(declare-primed-var b Bool) +(define-fun pre-f ((x Int) (y Int) (b Bool)) Bool (and (and (>= x 5) (<= x 9)) (and (>= y 1) (<= y 3)))) +(define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool (and (and (= b! b) (= y! x)) (ite b (= x! (+ x 10)) (= x! (+ x 12))))) +(define-fun post-f ((x Int) (y Int) (b Bool)) Bool (<= y x)) +(inv-constraint inv-f pre-f trans-f post-f) +(check-synth) |