1 files changed, 21 insertions, 6 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index c04920ab8..08bdd496b 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -35,9 +35,10 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::inst;
 
-QuantifiersEngine::QuantifiersEngine(context::Context* c, TheoryEngine* te):
+QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
 d_te( te ),
-d_quant_rel( false ){ //currently do not care about relevance
+d_quant_rel( false ),
+d_lemmas_produced_c(u){
   d_eq_query = new EqualityQueryQuantifiersEngine( this );
   d_term_db = new quantifiers::TermDb( this );
   d_tr_trie = new inst::TriggerTrie;
@@ -92,6 +93,10 @@ context::Context* QuantifiersEngine::getSatContext(){
   return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext();
 }
 
+context::Context* QuantifiersEngine::getUserContext(){
+  return d_te->theoryOf( THEORY_QUANTIFIERS )->getUserContext();
+}
+
 OutputChannel& QuantifiersEngine::getOutputChannel(){
   return d_te->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel();
 }
@@ -309,7 +314,7 @@ Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){
 
 bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
   if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
-    if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, modInst ) ){
+    if( d_inst_match_trie[f]->existsInstMatch( this, f, m, modEq, modInst ) ){
       return true;
     }
   }
@@ -323,9 +328,9 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b
 bool QuantifiersEngine::addLemma( Node lem ){
   Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl;
   lem = Rewriter::rewrite(lem);
-  if( d_lemmas_produced.find( lem )==d_lemmas_produced.end() ){
+  if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
     //d_curr_out->lemma( lem );
-    d_lemmas_produced[ lem ] = true;
+    d_lemmas_produced_c[ lem ] = true;
     d_lemmas_waiting.push_back( lem );
     Debug("inst-engine-debug") << "Added lemma : " << lem << std::endl;
     return true;
@@ -355,11 +360,21 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool
     }
   }
   //check for duplication modulo equality
-  if( !d_inst_match_trie[f].addInstMatch( this, f, m, modEq, modInst ) ){
+  inst::CDInstMatchTrie* imt;
+  std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_inst_match_trie.find( f );
+  if( it!=d_inst_match_trie.end() ){
+    imt = it->second;
+  }else{
+    imt = new CDInstMatchTrie( getUserContext() );
+    d_inst_match_trie[f] = imt;
+  }
+  Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
+  if( !imt->addInstMatch( this, f, m, getUserContext(), modEq, modInst ) ){
     Trace("inst-add-debug") << " -> Already exists." << std::endl;
     ++(d_statistics.d_inst_duplicate);
     return false;
   }
+  Trace("inst-add-debug") << "compute terms" << std::endl;
   //compute the vector of terms for the instantiation
   std::vector< Node > terms;
   for( size_t i=0; i<d_term_db->d_inst_constants[f].size(); i++ ){