diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-28 11:42:49 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-09-28 11:42:49 -0500 |
commit | 676fbb54488a995818773f05a6ce860916ee6667 (patch) | |
tree | 4a0d335b8438c593306da49cd930e95330ddc625 /test/regress/regress0/sygus | |
parent | 37f8a0a52fac6933af7bace33d8da648901a7bf9 (diff) | |
parent | 8c9e1ce5939737bac95cf16f59e6fc7fc856940b (diff) |
Merge branch 'master' into emptyEqemptyEq
Diffstat (limited to 'test/regress/regress0/sygus')
-rw-r--r-- | test/regress/regress0/sygus/inv-different-var-order.sy | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/inv-different-var-order.sy b/test/regress/regress0/sygus/inv-different-var-order.sy new file mode 100644 index 000000000..c3f43fc07 --- /dev/null +++ b/test/regress/regress0/sygus/inv-different-var-order.sy @@ -0,0 +1,22 @@ +; COMMAND-LINE: --sygus-out=status +;EXPECT: unsat +(set-logic LIA) +(synth-inv inv-f ((x Int) (y Int) (b Bool))) +(declare-primed-var b Bool) +(declare-primed-var x Int) +(declare-primed-var y Int) +(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 true) +(inv-constraint inv-f pre-f trans-f post-f) +(check-synth)
\ No newline at end of file |