Minor updates/fix to --cbqi-recurse

4 files changed, 18 insertions, 11 deletions

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 3edf97467..e3514d949 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -38,9 +38,13 @@ d_qe( qe ), d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c
 }
 
 void FirstOrderModel::assertQuantifier( Node n ){
-  d_forall_asserts.push_back( n );
-  if( n.getAttribute(AxiomAttribute()) ){
-    d_axiom_asserted = true;
+  if( n.getKind()==FORALL ){
+    d_forall_asserts.push_back( n );
+    if( n.getAttribute(AxiomAttribute()) ){
+      d_axiom_asserted = true;
+    }
+  }else if( n.getKind()==NOT ){
+    Assert( n[0].getKind()==FORALL );
   }
 }
 
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 63df56392..5cf5a4c72 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -679,6 +679,9 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
                 if( d_qe->addInstantiation( f, inst ) ){
                   Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
                   d_addedLemmas++;
+                  if( options::fmfOneInstPerRound() ){
+                    break;
+                  }
                 }else{
                   Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl;
                   //this can happen if evaluation is unknown
@@ -796,6 +799,9 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
         if( d_qe->addInstantiation( f, inst ) ){
           Trace("fmc-exh-debug")  << " ...success.";
           addedLemmas++;
+          if( options::fmfOneInstPerRound() ){
+            break;
+          }
         }else{
           Trace("fmc-exh-debug") << ", failed.";
         }
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 123dc02b6..53c6d9e27 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -393,17 +393,15 @@ void InstantiationEngine::debugSat( int reason ){
         }
       }
     }
+    if( options::recurseCbqi() && !options::preSkolemQuant() && d_setIncomplete ){
+      Debug("quantifiers-sat") << "Cannot conclude SAT with nested quantifiers in recursive strategy." << std::endl;
+      //TODO : only when existentials with inst constants
+      d_quantEngine->getOutputChannel().setIncomplete();
+    }
     //}
     Debug("quantifiers-sat") << "return SAT: Cbqi, no quantifier is active. " << std::endl;
-    //static bool setTrust = false;
-    //if( !setTrust ){
-    //  setTrust = true;
-    //  Notice() << "trust-";
-    //}
   }else if( reason==SAT_INST_STRATEGY ){
     Debug("quantifiers-sat") << "return SAT: No strategy chose to add an instantiation." << std::endl;
-    //Notice() << "sat ";
-    //Unimplemented();
   }
 }
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a16f46ace..53163cd5f 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -266,7 +266,6 @@ void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
 }
 
 void QuantifiersEngine::assertNode( Node f ){
-  Assert( f.getKind()==FORALL );
   d_model->assertQuantifier( f );
   for( int i=0; i<(int)d_modules.size(); i++ ){
     d_modules[i]->assertNode( f );