From c308c094548bcd9bee59e33334d147a9afe97018 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 14 May 2018 11:33:14 -0500
Subject: Add regressions, change defaults. (#1911)

---
 test/regress/Makefile.tests                     |  2 ++
 test/regress/regress1/sygus/large-const-simp.sy | 13 +++++++++++++
 test/regress/regress2/sygus/ex23.sy             | 23 +++++++++++++++++++++++
 3 files changed, 38 insertions(+)
 create mode 100644 test/regress/regress1/sygus/large-const-simp.sy
 create mode 100644 test/regress/regress2/sygus/ex23.sy

(limited to 'test')

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 5cb24d072..7784a6825 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1488,6 +1488,7 @@ REG1_TESTS = \
 	regress1/sygus/icfp_easy-ite.sy \
 	regress1/sygus/inv-example.sy \
 	regress1/sygus/inv-unused.sy \
+	regress1/sygus/large-const-simp.sy \
 	regress1/sygus/list-head-x.sy \
 	regress1/sygus/max.sy \
 	regress1/sygus/multi-fun-polynomial2.sy \
@@ -1589,6 +1590,7 @@ REG2_TESTS = \
 	regress2/strings/norn-dis-0707-3.smt2 \
 	regress2/sygus/MPwL_d1s3.sy \
 	regress2/sygus/array_sum_dd.sy \
+	regress2/sygus/ex23.sy \
 	regress2/sygus/icfp_easy_mt_ite.sy \
 	regress2/sygus/inv_gen_n_c11.sy \
 	regress2/sygus/lustre-real.sy \
diff --git a/test/regress/regress1/sygus/large-const-simp.sy b/test/regress/regress1/sygus/large-const-simp.sy
new file mode 100644
index 000000000..31f660b2a
--- /dev/null
+++ b/test/regress/regress1/sygus/large-const-simp.sy
@@ -0,0 +1,13 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status --sygus-add-const-grammar
+(set-logic LIA)
+
+(synth-fun lc ((x Int)) Int)
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (> (lc x) 1500))
+(constraint (< (lc x) 1600))
+
+(check-synth)
diff --git a/test/regress/regress2/sygus/ex23.sy b/test/regress/regress2/sygus/ex23.sy
new file mode 100644
index 000000000..61b08a838
--- /dev/null
+++ b/test/regress/regress2/sygus/ex23.sy
@@ -0,0 +1,23 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic LIA)
+
+(synth-inv inv-f ((y Int) (z Int) (c Int)))
+
+(declare-primed-var y Int)
+(declare-primed-var z Int)
+(declare-primed-var c Int)
+
+(define-fun pre-f ((y Int) (z Int) (c Int)) Bool
+(and (and (= c 0) (>= y 0)) (and (>= 127 y) (= z (* 36 y)))))
+
+
+(define-fun trans-f ((y Int) (z Int) (c Int) (y! Int) (z! Int) (c! Int)) Bool
+(and (and (and (< c 36) (= z! (+ z 1))) (= c! (+ c 1))) (= y! y)))
+
+(define-fun post-f ((y Int) (z Int) (c Int)) Bool
+(not (and (< c 36) (or (< z 0) (>= z 4608)))))
+
+(inv-constraint inv-f pre-f trans-f post-f)
+
+(check-synth)
-- 
cgit v1.2.3