More complete guess instantiation strategy, cvc4 now typically times out instead of answering unknown for benchmarks with quantifiers. Modified regressions accordingly. Minor fix for QCF regarding variable ordering. Improved relevant domain computation. Minor optimization for --mbqi=fmc

8 files changed, 2 insertions, 34 deletions

diff --git a/test/regress/regress0/bug512.minimized.smt2 b/test/regress/regress0/bug512.minimized.smt2
index 0b19f26df..1a2aaf56f 100644
--- a/test/regress/regress0/bug512.minimized.smt2
+++ b/test/regress/regress0/bug512.minimized.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --tlimit-per 1000
 ; EXPECT: unknown
 (set-logic UF)
 (declare-sort T 0)
diff --git a/test/regress/regress0/bug519.smt2 b/test/regress/regress0/bug519.smt2
index 22fdff674..406cb0c1b 100644
--- a/test/regress/regress0/bug519.smt2
+++ b/test/regress/regress0/bug519.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -mi
+; COMMAND-LINE: -mi --tlimit-per 1000
 ; EXPECT: unknown
 ; EXPECT: unsat
 
diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am
index 366204191..90a18f0e2 100644
--- a/test/regress/regress0/decision/Makefile.am
+++ b/test/regress/regress0/decision/Makefile.am
@@ -25,7 +25,6 @@ TESTS =	\
 	bitvec5.smt \
 	quant-Arrays_Q1-noinfer.smt2 \
 	quant-ex1.smt2 \
-	quant-ex1.disable_miniscope.smt2 \
 	uflia-xs-09-16-3-4-1-5.delta03.smt \
 	aufbv-fuzz01.smt \
 	bug347.smt \
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 93d513d9f..c478248da 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -28,10 +28,8 @@ TESTS =	\
 	bug269.smt2 \
 	burns13.smt2 \
 	burns4.smt2 \
-	ex1.smt2 \
 	ex3.smt2 \
 	ex6.smt2 \
-	ex7.smt2 \
 	opisavailable-12.smt2 \
 	ricart-agrawala6.smt2 \
 	set8.smt2 \
diff --git a/test/regress/regress0/quantifiers/ex1.smt2 b/test/regress/regress0/quantifiers/ex1.smt2
deleted file mode 100644
index 20230a6fa..000000000
--- a/test/regress/regress0/quantifiers/ex1.smt2
+++ /dev/null
@@ -1,13 +0,0 @@
-(set-logic AUFLIRA)
-(set-info :smt-lib-version 2.0)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-sort U 0)
-(declare-fun a () U)
-(declare-fun b () U)
-(declare-fun f (U) U)
-(declare-fun p () Bool)
-(assert (and (= a b) (forall ((x U)) (=> (and (= (f x) a) (not (= (f x) b))) p))))
-(check-sat)
-(get-info :reason-unknown)
-(exit)
diff --git a/test/regress/regress0/quantifiers/ex1.smt2.expect b/test/regress/regress0/quantifiers/ex1.smt2.expect
deleted file mode 100644
index 2bd8349de..000000000
--- a/test/regress/regress0/quantifiers/ex1.smt2.expect
+++ /dev/null
@@ -1,2 +0,0 @@
-% EXPECT: unknown
-% EXPECT: (:reason-unknown incomplete)
diff --git a/test/regress/regress0/quantifiers/ex7.smt2 b/test/regress/regress0/quantifiers/ex7.smt2
deleted file mode 100644
index 11a83fdc4..000000000
--- a/test/regress/regress0/quantifiers/ex7.smt2
+++ /dev/null
@@ -1,13 +0,0 @@
-(set-logic AUFLIRA)
-(set-info :smt-lib-version 2.0)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-sort U 0)
-(declare-fun a () U)
-(declare-fun b () U)
-(declare-fun c () U)
-(declare-fun f (U) U)
-(assert (and (= a b) (forall ((x U)) (=> (or (= (f x) c) (= x a)) (= x b)))))
-(check-sat)
-(get-info :reason-unknown)
-(exit)
diff --git a/test/regress/regress0/quantifiers/ex7.smt2.expect b/test/regress/regress0/quantifiers/ex7.smt2.expect
deleted file mode 100644
index 2bd8349de..000000000
--- a/test/regress/regress0/quantifiers/ex7.smt2.expect
+++ /dev/null
@@ -1,2 +0,0 @@
-% EXPECT: unknown
-% EXPECT: (:reason-unknown incomplete)