2 files changed, 22 insertions, 9 deletions
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 7ce299864..1543b2ebd 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -717,14 +717,10 @@ void CegInstantiator::processAssertions() {
   std::map< Node, Node > aux_subs;
 
   //for each variable
-  std::vector< TheoryId > tids;
-  tids.push_back(THEORY_UF);
   for( unsigned i=0; i<d_vars.size(); i++ ){
     Node pv = d_vars[i];
     TypeNode pvtn = pv.getType();
-    //collect relevant theories
-    std::map< TypeNode, bool > visited;
-    collectTheoryIds( pvtn, visited, tids );
+    Trace("cbqi-proc-debug") << "Collect theory ids from type " << pvtn << " of " << pv << std::endl;
     //collect information about eqc
     if( ee->hasTerm( pv ) ){
       Node pvr = ee->getRepresentative( pv );
@@ -739,8 +735,8 @@ void CegInstantiator::processAssertions() {
     }
   }
   //collect assertions for relevant theories
-  for( unsigned i=0; i<tids.size(); i++ ){
-    TheoryId tid = tids[i];
+  for( unsigned i=0; i<d_tids.size(); i++ ){
+    TheoryId tid = d_tids[i];
     Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid );
     if( theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid) ){
       Trace("cbqi-proc") << "Collect assertions from theory " << tid << std::endl;
@@ -781,7 +777,7 @@ void CegInstantiator::processAssertions() {
     TypeNode rtn = r.getType();
     TheoryId tid = Theory::theoryOf( rtn );
     //if we care about the theory of this eqc
-    if( std::find( tids.begin(), tids.end(), tid )!=tids.end() ){
+    if( std::find( d_tids.begin(), d_tids.end(), tid )!=d_tids.end() ){
       if( rtn.isInteger() || rtn.isReal() ){
         rtn = rtn.getBaseType();
       }
@@ -810,7 +806,7 @@ void CegInstantiator::processAssertions() {
     if( it!=aux_subs.end() ){
       addToAuxVarSubstitution( subs_lhs, subs_rhs, r, it->second );
     }else{
-      Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << r << "!!!" << std::endl;
+      Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << r << "!!! type is " << r.getType() << std::endl;
       Assert( false );
     }
   }
@@ -997,6 +993,21 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
   for( unsigned i=0; i<lems.size(); i++ ){
     collectCeAtoms( lems[i], visited );
   }
+
+  //compute the theory ids
+  d_tids.clear();
+  d_tids.push_back(THEORY_UF);
+  for( unsigned r=0; r<2; r++ ){
+    unsigned sz = r==0 ? d_vars.size() : d_aux_vars.size();
+    for( unsigned i=0; i<sz; i++ ){
+      Node pv = r==0 ? d_vars[i] : d_aux_vars[i];
+      TypeNode pvtn = pv.getType();
+      Trace("cbqi-proc-debug") << "Collect theory ids from type " << pvtn << " of " << pv << std::endl;
+      //collect relevant theories
+      std::map< TypeNode, bool > visited;
+      collectTheoryIds( pvtn, visited, d_tids );
+    }
+  }
 }
 
 
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h
index 94d02de9b..f9a711704 100644
--- a/src/theory/quantifiers/ceg_instantiator.h
+++ b/src/theory/quantifiers/ceg_instantiator.h
@@ -93,6 +93,8 @@ private:
   std::map< TypeNode, std::vector< Node > > d_curr_type_eqc;
   //auxiliary variables
   std::vector< Node > d_aux_vars;
+  // relevant theory ids
+  std::vector< TheoryId > d_tids;
   //literals to equalities for aux vars
   std::map< Node, std::map< Node, Node > > d_aux_eq;
   //the CE variables