More preparation for CASC proofs. Minor fix for sort inference (rewrite new assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.

14 files changed, 83 insertions, 59 deletions

diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index c6a5f4227..e86a96a8f 100755
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -73,20 +73,20 @@ void AbsDef::construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps
   }

 }

 

-void AbsDef::simplify( FirstOrderModelAbs * m, TNode n, unsigned depth ) {

+void AbsDef::simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth ) {

   if( d_value==val_none && !d_def.empty() ){

     //process the default

     std::map< unsigned, AbsDef >::iterator defd = d_def.find( d_default );

     Assert( defd!=d_def.end() );

     unsigned newDef = d_default;

     std::vector< unsigned > to_erase;

-    defd->second.simplify( m, n, depth+1 );

+    defd->second.simplify( m, q, n, depth+1 );

     int defVal = defd->second.d_value;

     bool isConstant = ( defVal!=val_none );

     //process each child

     for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){

       if( it->first!=d_default ){

-        it->second.simplify( m, n, depth+1 );

+        it->second.simplify( m, q, n, depth+1 );

         if( it->second.d_value==defVal && it->second.d_value!=val_none ){

           newDef = newDef | it->first;

           to_erase.push_back( it->first );

@@ -101,7 +101,7 @@ void AbsDef::simplify( FirstOrderModelAbs * m, TNode n, unsigned depth ) {
       d_def.erase( d_default );

       //set new default

       d_default = newDef;

-      d_def[d_default].construct_def_entry( m, n, defVal, depth+1 );

+      d_def[d_default].construct_def_entry( m, q, n, defVal, depth+1 );

       //erase redundant entries

       for( unsigned i=0; i<to_erase.size(); i++ ){

         d_def.erase( to_erase[i] );

@@ -120,6 +120,11 @@ void AbsDef::debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const{
   for( unsigned i=0; i<dSize; i++ ){

     Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0");

   }

+  //Trace(c) << "(";

+  //for( unsigned i=0; i<32; i++ ){

+  //  Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0");

+  //}

+  //Trace(c) << ")";

 }

 

 void AbsDef::debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth ) const{

@@ -257,11 +262,12 @@ void AbsDef::construct_normalize( FirstOrderModelAbs * m, TNode q, std::vector<
   }

 }

 

-void AbsDef::construct_def_entry( FirstOrderModelAbs * m, TNode n, int v, unsigned depth ) {

+void AbsDef::construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth ) {

   d_value = v;

   if( depth<n.getNumChildren() ){

-    unsigned dom = m->d_domain[n[depth].getType()];

-    d_def[dom].construct_def_entry( m, n, v, depth+1 );

+    TypeNode tn = q.isNull() ? n[depth].getType() : m->getVariable( q, depth ).getType();

+    unsigned dom = m->d_domain[tn] ;

+    d_def[dom].construct_def_entry( m, q, n, v, depth+1 );

     d_default = dom;

   }

 }

@@ -556,7 +562,7 @@ bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,
       for( std::map< unsigned, int >::iterator it = bchildren.begin(); it !=bchildren.end(); ++it ){

         if( ( it->second==0 && n.getKind()==AND ) ||

             ( it->second==1 && n.getKind()==OR ) ){

-          construct_def_entry( m, q[0], it->second );

+          construct_def_entry( m, q, q[0], it->second );

           return true;

         }

       }

@@ -654,11 +660,11 @@ bool AbsDef::isSimple( unsigned n ) {
   return (n & (n - 1))==0;

 }

 

-unsigned AbsDef::getId( unsigned n, unsigned start ) {

+unsigned AbsDef::getId( unsigned n, unsigned start, unsigned end ) {

   Assert( n!=0 );

   while( (n & ( 1 << start )) == 0 ){

     start++;

-    if( start==32 ){

+    if( start==end ){

       return start;

     }

   }

@@ -808,7 +814,7 @@ void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) {
         Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl;

         it->second->debugPrint("ambqi-model-debug", fm, fapps[0] );

         Trace("ambqi-model-debug") << "Simplifying " << f << "..." << std::endl;

-        it->second->simplify( fm, fapps[0] );

+        it->second->simplify( fm, TNode::null(), fapps[0] );

         Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl;

         it->second->debugPrint("ambqi-model", fm, fapps[0] );

 

@@ -831,7 +837,7 @@ void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) {
 

 //do exhaustive instantiation

 bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {

-  Trace("ambqi-check") << "exhaustive instantiation " << q << " " << effort << std::endl;

+  Trace("ambqi-check") << "Exhaustive instantiation " << q << " " << effort << std::endl;

   if (effort==0) {

     FirstOrderModelAbs * fma = fm->asFirstOrderModelAbs();

     bool quantValid = true;

@@ -843,6 +849,7 @@ bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, in
       }

     }

     if( quantValid ){

+      Trace("ambqi-check") << "Compute interpretation..." << std::endl;

       AbsDef ad;

       doCheck( fma, q, ad, q[1] );

       //now process entries

@@ -850,6 +857,7 @@ bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, in
       Trace("ambqi-inst") << "Interpretation of " << q << " is : " << std::endl;

       ad.debugPrint( "ambqi-inst", fma, q[0] );

       Trace("ambqi-inst") << std::endl;

+      Trace("ambqi-check") << "Add instantiations..." << std::endl;

       int lem = 0;

       quantValid = ad.addInstantiations( fma, d_qe, q, lem );

       Trace("ambqi-inst") << "...Added " << lem << " lemmas." << std::endl;

@@ -919,7 +927,7 @@ bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNod
     }

     Trace("ambqi-check-try") << "Interpretation for " << n << " is : " << std::endl;

     ad.debugPrint("ambqi-check-try", m, q[0] );

-    ad.simplify( m, q[0] );

+    ad.simplify( m, q, q[0] );

     Trace("ambqi-check-debug") << "(Simplified) Interpretation for " << n << " is : " << std::endl;

     ad.debugPrint("ambqi-check-debug", m, q[0] );

     Trace("ambqi-check-debug") << std::endl;

diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h
index 784fa5093..349073cb4 100755
--- a/src/theory/quantifiers/ambqi_builder.h
+++ b/src/theory/quantifiers/ambqi_builder.h
@@ -36,7 +36,7 @@ private:
                           std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,

                           std::vector< unsigned >& entry, std::vector< bool >& entry_def );

   void construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth = 0 );

-  void construct_def_entry( FirstOrderModelAbs * m, TNode n, int v, unsigned depth = 0 );

+  void construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth = 0 );

   void apply_ucompose( FirstOrderModelAbs * m, TNode q,

                        std::vector< unsigned >& entry, std::vector< bool >& entry_def, std::vector< int >& terms,

                        std::map< unsigned, int >& vchildren, AbsDef * a, unsigned depth = 0 );

@@ -59,7 +59,7 @@ public:
   void construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth = 0 );

   void debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const;

   void debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth = 0 ) const;

-  void simplify( FirstOrderModelAbs * m, TNode q, unsigned depth = 0 );

+  void simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth = 0 );

   int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, int& inst ){

     std::vector< Node > terms;

     terms.resize( q[0].getNumChildren() );

@@ -73,7 +73,7 @@ public:
   void negate();

   Node getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth = 0 );

   static bool isSimple( unsigned n );

-  static unsigned getId( unsigned n, unsigned start=0 );

+  static unsigned getId( unsigned n, unsigned start=0, unsigned end=32 );

   Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< Node >& args );

   Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< unsigned >& iargs, unsigned depth = 0 );

   //for debugging

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index e4b588ac1..3edf97467 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -102,7 +102,8 @@ Node FirstOrderModel::getSomeDomainElement(TypeNode tn){
   if (!d_rep_set.hasType(tn)) {
     Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;
     Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);
-    d_rep_set.add(mbt);
+    Trace("fmc-model-debug") << "Add to representative set..." << std::endl;
+    d_rep_set.add(tn, mbt);
   }else if( d_rep_set.d_type_reps[tn].size()==0 ){
     Message() << "empty reps" << std::endl;
     exit(0);
@@ -986,7 +987,7 @@ void FirstOrderModelAbs::collectEqVars( TNode q, TNode n, std::map< int, bool >&
   for( unsigned i=0; i<n.getNumChildren(); i++ ){
     if( n.getKind()==EQUAL && n[i].getKind()==BOUND_VARIABLE ){
       int v = getVariableId( q, n[i] );
-      Assert( v>=0 && v<q.getNumChildren() );
+      Assert( v>=0 && v<(int)q[0].getNumChildren() );
       eq_vars[v] = true;
     }
     collectEqVars( q, n[i], eq_vars );
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 0f3e53827..63df56392 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -61,7 +61,7 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {
         return true;
       }
     }
-    if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !c[index].getType().isInteger() ){
+    if( c[index].getType().isSort() ){
       //for star: check if all children are defined and have generalizations
       if( c[index]==st ){     ///options::fmfFmcCoverSimplify()
         //check if all children exist and are complete
@@ -537,7 +537,9 @@ void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){
     }else{
       mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn);
     }
+    Trace("fmc") << "Get used rep for " << mbn << std::endl;
     Node mbnr = fm->getUsedRepresentative( mbn );
+    Trace("fmc") << "...got  " << mbnr << std::endl;
     fm->d_model_basis_rep[tn] = mbnr;
     Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl;
   }
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 096d0cab2..703a44d03 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -198,18 +198,18 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No
   }
 }
 
