fix quantifier non-bug

3 files changed, 4 insertions, 1 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 9aefda75a..dcf60e8f1 100644
--- 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 11ff9ecad..c1476acb8 100644
--- 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 ff7648843..2440a2e53 100644
--- 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);
     }