Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullModel=false assigns values to eqc. Bug fix for fmf-fun. Minor change to resource limiting for quantifiers. Add fmf regressions.

1 files changed, 11 insertions, 0 deletions

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 078614509..cb969088d 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -127,6 +127,17 @@ Node InstMatch::get( int i ) {
   return d_vals[i];
 }
 
+void InstMatch::getTerms( QuantifiersEngine* qe, Node f, std::vector< Node >& inst ){
+  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+    Node val = get( i );
+    if( val.isNull() ){
+      Node ic =  qe->getTermDatabase()->getInstantiationConstant( f, i );
+      val = qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
+    }
+    inst.push_back( val );
+  }
+}
+
 void InstMatch::setValue( int i, TNode n ) {
   d_vals[i] = n;
 }