-void InstMatchTrie::print( const char * c, Node q, std::vector< Node >& terms ) const {
+void InstMatchTrie::print( std::ostream& out, Node q, std::vector< Node >& terms ) const {
   if( terms.size()==q[0].getNumChildren() ){
-    Trace(c) << "  ( ";
+    out << "  ( ";
     for( unsigned i=0; i<terms.size(); i++ ){
-      if( i>0 ) Trace(c) << ", ";
-      Trace(c) << terms[i];
+      if( i>0 ) out << ", ";
+      //out << terms[i];
     }
-    Trace(c) << " )" << std::endl;
+    out << " )" << std::endl;
   }else{
     for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
       terms.push_back( it->first );
-      it->second.print( c, q, terms );
+      it->second.print( out, q, terms );
       terms.pop_back();
     }
   }
@@ -282,19 +282,19 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector<
   }
 }
 
-void CDInstMatchTrie::print( const char * c, Node q, std::vector< Node >& terms ) const{
+void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< Node >& terms ) const{
   if( d_valid.get() ){
     if( terms.size()==q[0].getNumChildren() ){
-      Trace(c) << "  ( ";
+      out << "  ( ";
       for( unsigned i=0; i<terms.size(); i++ ){
-        if( i>0 ) Trace(c) << ", ";
-        Trace(c) << terms[i];
+        if( i>0 ) out << ", ";
+        //out << terms[i];
       }
-      Trace(c) << " )" << std::endl;
+      out << " )" << std::endl;
     }else{
       for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
         terms.push_back( it->first );
-        it->second->print( c, q, terms );
+        it->second->print( out, q, terms );
         terms.pop_back();
       }
     }
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 2cf63210b..accd3baed 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -101,7 +101,7 @@ public:
   /** the data */
   std::map< Node, InstMatchTrie > d_data;
 private:
-  void print( const char * c, Node q, std::vector< Node >& terms ) const;
+  void print( std::ostream& out, Node q, std::vector< Node >& terms ) const;
 public:
   InstMatchTrie(){}
   ~InstMatchTrie(){}
@@ -128,9 +128,9 @@ public:
   }
   bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
                      bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
