Handle fmf.card as input from user, add support in SMT2 parser, as requested by Martin Brain. Fix two minor bugs : E-matching with datatypes, instantiation caching with incremental.

1 files changed, 11 insertions, 8 deletions

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 738cfed60..8b62fc39b 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -83,14 +83,17 @@ void ModelEngine::check( Theory::Effort e ){
           Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
           //let the strong solver verify that the model is minimal
           //for debugging, this will if there are terms in the model that the strong solver was not notified of
-          ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm );
-          Trace("model-engine-debug") << "Check model..." << std::endl;
-          d_incomplete_check = false;
-          //print debug
-          Debug("fmf-model-complete") << std::endl;
-          debugPrint("fmf-model-complete");
-          //successfully built an acceptable model, now check it
-          addedLemmas += checkModel();
+          if( ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm ) ){
+            Trace("model-engine-debug") << "Check model..." << std::endl;
+            d_incomplete_check = false;
+            //print debug
+            Debug("fmf-model-complete") << std::endl;
+            debugPrint("fmf-model-complete");
+            //successfully built an acceptable model, now check it
+            addedLemmas += checkModel();
+          }else{
+            addedLemmas++;
+          }
         }
       }
       if( addedLemmas==0 ){