Merge branch 'master' into emptyEqemptyEq

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