Compute model basis only for fmf. Add another co-datatype regression.

2 files changed, 7 insertions, 3 deletions

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 5dc8bb384..a95de086a 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -398,9 +398,11 @@ void TermDb::reset( Theory::Effort effort ){
     if( !it->second.empty() ){
       for( unsigned i=0; i<it->second.size(); i++ ){
         Node n = it->second[i];
-        computeModelBasisArgAttribute( n );
         if( hasTermCurrent( n ) ){
           if( !n.getAttribute(NoMatchAttribute()) ){
+            if( options::finiteModelFind() ){
+              computeModelBasisArgAttribute( n );
+            }
             computeArgReps( n );
             if( !d_func_map_trie[ it->first ].addTerm( n, d_arg_reps[n] ) ){
               NoMatchAttribute nma;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index c10992435..899d035ea 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -295,13 +295,15 @@ void QuantifiersEngine::check( Theory::Effort e ){
       return;
     }
 
+    Trace("quant-engine-debug2") << "Reset term db..." << std::endl;
     d_term_db->reset( e );
     d_eq_query->reset();
     if( d_rel_dom ){
       d_rel_dom->reset();
     }
     d_model->reset_round();
-    for( int i=0; i<(int)d_modules.size(); i++ ){
+    for( unsigned i=0; i<d_modules.size(); i++ ){
+      Trace("quant-engine-debug2") << "Reset " << d_modules[i]->identify().c_str() << std::endl;
       d_modules[i]->reset_round( e );
     }
     Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
@@ -333,7 +335,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
       }
       if( success ){
         //check each module
-        for( int i=0; i<(int)qm.size(); i++ ){
+        for( unsigned i=0; i<qm.size(); i++ ){
           Trace("quant-engine-debug") << "Check " << qm[i]->identify().c_str() << " at effort " << quant_e << "..." << std::endl;
           qm[i]->check( e, quant_e );
         }