-  void print( const char * c, Node q ) const{
+  void print( std::ostream& out, Node q ) const{
     std::vector< Node > terms;
-    print( c, q, terms );
+    print( out, q, terms );
   }
 };/* class InstMatchTrie */
 
@@ -142,7 +142,7 @@ public:
   /** is valid */
   context::CDO< bool > d_valid;
 private:
-  void print( const char * c, Node q, std::vector< Node >& terms ) const;
+  void print( std::ostream& out, Node q, std::vector< Node >& terms ) const;
 public:
   CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
   ~CDInstMatchTrie(){}
@@ -169,9 +169,9 @@ public:
   }
   bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false,
                      bool modInst = false, int index = 0, bool onlyExist = false );
-  void print( const char * c, Node q ) const{
+  void print( std::ostream& out, Node q ) const{
     std::vector< Node > terms;
-    print( c, q, terms );
+    print( out, q, terms );
   }
 };/* class CDInstMatchTrie */
 
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 06858cf92..123dc02b6 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -210,7 +210,7 @@ void InstantiationEngine::check( Theory::Effort e ){
     }
     ++(d_statistics.d_instantiation_rounds);
     bool quantActive = false;
-    Debug("quantifiers") << "quantifiers:  check:  asserted quantifiers size"
+    Debug("quantifiers") << "quantifiers:  check:  asserted quantifiers size="
                          << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl;
     for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 8fecc6ee0..a16f46ace 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -623,18 +623,20 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
   }
 }
 
