From db83224b35a218a0bb449850530f0d2bea484eae Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 19 Mar 2018 23:16:45 -0500
Subject: Enable CEGQI for non-linear (#1674)

---
 test/regress/regress0/quantifiers/Makefile.am       | 4 +++-
 test/regress/regress0/quantifiers/cegqi-nl-simp.cvc | 2 ++
 test/regress/regress0/quantifiers/cegqi-nl-sq.smt2  | 5 +++++
 3 files changed, 10 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/quantifiers/cegqi-nl-simp.cvc
 create mode 100644 test/regress/regress0/quantifiers/cegqi-nl-sq.smt2

(limited to 'test/regress/regress0/quantifiers')

diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 1711c301e..809297863 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -71,7 +71,9 @@ TESTS =	\
 	qbv-test-invert-concat-1.smt2 \
 	qbv-test-invert-sign-extend.smt2 \
 	clock-10.smt2 \
-	lra-triv-gn.smt2
+	lra-triv-gn.smt2 \
+	cegqi-nl-simp.cvc \
+	cegqi-nl-sq.smt2
 
 EXTRA_DIST = $(TESTS) \
 	bug291.smt2.expect
diff --git a/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc
new file mode 100644
index 000000000..63cf52fd6
--- /dev/null
+++ b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc
@@ -0,0 +1,2 @@
+% EXPECT: valid
+QUERY FORALL (x:INT) : EXISTS (y:INT) : (x*y=x) ;
diff --git a/test/regress/regress0/quantifiers/cegqi-nl-sq.smt2 b/test/regress/regress0/quantifiers/cegqi-nl-sq.smt2
new file mode 100644
index 000000000..703f816d5
--- /dev/null
+++ b/test/regress/regress0/quantifiers/cegqi-nl-sq.smt2
@@ -0,0 +1,5 @@
+(set-logic NIA)
+(set-info :status unsat)
+(assert (not (exists ((?X Int)) (= (* ?X ?X) ?X))))
+(check-sat)
+(exit)
-- 
cgit v1.2.3