From 672d1347c2daeddb8c434ea996f95ba555d22589 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 26 Sep 2018 18:13:29 -0500
Subject: Makes SyGuS parsing more robust in invariant problems (#2509)

---
 test/regress/CMakeLists.txt                        |  1 +
 test/regress/Makefile.tests                        |  1 +
 .../regress0/sygus/inv-different-var-order.sy      | 22 ++++++++++++++++++++++
 3 files changed, 24 insertions(+)
 create mode 100644 test/regress/regress0/sygus/inv-different-var-order.sy

(limited to 'test')

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 35672d77a..5252954dc 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -826,6 +826,7 @@ set(regress_0_tests
   regress0/sygus/check-generic-red.sy
   regress0/sygus/const-var-test.sy
   regress0/sygus/dt-no-syntax.sy
+  regress0/sygus/inv-different-var-order.sy
   regress0/sygus/let-ringer.sy
   regress0/sygus/let-simp.sy
   regress0/sygus/no-syntax-test-bool.sy
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index c79f42078..08d0ca5bb 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -839,6 +839,7 @@ REG0_TESTS = \
 	regress0/sygus/const-var-test.sy \
 	regress0/sygus/dt-no-syntax.sy \
 	regress0/sygus/hd-05-d1-prog-nogrammar.sy \
+	regress0/sygus/inv-different-var-order.sy \
 	regress0/sygus/let-ringer.sy \
 	regress0/sygus/let-simp.sy \
 	regress0/sygus/no-syntax-test-bool.sy \
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
-- 
cgit v1.2.3