-void QuantifiersEngine::printInstantiations( const char * c ) {
-  if( options::incrementalSolving() ){
-    for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
-      Trace(c) << "Instantiations of " << it->first << " : " << std::endl;
-      it->second->print( c, it->first );
-    }
-  }else{
+void QuantifiersEngine::printInstantiations( std::ostream& out ) {
+  //Trace("ajr-temp") << "QE print inst." << std::endl;
+  //if( options::incrementalSolving() ){
+  //  for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
+  //    out << "Instantiations of " << it->first << " : " << std::endl;
+  //    it->second->print( out, it->first );
+  //  }
+  //}else{
     for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
-      Trace(c) << "Instantiations of " << it->first << " : " << std::endl;
-      it->second.print( c, it->first );
+      out << "Instantiations of " << it->first << " : " << std::endl;
+      it->second.print( out, it->first );
+      out << std::endl;
     }
-  }
+  //}
 }
 
 QuantifiersEngine::Statistics::Statistics():
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 7a899db0c..fa3c66f4f 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -236,7 +236,7 @@ public:
   eq::EqualityEngine* getMasterEqualityEngine() ;
 public:
   /** print instantiations */
-  void printInstantiations( const char * c );
+  void printInstantiations( std::ostream& out );
   /** statistics class */
   class Statistics {
   public:
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 2e8eb51b1..7dd8d02f6 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -37,10 +37,10 @@ int RepSet::getNumRepresentatives( TypeNode tn ) const{
   }
 }
 
-void RepSet::add( Node n ){
-  TypeNode t = n.getType();
-  d_tmap[ n ] = (int)d_type_reps[t].size();
-  d_type_reps[t].push_back( n );
+void RepSet::add( TypeNode tn, Node n ){
+  d_tmap[ n ] = (int)d_type_reps[tn].size();
+  Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn << " : " << n << std::endl;
+  d_type_reps[tn].push_back( n );
 }
 
 int RepSet::getIndexFor( Node n ) const {
@@ -59,7 +59,7 @@ void RepSet::complete( TypeNode t ){
     while( !te.isFinished() ){
       Node n = *te;
       if( std::find( d_type_reps[t].begin(), d_type_reps[t].end(), n )==d_type_reps[t].end() ){
-        add( n );
+        add( t, n );
       }
       ++te;
     }
@@ -143,7 +143,7 @@ bool RepSetIterator::initialize(){
       if( !d_rep_set->hasType( tn ) ){
         Node var = NodeManager::currentNM()->mkSkolem( "repSet", tn, "is a variable created by the RepSetIterator" );
         Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
-        d_rep_set->add( var );
+        d_rep_set->add( tn, var );
       }
     }else if( tn.isInteger() ){
       bool inc = false;
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index a619915ee..c72e46e76 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -40,7 +40,7 @@ public:
   /** get cardinality for type */
   int getNumRepresentatives( TypeNode tn ) const;
   /** add representative for type */
-  void add( Node n );
+  void add( TypeNode tn, Node n );
   /** returns index in d_type_reps for node n */
   int getIndexFor( Node n ) const;
   /** complete all values */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 18968e897..c63df83ee 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1179,6 +1179,12 @@ Node TheoryEngine::getModelValue(TNode var) {
   return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
 }
 
+void TheoryEngine::printInstantiations( std::ostream& out ) {
+  if( d_quantEngine ){
+    d_quantEngine->printInstantiations( out );
+  }
+}
+
 static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
 
   std::set<TNode> all;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 0495a866b..615598e44 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -759,6 +759,11 @@ public:
   Node getModelValue(TNode var);
 
   /**
+   * Print all instantiations made by the quantifiers module.
+   */
+  void printInstantiations( std::ostream& out );
+
+  /**
    * Forwards an entailment check according to the given theoryOfMode.
    * See theory.h for documentation on entailmentCheck().
    */
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 7187a373f..203f116bb 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -737,7 +737,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
   std::map< Node, Node >::iterator itMap;
   for (itMap = constantReps.begin(); itMap != constantReps.end(); ++itMap) {
     tm->d_reps[itMap->first] = itMap->second;
-    tm->d_rep_set.add(itMap->second);
+    tm->d_rep_set.add(itMap->second.getType(), itMap->second);
   }
 
   if (!fullModel) {
@@ -745,14 +745,14 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
     // Make sure every EC has a rep
     for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap ) {
       tm->d_reps[itMap->first] = itMap->second;
-      tm->d_rep_set.add(itMap->second);
+      tm->d_rep_set.add(itMap->second.getType(), itMap->second);
     }
     for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) {
       set<Node>& noRepSet = TypeSet::getSet(it);
       set<Node>::iterator i;
       for (i = noRepSet.begin(); i != noRepSet.end(); ++i) {
         tm->d_reps[*i] = *i;
-        tm->d_rep_set.add(*i);
+        tm->d_rep_set.add((*i).getType(), *i);
       }
     }
   }