fix quantifier non-bug

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 9aefda75af9a2df4f4fd573e682764339c5248ca..dcf60e8f1055e927f336771c0dd8eec4383d213b 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1095,7 +1095,7 @@ lbool Solver::search(int nof_conflicts)
                  (!order_heap.empty() || qhead < trail.size()) ) {
                 check_type = CHECK_WITH_THEORY;
                 continue;
-              } else if (!decisionEngineDone && recheck) {
+              } else if (recheck) {
                 // There some additional stuff added, so we go for another full-check
                 continue;
               } else {

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 11ff9ecadfbaccce9f2c6fef2d3838cd4a6c1244..c1476acb849332a0be8e2d1d8c29ac2bde388461 100644 (file)
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -183,6 +183,8 @@ void InstantiationEngine::check( Theory::Effort e ){
     // such that the counterexample literal is not in positive in d_counterexample_asserts
    // for( BoolMap::iterator i = d_forall_asserts.begin(); i != d_forall_asserts.end(); i++ ) {
     //  if( (*i).second ) {
+    Debug("quantifiers") << "quantifiers:  check:  asserted quantifiers size" 
+                         << getQuantifiersEngine()->getNumAssertedQuantifiers() << std::endl;
     for( int i=0; i<(int)getQuantifiersEngine()->getNumAssertedQuantifiers(); i++ ){
       Node n = getQuantifiersEngine()->getAssertedQuantifier( i );
       if( Options::current()->cbqi && hasAddedCbqiLemma( n ) ){

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index ff7648843c328113d99a27ffcb0ec3ff23dbc49e..2440a2e53ba1aedd1a27a53819e27e4b4bc6f171 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -265,6 +265,7 @@ class TheoryEngine {
     }
 
     void setIncomplete() throw(AssertionException) {
+      Trace("theory") << "TheoryEngine::setIncomplete()" << std::endl;
       d_engine->setIncomplete(d_theory);
     }
 

diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am
index 1cc6052271b1577dd362eb2f9d43dcca6a2808b3..70b47a3a948fa60d38e3aedcc6ebb772611e6d79 100644 (file)
--- a/test/regress/regress0/decision/Makefile.am
+++ b/test/regress/regress0/decision/Makefile.am
@@ -16,6 +16,8 @@ TESTS =       \
        bitvec0.delta01.smt \
        bitvec5.smt \
        quant-Arrays_Q1-noinfer.smt2 \
+       quant-ex1.smt2 \
+       quant-ex1.disable_miniscope.smt2 \
        quant-symmetric_unsat_7.smt2 \
        uflia-error0.smt2 \
        uflia-xs-09-16-3-4-1-5.smt \
@@ -24,7 +26,6 @@ TESTS =       \
 
 # Incorrect answers:
 #      aufbv-fuzz01.smt \
-#      quant-ex1.smt2 \
 #
 
 EXTRA_DIST = $(TESTS)

diff --git a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2 b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2
new file mode 100644 (file)
index 0000000..a8f4ff2
--- /dev/null
+++ b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2
@@ -0,0 +1,12 @@
+(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)
+(exit)

diff --git a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect
new file mode 100644 (file)
index 0000000..9d5c95c
--- /dev/null
+++ b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect
@@ -0,0 +1,3 @@
+% COMMAND-LINE: --decision=justification --disable-miniscope-quant-fv --disable-miniscope-quant
+% EXPECT: unknown (INCOMPLETE)
+% EXIT: 0

diff --git a/test/regress/regress0/decision/quant-ex1.smt2.expect b/test/regress/regress0/decision/quant-ex1.smt2.expect
index 66f5e51ba8972dcd81594c7ff0fa7c62dce88f3b..38a730c5756e70b306449ce80a7e00df96366764 100644 (file)
--- a/test/regress/regress0/decision/quant-ex1.smt2.expect
+++ b/test/regress/regress0/decision/quant-ex1.smt2.expect
@@ -1,3 +1,3 @@
-% COMMAND-LINE: --decision=justificationo
-% EXPECT: unknown (INCOMPLETE)
-% EXIT: 0
+% COMMAND-LINE: --decision=justification
+% EXPECT: sat
+% EXIT: 10