More refactoring of cbqi. Add a few regressions. Add option for qcf.

3 files changed, 39 insertions, 1 deletions

diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 6608ae22d..43c77973f 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -86,7 +86,9 @@ TESTS =	\
 	z3.620661-no-fv-trigger.smt2 \
 	bug_743.smt2 \
 	quaternion_ds1_symm_0428.fof.smt2 \
-	bug749-rounding.smt2
+	bug749-rounding.smt2 \
+	RNDPRE_4_1-dd-nqe.smt2 \
+	mix-complete-strat.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/RNDPRE_4_1-dd-nqe.smt2 b/test/regress/regress0/quantifiers/RNDPRE_4_1-dd-nqe.smt2
new file mode 100644
index 000000000..6379d6cec
--- /dev/null
+++ b/test/regress/regress0/quantifiers/RNDPRE_4_1-dd-nqe.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --cbqi-nested-qe
+; EXPECT: unsat
+(set-logic LRA)
+
+(declare-fun c () Real)
+
+(assert 
+(forall ((?x2 Real)) 
+(exists ((?x3 Real)) 
+(and
+(forall ((?x4 Real)) (or 
+(not (>= ?x4 4)) 
+(and (> c (+ ?x2 ?x3)) (> (+ c ?x3 ?x4) 0))) )
+(not (> (+ c ?x2 ?x3) 0)) )
+)) )
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/quantifiers/mix-complete-strat.smt2 b/test/regress/regress0/quantifiers/mix-complete-strat.smt2
new file mode 100644
index 000000000..c2209f697
--- /dev/null
+++ b/test/regress/regress0/quantifiers/mix-complete-strat.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic UFLIA)
+(set-info :status sat)
+
+(declare-sort U 0)
+(declare-fun P (U) Bool)
+
+(assert (forall ((x U)) (P x)))
+
+(declare-fun u () U)
+(assert (P u))
+
+(declare-const a Int)
+(declare-const b Int)
+(assert (forall ((x Int)) (or (> x a) (< x b))))
+
+(check-sat)