diff options
Diffstat (limited to 'test/regress/regress0/sygus/inv-unused.sy')
| -rw-r--r-- | test/regress/regress0/sygus/inv-unused.sy | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/inv-unused.sy b/test/regress/regress0/sygus/inv-unused.sy new file mode 100644 index 000000000..91ba95d39 --- /dev/null +++ b/test/regress/regress0/sygus/inv-unused.sy @@ -0,0 +1,13 @@ +; 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 (>= x 5) (<= x 9))) +(define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool (= x! (+ x 1))) +(define-fun post-f ((x Int) (y Int) (b Bool)) Bool (> x 0)) +(inv-constraint inv-f pre-f trans-f post-f) +; invariant does not depend on arguments y and b +(check-synth) |