From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 4 Feb 2013 06:08:32 +0000 (-0600)
Subject: Model no longer adds subterms of quantifiers to equality engine, this fixed bug 492... 
X-Git-Tag: cvc5-1.0.0~7432
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e54c0f73712b25f1d6d49a3817c923eea077da81;p=cvc5.git

Model no longer adds subterms of quantifiers to equality engine, this fixed bug 492 and resolves previous issue for bug 486.\n Multiple improvements for E-matching: do not choose multi-triggers if single triggers exist, only create multi-triggers that contain all variables, consider multiple terms per equivalence class but only add one instantiation per round per (trigger,term) pair.\nImprovements for strong solver: make use of sort inference information when choosing splits, check for cliques eagerly when disequalities are asserted.
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4104c0916..948e42857 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2641,8 +2641,7 @@ void SmtEnginePrivate::processAssertions() {
 
   if( options::sortInference() ){
     //sort inference technique
-    SortInference si;
-    si.simplify( d_assertionsToPreprocess );
+    d_smt.d_theoryEngine->getSortInference()->simplify( d_assertionsToPreprocess );
   }
 
   dumpAssertions("pre-simplify", d_assertionsToPreprocess);
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 713587be2..bbc51c9e0 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -395,6 +395,9 @@ bool TheoryEngineModelBuilder::isAssignable(TNode n)
 
 void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cache)
 {
+  if (n.getKind()==FORALL || n.getKind()==EXISTS) {
+    return;
+  }
   if (cache.find(n) != cache.end()) {
     return;
   }
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 3b5e594fb..7dc0058cf 100755
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -41,6 +41,13 @@ InstMatchGenerator::InstMatchGenerator( std::vector< Node >& pats, QuantifiersEn
   }
 }
 
+void InstMatchGenerator::setActiveAdd(){
+  d_active_add = true;
+  if( !d_children.empty() ){
+    d_children[d_children.size()-1]->setActiveAdd();
+  }
+}
+
 void InstMatchGenerator::initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe ){
   int childMatchPolicy = d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ? 0 : d_matchPolicy;
   for( int i=0; i<(int)pats.size(); i++ ){
@@ -52,6 +59,7 @@ void InstMatchGenerator::initializePatterns( std::vector< Node >& pats, Quantifi
 }
 
 void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){
+  d_active_add = false;
   Debug("inst-match-gen") << "Pattern term is " << pat << std::endl;
   Assert( pat.hasAttribute(InstConstantAttribute()) );
   d_pattern = pat;
@@ -136,9 +144,9 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){
 }
 
 /** get match (not modulo equality) */
-bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ){
+bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe ){
   Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("
-                    << m.size() << ")" << ", " << d_children.size() << std::endl;
+                    << m << ")" << ", " << d_children.size() << std::endl;
   Assert( !d_match_pattern.isNull() );
   if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){
     return true;
@@ -191,7 +199,7 @@ bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe )
     int index = 0;
     while( index>=0 && index<(int)d_children.size() ){
       partial.push_back( InstMatch( &partial[index] ) );
-      if( d_children[index]->getNextMatch2( partial[index+1], qe ) ){
+      if( d_children[index]->getNextMatch2( f, partial[index+1], qe ) ){
         index++;
       }else{
         d_children[index]->d_cg->reset( reps[index] );
@@ -203,15 +211,22 @@ bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe )
       }
     }
     if( index>=0 ){
-      m = partial.back();
-      return true;
+      if( d_children.empty() && d_active_add ){
+        Trace("active-add") << "Active Adding instantiation " << partial.back() << std::endl;
+        bool succ = qe->addInstantiation( f, partial.back() );
+        Trace("active-add") << "Success = " << succ << std::endl;
+        return succ;
+      }else{
+        m = partial.back();
+        return true;
+      }
     }else{
       return false;
     }
   }
 }
 
-bool InstMatchGenerator::getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched ){
+bool InstMatchGenerator::getNextMatch2( Node f, InstMatch& m, QuantifiersEngine* qe, bool saveMatched ){
   bool success = false;
   Node t;
   do{
@@ -219,7 +234,7 @@ bool InstMatchGenerator::getNextMatch2( InstMatch& m, QuantifiersEngine* qe, boo
     t = d_cg->getNextCandidate();
     //if t not null, try to fit it into match m
     if( !t.isNull() && t.getType()==d_match_pattern.getType() ){
-      success = getMatch( t, m, qe );
+      success = getMatch( f, t, m, qe );
     }
   }while( !success && !t.isNull() );
   if (saveMatched) m.d_matched = t;
@@ -315,7 +330,7 @@ void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
   }
 }
 
-bool InstMatchGenerator::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
+bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){
   m.d_matched = Node::null();
   if( d_match_pattern.isNull() ){
     int index = (int)d_partial.size();
@@ -325,7 +340,7 @@ bool InstMatchGenerator::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
       }else{
         d_partial.push_back( InstMatch() );
       }
-      if( d_children[index]->getNextMatch( d_partial[index], qe ) ){
+      if( d_children[index]->getNextMatch( f, d_partial[index], qe ) ){
         index++;
       }else{
         d_children[index]->reset( Node::null(), qe );
@@ -344,7 +359,7 @@ bool InstMatchGenerator::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
       return false;
     }
   }else{
-    bool res = getNextMatch2( m, qe, true );
+    bool res = getNextMatch2( f, m, qe, true );
     Assert(!res || !m.d_matched.isNull());
     return res;
   }
@@ -356,16 +371,21 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif
   //now, try to add instantiation for each match produced
   int addedLemmas = 0;
   InstMatch m;
-  while( getNextMatch( m, qe ) ){
-    //m.makeInternal( d_quantEngine->getEqualityQuery() );
-    m.add( baseMatch );
-    if( qe->addInstantiation( f, m ) ){
-      addedLemmas++;
-      if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){
-        return addedLemmas;
+  while( getNextMatch( f, m, qe ) ){
+    //if( d_active_add ){
+    //  std::cout << "should not add at top level." << std::endl;
+    //}
+    if( !d_active_add ){
+      //m.makeInternal( d_quantEngine->getEqualityQuery() );
+      m.add( baseMatch );
+      if( qe->addInstantiation( f, m ) ){
+        addedLemmas++;
+        if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){
+          return addedLemmas;
+        }
       }
+      m.clear();
     }
-    m.clear();
   }
   //return number of lemmas added
   return addedLemmas;
@@ -375,7 +395,7 @@ int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){
   Assert( options::eagerInstQuant() );
   if( !d_match_pattern.isNull() ){
     InstMatch m;
-    if( getMatch( t, m, qe ) ){
+    if( getMatch( f, t, m, qe ) ){
       if( qe->addInstantiation( f, m ) ){
         return 1;
       }
@@ -473,7 +493,7 @@ int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, Qu
     Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl;
     std::vector< InstMatch > newMatches;
     InstMatch m;
-    while( d_children[i]->getNextMatch( m, qe ) ){
+    while( d_children[i]->getNextMatch( f, m, qe ) ){
       m.makeRepresentative( qe );
       newMatches.push_back( InstMatch( &m ) );
       m.clear();
@@ -595,7 +615,7 @@ int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){
     if( ((InstMatchGenerator*)d_children[i])->d_match_pattern.getOperator()==t.getOperator() ){
       InstMatch m;
       //if it produces a match, then process it with the rest
-      if( ((InstMatchGenerator*)d_children[i])->getMatch( t, m, qe ) ){
+      if( ((InstMatchGenerator*)d_children[i])->getMatch( f, t, m, qe ) ){
         processNewMatch( qe, m, i, addedLemmas );
       }
     }
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index af65e809b..a544f605a 100755
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -38,11 +38,13 @@ public:
   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
   virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0;
   /** get the next match.  must call reset( eqc ) before this function. */
-  virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0;
+  virtual bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) = 0;
   /** add instantiations directly */
   virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;
   /** add ground term t, called when t is added to term db */
   virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0;
+  /** set active add */
+  virtual void setActiveAdd() {}
 };/* class IMGenerator */
 
 class CandidateGenerator;
@@ -78,7 +80,7 @@ private:
   /** get the next match.  must call d_cg->reset( ... ) before using.
       only valid for use where !d_match_pattern.isNull().
   */
-  bool getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false );
+  bool getNextMatch2( Node f, InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false );
   /** for arithmetic */
   bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe );
 public:
@@ -86,7 +88,7 @@ public:
       d_match_pattern and t should have the same shape.
       only valid for use where !d_match_pattern.isNull().
   */
-  bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe );
+  bool getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe );
 
   /** constructors */
   InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchOption = 0 );
@@ -105,11 +107,14 @@ public:
   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
   void reset( Node eqc, QuantifiersEngine* qe );
   /** get the next match.  must call reset( eqc ) before this function. */
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe );
+  bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe );
   /** add instantiations */
   int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
   /** add ground term t */
   int addTerm( Node f, Node t, QuantifiersEngine* qe );
+
+  bool d_active_add;
+  void setActiveAdd();
 };/* class InstMatchGenerator */
 
 /** smart multi-trigger implementation */
@@ -152,7 +157,7 @@ public:
   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
   void reset( Node eqc, QuantifiersEngine* qe );
   /** get the next match.  must call reset( eqc ) before this function. (not implemented) */
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }
+  bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; }
   /** add instantiations */
   int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
   /** add ground term t */
@@ -178,7 +183,7 @@ public:
   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
   void reset( Node eqc, QuantifiersEngine* qe ) {}
   /** get the next match.  must call reset( eqc ) before this function. (not implemented) */
-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }
+  bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; }
   /** add instantiations */
   int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
   /** add ground term t, possibly add instantiations */
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 48af334ff..91cd2829c 100755
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -27,7 +27,6 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::inst;
 using namespace CVC4::theory::quantifiers;
 
-#define USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER
 //#define MULTI_TRIGGER_FULL_EFFORT_HALF
 #define MULTI_MULTI_TRIGGERS
 
@@ -65,18 +64,13 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
     //Notice() << "Try user-provided patterns..." << std::endl;
     for( int i=0; i<(int)d_user_gen[f].size(); i++ ){
       bool processTrigger = true;
-      if( effort!=Theory::EFFORT_LAST_CALL && d_user_gen[f][i]->isMultiTrigger() ){
-//#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF
-//        processTrigger = d_counter[f]%2==0;
-//#endif
-      }
       if( processTrigger ){
         //if( d_user_gen[f][i]->isMultiTrigger() )
-          //Notice() << "  Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl;
+          Trace("process-trigger") << "  Process (user) " << (*d_user_gen[f][i]) << "..." << std::endl;
         InstMatch baseMatch;
         int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );
         //if( d_user_gen[f][i]->isMultiTrigger() )
-          //Notice() << "  Done, numInst = " << numInst << "." << std::endl;
+          Trace("process-trigger") << "  Done, numInst = " << numInst << "." << std::endl;
         d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst;
         if( d_user_gen[f][i]->isMultiTrigger() ){
           d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
@@ -125,6 +119,7 @@ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort
       itt->first->reset( Node::null() );
     }
   }
+  d_processed_trigger.clear();
 }
 
 int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){
@@ -134,6 +129,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
   if( e<peffort ){
     return STATUS_UNFINISHED;
   }else{
+    int status = STATUS_UNKNOWN;
     bool gen = false;
     if( e==peffort ){
       if( d_counter.find( f )==d_counter.end() ){
@@ -147,7 +143,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
       gen = true;
     }
     if( gen ){
-      generateTriggers( f );
+      generateTriggers( f, effort, e, status );
     }
     Debug("quant-uf-strategy")  << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl;
     //Notice() << "Try auto-generated triggers..." << std::endl;
@@ -155,18 +151,14 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
       Trigger* tr = itt->first;
       if( tr ){
         bool processTrigger = itt->second;
-        if( effort!=Theory::EFFORT_LAST_CALL && tr->isMultiTrigger() ){
-#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF
-          processTrigger = d_counter[f]%2==0;
-#endif
-        }
-        if( processTrigger ){
+        if( processTrigger && d_processed_trigger[f].find( tr )==d_processed_trigger[f].end() ){
+          d_processed_trigger[f][tr] = true;
           //if( tr->isMultiTrigger() )
-            Debug("quant-uf-strategy-auto-gen-triggers") << "  Process " << (*tr) << "..." << std::endl;
+            Trace("process-trigger") << "  Process " << (*tr) << "..." << std::endl;
           InstMatch baseMatch;
           int numInst = tr->addInstantiations( baseMatch );
           //if( tr->isMultiTrigger() )
-            Debug("quant-uf-strategy-auto-gen-triggers") << "  Done, numInst = " << numInst << "." << std::endl;
+            Trace("process-trigger") << "  Done, numInst = " << numInst << "." << std::endl;
           if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){
             d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen_min += numInst;
           }else{
@@ -181,24 +173,24 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
     }
     Debug("quant-uf-strategy") << "done." << std::endl;
     //Notice() << "done" << std::endl;
+    return status;
   }
-  return STATUS_UNKNOWN;
 }
 
-void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
-  Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
+void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effort, int e, int & status ){
+  Trace("auto-gen-trigger-debug") << "Generate trigger for " << f << std::endl;
   if( d_patTerms[0].find( f )==d_patTerms[0].end() ){
     //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy
     d_patTerms[0][f].clear();
     d_patTerms[1][f].clear();
     std::vector< Node > patTermsF;
     Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, true );
-    Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl;
-    Debug("auto-gen-trigger") << "   ";
+    Trace("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl;
+    Trace("auto-gen-trigger") << "   ";
     for( int i=0; i<(int)patTermsF.size(); i++ ){
-      Debug("auto-gen-trigger") << patTermsF[i] << " ";
+      Trace("auto-gen-trigger") << patTermsF[i] << " ";
     }
-    Debug("auto-gen-trigger") << std::endl;
+    Trace("auto-gen-trigger") << std::endl;
     //extend to literal matching (if applicable)
     d_quantEngine->getPhaseReqTerms( f, patTermsF );
     //sort into single/multi triggers
@@ -214,23 +206,22 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
       }
     }
     d_made_multi_trigger[f] = false;
-    Debug("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl;
-    Debug("auto-gen-trigger") << "   ";
+    Trace("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl;
+    Trace("auto-gen-trigger") << "   ";
     for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){
-      Debug("auto-gen-trigger") << d_patTerms[0][f][i] << " ";
+      Trace("auto-gen-trigger") << d_patTerms[0][f][i] << " ";
     }
-    Debug("auto-gen-trigger") << std::endl;
-    Debug("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl;
-    Debug("auto-gen-trigger") << "   ";
+    Trace("auto-gen-trigger") << std::endl;
+    Trace("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl;
+    Trace("auto-gen-trigger") << "   ";
     for( int i=0; i<(int)d_patTerms[1][f].size(); i++ ){
-      Debug("auto-gen-trigger") << d_patTerms[1][f][i] << " ";
+      Trace("auto-gen-trigger") << d_patTerms[1][f][i] << " ";
     }
-    Debug("auto-gen-trigger") << std::endl;
+    Trace("auto-gen-trigger") << std::endl;
   }
 
   //populate candidate pattern term vector for the current trigger
   std::vector< Node > patTerms;
-#ifdef USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER
   //try to add single triggers first
   for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){
     if( !d_single_trigger_gen[d_patTerms[0][f][i]] ){
@@ -241,13 +232,9 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
   if( patTerms.empty() ){
     patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );
   }
-#else
-  patTerms.insert( patTerms.begin(), d_patTerms[0][f].begin(), d_patTerms[0][f].end() );
-  patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );
-#endif
 
   if( !patTerms.empty() ){
-    Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
+    Trace("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
     //sort terms based on relevance
     if( d_rlv_strategy==RELEVANCE_DEFAULT ){
       sortQuantifiersForSymbol sqfs;
@@ -273,6 +260,15 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
                                options::smartTriggers() );
       d_single_trigger_gen[ patTerms[0] ] = true;
     }else{
+      //only generate multi trigger if effort level > 5, or if no single triggers exist
+      if( !d_patTerms[0][f].empty() ){
+        if( e<=5 ){
+          status = STATUS_UNFINISHED;
+          return;
+        }else{
+          Trace("multi-trigger-debug") << "Resort to choosing multi-triggers..." << std::endl;
+        }
+      }
       //if we are re-generating triggers, shuffle based on some method
       if( d_made_multi_trigger[f] ){
 #ifndef MULTI_MULTI_TRIGGERS
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index 23f0d8a54..fa4094634 100755
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -80,12 +80,14 @@ private:
   std::map< Node, bool > d_is_single_trigger;
   std::map< Node, bool > d_single_trigger_gen;
   std::map< Node, bool > d_made_multi_trigger;
+  //processed trigger this round
+  std::map< Node, std::map< inst::Trigger*, bool > > d_processed_trigger;
 private:
   /** process functions */
   void processResetInstantiationRound( Theory::Effort effort );
   int process( Node f, Theory::Effort effort, int e );
   /** generate triggers */
-  void generateTriggers( Node f );
+  void generateTriggers( Node f, Theory::Effort effort, int e, int & status );
 public:
   /** tstrt is the type of triggers to use (maximum depth, minimum depth, or all)
       rstrt is the relevance setting for trigger (use only relevant triggers vs. use all)
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index bc45e6051..eace177b7 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -45,8 +45,8 @@ option macrosQuant --macros-quant bool :default false
 option smartTriggers /--disable-smart-triggers bool :default true
  disable smart triggers
 # Whether to use relevent triggers
-option relevantTriggers /--relevant-triggers bool :default true
- prefer triggers that are more relevant based on SInE style method
+option relevantTriggers --relevant-triggers bool :default true
+ prefer triggers that are more relevant based on SInE style analysis
 
 # Whether to consider terms in the bodies of quantifiers for matching
 option registerQuantBodyTerms --register-quant-body-terms bool :default false
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index d60aa2ef4..78109ea37 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -206,6 +206,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
     ModelBasisAttribute mba;
     mbt.setAttribute(mba,true);
     d_model_basis_term[tn] = mbt;
+    Trace("model-basis-term") << "Choose " << mbt << " as model basis term for " << tn << std::endl;
   }
   return d_model_basis_term[tn];
 }
@@ -367,6 +368,10 @@ Node TermDb::getSkolemizedBody( Node f ){
       Node skv = NodeManager::currentNM()->mkSkolem( "skv_$$", f[0][i].getType(), "is a termdb-created skolemized body" );
       d_skolem_constants[ f ].push_back( skv );
       vars.push_back( f[0][i] );
+      //carry information for sort inference
+      if( options::sortInference() ){
+        d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], skv );
+      }
     }
     d_skolem_body[ f ] = f[ 1 ].substitute( vars.begin(), vars.end(),
                                             d_skolem_constants[ f ].begin(), d_skolem_constants[ f ].end() );
@@ -515,6 +520,34 @@ int TermDb::isInstanceOf( Node n1, Node n2 ){
   return 0;
 }
 
+bool TermDb::isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ){
+  if( n1==n2 ){
+    return true;
+  }else if( n2.getKind()==INST_CONSTANT ){
+    //if( !node_contains( n1, n2 ) ){
+    //  return false;
+    //}
+    if( subs.find( n2 )==subs.end() ){
+      subs[n2] = n1;
+    }else if( subs[n2]!=n1 ){
+      return false;
+    }
+    return true;
+  }else if( n1.getKind()==n2.getKind() && n1.getMetaKind()==kind::metakind::PARAMETERIZED ){
+    if( n1.getOperator()!=n2.getOperator() ){
+      return false;
+    }
+    for( int i=0; i<(int)n1.getNumChildren(); i++ ){
+      if( !isUnifiableInstanceOf( n1[i], n2[i], subs ) ){
+        return false;
+      }
+    }
+    return true;
+  }else{
+    return false;
+  }
+}
+
 void TermDb::filterInstances( std::vector< Node >& nodes ){
   std::vector< bool > active;
   active.resize( nodes.size(), true );
@@ -523,8 +556,10 @@ void TermDb::filterInstances( std::vector< Node >& nodes ){
       if( active[i] && active[j] ){
         int result = isInstanceOf( nodes[i], nodes[j] );
         if( result==1 ){
+          Trace("filter-instances") << nodes[j] << " is an instance of " << nodes[i] << std::endl;
           active[j] = false;
         }else if( result==-1 ){
+          Trace("filter-instances") << nodes[i] << " is an instance of " << nodes[j] << std::endl;
           active[i] = false;
         }
       }
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index a1f1de1dc..9ac431107 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -212,6 +212,8 @@ private:
   std::map< TNode, std::vector< TNode > > d_var_contains;
   /** triggers for each operator */
   std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
+  /** helper for is intance of */
+  bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs );
 public:
   /** compute var contains */
   void computeVarContains( Node n );
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index bc577fda6..4b181a807 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -40,6 +40,7 @@ d_quantEngine( qe ), d_f( f ){
         d_mg = new InstMatchGeneratorSimple( f, d_nodes[0] );
       }else{
         d_mg = new InstMatchGenerator( d_nodes[0], qe, matchOption );
+        d_mg->setActiveAdd();
       }
     }else{
       d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe, matchOption );
@@ -59,7 +60,7 @@ d_quantEngine( qe ), d_f( f ){
       ++(qe->d_statistics.d_simple_triggers);
     }
   }else{
-    Debug("multi-trigger") << "Multi-trigger " << (*this) << std::endl;
+    Trace("multi-trigger") << "Multi-trigger " << (*this) << " for " << f << std::endl;
     //Notice() << "Multi-trigger for " << f << " : " << std::endl;
     //Notice() << "   " << (*this) << std::endl;
     ++(qe->d_statistics.d_multi_triggers);
@@ -80,14 +81,14 @@ void Trigger::reset( Node eqc ){
   d_mg->reset( eqc, d_quantEngine );
 }
 
-bool Trigger::getNextMatch( InstMatch& m ){
-  bool retVal = d_mg->getNextMatch( m, d_quantEngine );
+bool Trigger::getNextMatch( Node f, InstMatch& m ){
+  bool retVal = d_mg->getNextMatch( f, m, d_quantEngine );
   return retVal;
 }
 
-bool Trigger::getMatch( Node t, InstMatch& m ){
+bool Trigger::getMatch( Node f, Node t, InstMatch& m ){
   //FIXME: this assumes d_mg is an inst match generator
-  return ((InstMatchGenerator*)d_mg)->getMatch( t, m, d_quantEngine );
+  return ((InstMatchGenerator*)d_mg)->getMatch( f, t, m, d_quantEngine );
 }
 
 int Trigger::addTerm( Node t ){
@@ -115,6 +116,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
     temp.insert( temp.begin(), nodes.begin(), nodes.end() );
     std::map< Node, bool > vars;
     std::map< Node, std::vector< Node > > patterns;
+    size_t varCount = 0;
     for( int i=0; i<(int)temp.size(); i++ ){
       bool foundVar = false;
       qe->getTermDatabase()->computeVarContains( temp[i] );
@@ -122,6 +124,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
         Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j];
         if( v.getAttribute(InstConstantAttribute())==f ){
           if( vars.find( v )==vars.end() ){
+            varCount++;
             vars[ v ] = true;
             foundVar = true;
           }
@@ -134,32 +137,40 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
           patterns[ v ].push_back( temp[i] );
         }
       }
-    }
-    //now, minimalize the trigger
-    for( int i=0; i<(int)trNodes.size(); i++ ){
-      bool keepPattern = false;
-      Node n = trNodes[i];
-      for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){
-        Node v = qe->getTermDatabase()->d_var_contains[ n ][j];
-        if( patterns[v].size()==1 ){
-          keepPattern = true;
-          break;
-        }
+      if( varCount==f[0].getNumChildren() ){
+        break;
       }
-      if( !keepPattern ){
-        //remove from pattern vector
+    }
+    if( varCount<f[0].getNumChildren() ){
+      //do not generate multi-trigger if it does not contain all variables
+      return NULL;
+    }else{
+      //now, minimize the trigger
+      for( int i=0; i<(int)trNodes.size(); i++ ){
+        bool keepPattern = false;
+        Node n = trNodes[i];
         for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){
           Node v = qe->getTermDatabase()->d_var_contains[ n ][j];
-          for( int k=0; k<(int)patterns[v].size(); k++ ){
-            if( patterns[v][k]==n ){
-              patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
-              break;
+          if( patterns[v].size()==1 ){
+            keepPattern = true;
+            break;
+          }
+        }
+        if( !keepPattern ){
+          //remove from pattern vector
+          for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){
+            Node v = qe->getTermDatabase()->d_var_contains[ n ][j];
+            for( int k=0; k<(int)patterns[v].size(); k++ ){
+              if( patterns[v][k]==n ){
+                patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
+                break;
+              }
             }
           }
+          //remove from trigger nodes
+          trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 );
+          i--;
         }
-        //remove from trigger nodes
-        trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 );
-        i--;
       }
     }
   }else{
@@ -322,16 +333,16 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
     temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() );
     qe->getTermDatabase()->filterInstances( temp );
     if( temp.size()!=patTerms2.size() ){
-      Debug("trigger-filter-instance") << "Filtered an instance: " << std::endl;
-      Debug("trigger-filter-instance") << "Old: ";
+      Trace("trigger-filter-instance") << "Filtered an instance: " << std::endl;
+      Trace("trigger-filter-instance") << "Old: ";
       for( int i=0; i<(int)patTerms2.size(); i++ ){
-        Debug("trigger-filter-instance") << patTerms2[i] << " ";
+        Trace("trigger-filter-instance") << patTerms2[i] << " ";
       }
-      Debug("trigger-filter-instance") << std::endl << "New: ";
+      Trace("trigger-filter-instance") << std::endl << "New: ";
       for( int i=0; i<(int)temp.size(); i++ ){
-        Debug("trigger-filter-instance") << temp[i] << " ";
+        Trace("trigger-filter-instance") << temp[i] << " ";
       }
-      Debug("trigger-filter-instance") << std::endl;
+      Trace("trigger-filter-instance") << std::endl;
     }
     if( tstrt==TS_ALL ){
       patTerms.insert( patTerms.begin(), temp.begin(), temp.end() );
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 6fcd316f4..93731283b 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -56,12 +56,12 @@ public:
   /** reset, eqc is the equivalence class to search in (search in any if eqc=null) */
   void reset( Node eqc );
   /** get next match.  must call reset( eqc ) once before this function. */
-  bool getNextMatch( InstMatch& m );
+  bool getNextMatch( Node f, InstMatch& m );
   /** get the match against ground term or formula t.
       the trigger and t should have the same shape.
       Currently the trigger should not be a multi-trigger.
   */
-  bool getMatch( Node t, InstMatch& m);
+  bool getMatch( Node f, Node t, InstMatch& m);
   /** add ground term t, called when t is added to the TermDb */
   int addTerm( Node t );
   /** return whether this is a multi-trigger */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 08bdd496b..f938199f8 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -71,6 +71,7 @@ d_lemmas_produced_c(u){
   d_optMatchIgnoreModelBasis = false;
   d_optInstLimitActive = false;
   d_optInstLimit = 0;
+  d_total_inst_count_debug = 0;
 }
 
 QuantifiersEngine::~QuantifiersEngine(){
@@ -142,10 +143,23 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
     //build the model if not done so already
     //  this happens if no quantifiers are currently asserted and no model-building module is enabled
-    if( options::produceModels() && e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma && !d_model->isModelSet() ){
-      d_te->getModelBuilder()->buildModel( d_model, true );
+    if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
+      if( options::produceModels() && !d_model->isModelSet() ){
+        d_te->getModelBuilder()->buildModel( d_model, true );
+      }
+      if( Trace.isOn("inst-per-quant") ){
+        for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){
+          Trace("inst-per-quant") << " * " << it->second << " for " << it->first << std::endl;
+        }
+      }
+    }else{
+      if( Trace.isOn("inst-per-quant-round") ){
+        for( std::map< Node, int >::iterator it = d_temp_inst_debug.begin(); it != d_temp_inst_debug.end(); ++it ){
+          Trace("inst-per-quant-round") << " * " << it->second << " for " << it->first << std::endl;
+          d_temp_inst_debug[it->first] = 0;
+        }
+      }
     }
-
     Trace("quant-engine") << "Finished quantifiers engine check." << std::endl;
   }
 }
@@ -242,6 +256,9 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
   Node lem = nb;
   //check for duplication
   if( addLemma( lem ) ){
+    d_total_inst_debug[f]++;
+    d_temp_inst_debug[f]++;
+    d_total_inst_count_debug++;
     Trace("inst") << "*** Instantiate " << f << " with " << std::endl;
     uint64_t maxInstLevel = 0;
     for( int i=0; i<(int)terms.size(); i++ ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 29381a309..fa8a51d1f 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -119,6 +119,10 @@ private:
   rrinst::TriggerTrie* d_rr_tr_trie;
   /** extended model object */
   quantifiers::FirstOrderModel* d_model;
+  /** statistics for debugging */
+  std::map< Node, int > d_total_inst_debug;
+  std::map< Node, int > d_temp_inst_debug;
+  int d_total_inst_count_debug;
 private:
   KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time");
 public:
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 27371eac3..388c0edf0 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -41,6 +41,7 @@
 #include "util/hash.h"
 #include "util/cache.h"
 #include "util/cvc4_assert.h"
+#include "util/sort_inference.h"
 #include "theory/ite_simplifier.h"
 #include "theory/unconstrained_simplifier.h"
 #include "theory/uf/equality_engine.h"
@@ -422,6 +423,9 @@ class TheoryEngine {
 
   RemoveITE& d_iteRemover;
 
+  /** sort inference module */
+  SortInference d_sortInfer;
+
   /** Time spent in theory combination */
   TimerStat d_combineTheoriesTime;
 
@@ -732,6 +736,7 @@ public:
 
   SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; }
 
+  SortInference* getSortInference() { return &d_sortInfer; }
 private:
   std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;
 public:
diff --git a/src/theory/uf/options b/src/theory/uf/options
index 2569ccbff..d6a2bb025 100644
--- a/src/theory/uf/options
+++ b/src/theory/uf/options
@@ -25,6 +25,8 @@ option ufssAbortCardinality --uf-ss-abort-card=N int :default -1
 option ufssSmartSplits --uf-ss-smart-split bool :default false
  use smart splitting heuristic for uf strong solver
 option ufssExplainedCliques --uf-ss-explained-cliques bool :default false
- add explained clique lemmas for uf strong solver
+ use explained clique lemmas for uf strong solver
+option ufssSimpleCliques --uf-ss-simple-cliques bool :default true
+ always use simple clique lemmas for uf strong solver
 
 endmodule
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 46ac5aa60..0a96cf548 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -533,6 +533,7 @@ void StrongSolverTheoryUf::SortRepModel::assertDisequal( Node a, Node b, Node re
           //internal disequality
           d_regions[ai]->setDisequal( a, b, 1, true );
           d_regions[ai]->setDisequal( b, a, 1, true );
+          checkRegion( ai, false );  //do not need to check if it needs to combine (no new ext. disequalities)
         }else{
           //external disequality
           d_regions[ai]->setDisequal( a, b, 0, true );
@@ -610,14 +611,33 @@ void StrongSolverTheoryUf::SortRepModel::check( Theory::Effort level, OutputChan
         if( level==Theory::EFFORT_FULL ){
           if( !addedLemma ){
             Trace("uf-ss-debug") << "No splits added. " << d_cardinality << std::endl;
-            if( !options::ufssColoringSat() ){
+            Trace("uf-ss-si")  << "Must combine region" << std::endl;
+            if( true || !options::ufssColoringSat() ){
               bool recheck = false;
               //naive strategy, force region combination involving the first valid region
-              for( int i=0; i<(int)d_regions_index; i++ ){
-                if( d_regions[i]->d_valid ){
-                  forceCombineRegion( i, false );
-                  recheck = true;
-                  break;
+              if( options::sortInference()){
+                std::map< int, int > sortsFound;
+                for( int i=0; i<(int)d_regions_index; i++ ){
+                  if( d_regions[i]->d_valid ){
+                    Node op = d_regions[i]->d_nodes.begin()->first;
+                    int sort_id = d_th->getQuantifiersEngine()->getTheoryEngine()->getSortInference()->getSortId(op) ;
+                    if( sortsFound.find( sort_id )!=sortsFound.end() ){
+                      combineRegions( sortsFound[sort_id], i );
+                      recheck = true;
+                      break;
+                    }else{
+                      sortsFound[sort_id] = i;
+                    }
+                  }
+                }
+              }
+              if( !recheck ) {
+                for( int i=0; i<(int)d_regions_index; i++ ){
+                  if( d_regions[i]->d_valid ){
+                    forceCombineRegion( i, false );
+                    recheck = true;
+                    break;
+                  }
                 }
               }
               if( recheck ){
@@ -803,15 +823,10 @@ void StrongSolverTheoryUf::SortRepModel::assertCardinality( OutputChannel* out,
   }
 }
 
-void StrongSolverTheoryUf::SortRepModel::checkRegion( int ri, bool rec ){
+void StrongSolverTheoryUf::SortRepModel::checkRegion( int ri, bool checkCombine ){
   if( isValid(ri) && d_hasCard ){
     Assert( d_cardinality>0 );
-    //first check if region is in conflict
-    std::vector< Node > clique;
-    if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){
-      //explain clique
-      addCliqueLemma( clique, &d_th->getOutputChannel() );
-    }else if( d_regions[ri]->getMustCombine( d_cardinality ) ){
+    if( checkCombine && d_regions[ri]->getMustCombine( d_cardinality ) ){
       ////alternatively, check if we can reduce the number of external disequalities by moving single nodes
       //for( std::map< Node, bool >::iterator it = d_regions[i]->d_reps.begin(); it != d_regions[i]->d_reps.end(); ++it ){
       //  if( it->second ){
@@ -822,10 +837,16 @@ void StrongSolverTheoryUf::SortRepModel::checkRegion( int ri, bool rec ){
       //  }
       //}
       int riNew = forceCombineRegion( ri, true );
-      if( riNew>=0 && rec ){
-        checkRegion( riNew, rec );
+      if( riNew>=0 ){
+        checkRegion( riNew, checkCombine );
       }
     }
+    //now check if region is in conflict
+    std::vector< Node > clique;
+    if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){
+      //explain clique
+      addCliqueLemma( clique, &d_th->getOutputChannel() );
+    }
   }
 }
 
@@ -996,6 +1017,13 @@ bool StrongSolverTheoryUf::SortRepModel::addSplit( Region* r, OutputChannel* out
     Assert( s!=Node::null() && s.getKind()==EQUAL );
     s = Rewriter::rewrite( s );
     Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
+    if( options::sortInference()) {
+      for( int i=0; i<2; i++ ){
+        int si = d_th->getQuantifiersEngine()->getTheoryEngine()->getSortInference()->getSortId( s[i] );
+        Trace("uf-ss-split-si") << si << " ";
+      }
+      Trace("uf-ss-split-si")  << std::endl;
+    }
     //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " ";
     //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl;
     //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl;
@@ -1018,117 +1046,149 @@ void StrongSolverTheoryUf::SortRepModel::addCliqueLemma( std::vector< Node >& cl
   while( clique.size()>size_t(d_cardinality+1) ){
     clique.pop_back();
   }
-  if( !options::ufssExplainedCliques() ){
+  if( options::ufssSimpleCliques() && !options::ufssExplainedCliques() ){
     //add as lemma
     std::vector< Node > eqs;
     for( int i=0; i<(int)clique.size(); i++ ){
       for( int j=0; j<i; j++ ){
+        Node r1 = d_th->d_equalityEngine.getRepresentative(clique[i]);
+        Node r2 = d_th->d_equalityEngine.getRepresentative(clique[j]);
         eqs.push_back( clique[i].eqNode( clique[j] ) );
       }
     }
     eqs.push_back( d_cardinality_literal[ d_cardinality ].notNode() );
     Node lem = NodeManager::currentNM()->mkNode( OR, eqs );
+    Trace("uf-ss-lemma") << "*** Add clique conflict " << lem << std::endl;
+    ++( d_th->getStrongSolver()->d_statistics.d_clique_lemmas );
     out->lemma( lem );
-    return;
-  }
-  //if( options::ufssModelInference() ||
-  if( Trace.isOn("uf-ss-cliques") ){
-    std::vector< Node > clique_vec;
-    clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() );
-    d_cliques[ d_cardinality ].push_back( clique_vec );
-  }
-
-  //found a clique
-  Debug("uf-ss-cliques") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl;
-  Debug("uf-ss-cliques") << "   ";
-  for( int i=0; i<(int)clique.size(); i++ ){
-    Debug("uf-ss-cliques") << clique[i] << " ";
-  }
-  Debug("uf-ss-cliques") << std::endl;
-  Debug("uf-ss-cliques") << "Finding clique disequalities..." << std::endl;
-  std::vector< Node > conflict;
-  //collect disequalities, and nodes that must be equal within representatives
-  std::map< Node, std::map< Node, bool > > explained;
-  std::map< Node, std::map< Node, bool > > nodesWithinRep;
-  for( int i=0; i<(int)d_disequalities_index; i++ ){
-    //if both sides of disequality exist in clique
-    Node r1 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][0] );
-    Node r2 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][1] );
-    if( r1!=r2 && ( explained.find( r1 )==explained.end() || explained[r1].find( r2 )==explained[r1].end() ) &&
-        std::find( clique.begin(), clique.end(), r1 )!=clique.end() &&
-        std::find( clique.begin(), clique.end(), r2 )!=clique.end() ){
-      explained[r1][r2] = true;
-      explained[r2][r1] = true;
-      conflict.push_back( d_disequalities[i] );
-      Debug("uf-ss-cliques") << "   -> disequality : " << d_disequalities[i] << std::endl;
-      nodesWithinRep[r1][ d_disequalities[i][0][0] ] = true;
-      nodesWithinRep[r2][ d_disequalities[i][0][1] ] = true;
-      if( conflict.size()==(clique.size()*( clique.size()-1 )/2) ){
-        break;
+  }else{
+    //debugging information
+    if( Trace.isOn("uf-ss-cliques") ){
+      std::vector< Node > clique_vec;
+      clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() );
+      d_cliques[ d_cardinality ].push_back( clique_vec );
+    }
+    //found a clique
+    Debug("uf-ss-cliques") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl;
+    Debug("uf-ss-cliques") << "   ";
+    for( int i=0; i<(int)clique.size(); i++ ){
+      Debug("uf-ss-cliques") << clique[i] << " ";
+    }
+    Debug("uf-ss-cliques") << std::endl;
+    Debug("uf-ss-cliques") << "Finding clique disequalities..." << std::endl;
+
+    //we will scan through each of the disequaltities
+    bool isSatConflict = true;
+    std::vector< Node > conflict;
+    //collect disequalities, and nodes that must be equal within representatives
+    std::map< Node, std::map< Node, bool > > explained;
+    std::map< Node, std::map< Node, bool > > nodesWithinRep;
+    //map from the reprorted clique members to those reported in the lemma
+    std::map< Node, Node > cliqueRepMap;
+    for( int i=0; i<(int)d_disequalities_index; i++ ){
+      //if both sides of disequality exist in clique
+      Node r1 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][0] );
+      Node r2 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][1] );
+      if( r1!=r2 && ( explained.find( r1 )==explained.end() || explained[r1].find( r2 )==explained[r1].end() ) &&
+          std::find( clique.begin(), clique.end(), r1 )!=clique.end() &&
+          std::find( clique.begin(), clique.end(), r2 )!=clique.end() ){
+        explained[r1][r2] = true;
+        explained[r2][r1] = true;
+        if( options::ufssExplainedCliques() ){
+          conflict.push_back( d_disequalities[i] );
+          Debug("uf-ss-cliques") << "   -> disequality : " << d_disequalities[i] << std::endl;
+          nodesWithinRep[r1][ d_disequalities[i][0][0] ] = true;
+          nodesWithinRep[r2][ d_disequalities[i][0][1] ] = true;
+        }else{
+          //get the terms we report in the lemma
+          Node ru1 = r1;
+          if( cliqueRepMap.find( r1 )==cliqueRepMap.end() ){
+            ru1 = d_disequalities[i][0][0];
+            cliqueRepMap[r1] = ru1;
+          }else{
+            ru1 = cliqueRepMap[r1];
+          }
+          Node ru2 = r2;
+          if( cliqueRepMap.find( r2 )==cliqueRepMap.end() ){
+            ru2 = d_disequalities[i][0][1];
+            cliqueRepMap[r2] = ru2;
+          }else{
+            ru2 = cliqueRepMap[r2];
+          }
+          if( ru1!=d_disequalities[i][0][0] || ru2!=d_disequalities[i][0][1] ){
+            //disequalities have endpoints that are not connected within an equivalence class
+            // we will be producing a lemma, introducing a new literal ru1 != ru2
+            conflict.push_back( ru1.eqNode( ru2 ).notNode() );
+            isSatConflict = false;
+          }else{
+            conflict.push_back( d_disequalities[i] );
+          }
+        }
+        if( conflict.size()==(clique.size()*( clique.size()-1 )/2) ){
+          break;
+        }
       }
     }
-  }
-  //Debug("uf-ss-cliques") << conflict.size() << " " << clique.size() << std::endl;
-  Assert( (int)conflict.size()==((int)clique.size()*( (int)clique.size()-1 )/2) );
-  //Assert( (int)conflict.size()==(int)clique.size()*( (int)clique.size()-1 )/2 );
-  Debug("uf-ss-cliques") << "Finding clique equalities internal to eq classes..." << std::endl;
-  //now, we must explain equalities within each equivalence class
-  for( std::map< Node, std::map< Node, bool > >::iterator it = nodesWithinRep.begin(); it != nodesWithinRep.end(); ++it ){
-    if( it->second.size()>1 ){
-      Node prev;
-      //add explanation of t1 = t2 = ... = tn
-      Debug("uf-ss-cliques") << "Explain ";
-      for( std::map< Node, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-        if( prev!=Node::null() ){
-          Debug("uf-ss-cliques") << " = ";
-          //explain it2->first and prev
-          std::vector< TNode > expl;
-          d_th->d_equalityEngine.explainEquality( it2->first, prev, true, expl );
-          for( int i=0; i<(int)expl.size(); i++ ){
-            if( std::find( conflict.begin(), conflict.end(), expl[i] )==conflict.end() ){
-              conflict.push_back( expl[i] );
+    if( options::ufssExplainedCliques() ){
+      //Debug("uf-ss-cliques") << conflict.size() << " " << clique.size() << std::endl;
+      Assert( (int)conflict.size()==((int)clique.size()*( (int)clique.size()-1 )/2) );
+      //Assert( (int)conflict.size()==(int)clique.size()*( (int)clique.size()-1 )/2 );
+      Debug("uf-ss-cliques") << "Finding clique equalities internal to eq classes..." << std::endl;
+      //now, we must explain equalities within each equivalence class
+      for( std::map< Node, std::map< Node, bool > >::iterator it = nodesWithinRep.begin(); it != nodesWithinRep.end(); ++it ){
+        if( it->second.size()>1 ){
+          Node prev;
+          //add explanation of t1 = t2 = ... = tn
+          Debug("uf-ss-cliques") << "Explain ";
+          for( std::map< Node, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+            if( prev!=Node::null() ){
+              Debug("uf-ss-cliques") << " = ";
+              //explain it2->first and prev
+              std::vector< TNode > expl;
+              d_th->d_equalityEngine.explainEquality( it2->first, prev, true, expl );
+              for( int i=0; i<(int)expl.size(); i++ ){
+                if( std::find( conflict.begin(), conflict.end(), expl[i] )==conflict.end() ){
+                  conflict.push_back( expl[i] );
+                }
+              }
             }
+            prev = it2->first;
+            Debug("uf-ss-cliques") << prev;
           }
+          Debug("uf-ss-cliques") << std::endl;
         }
-        prev = it2->first;
-        Debug("uf-ss-cliques") << prev;
+      }
+      Debug("uf-ss-cliques") << "Explanation of clique (size=" << conflict.size() << ") = " << std::endl;
+      for( int i=0; i<(int)conflict.size(); i++ ){
+        Debug("uf-ss-cliques") << conflict[i] << " ";
       }
       Debug("uf-ss-cliques") << std::endl;
     }
-  }
-  Debug("uf-ss-cliques") << "Explanation of clique (size=" << conflict.size() << ") = " << std::endl;
-  for( int i=0; i<(int)conflict.size(); i++ ){
-    Debug("uf-ss-cliques") << conflict[i] << " ";
-    //bool value;
-    //bool hasValue = d_th->getValuation().hasSatValue( conflict[i], value );
-    //Assert( hasValue );
-    //Assert( value );
-  }
-  Debug("uf-ss-cliques") << std::endl;
-  //now, make the conflict
-#if 1
-  conflict.push_back( d_cardinality_literal[ d_cardinality ] );
-  Node conflictNode = NodeManager::currentNM()->mkNode( AND, conflict );
-  Trace("uf-ss-lemma") << "*** Add clique conflict " << conflictNode << std::endl;
-  //Notice() << "*** Add clique conflict " << conflictNode << std::endl;
-  out->conflict( conflictNode );
-  d_conflict = true;
-#else
-  Node conflictNode = conflict.size()==1 ? conflict[0] : NodeManager::currentNM()->mkNode( AND, conflict );
-  //add cardinality constraint
-  Node cardNode = d_cardinality_literal[ d_cardinality ];
-  //bool value;
-  //bool hasValue = d_th->getValuation().hasSatValue( cardNode, value );
-  //Assert( hasValue );
-  //Assert( value );
-  conflictNode = NodeManager::currentNM()->mkNode( IMPLIES, conflictNode, cardNode.notNode() );
-  Trace("uf-ss-lemma") << "*** Add clique conflict " << conflictNode << std::endl;
-  //Notice() << "*** Add clique conflict " << conflictNode << std::endl;
-  out->lemma( conflictNode );
-#endif
-  ++( d_th->getStrongSolver()->d_statistics.d_clique_lemmas );
+    //now, make the conflict
+    if( isSatConflict ){
+      conflict.push_back( d_cardinality_literal[ d_cardinality ] );
+      Node conflictNode = NodeManager::currentNM()->mkNode( AND, conflict );
+      Trace("uf-ss-lemma") << "*** Add clique conflict " << conflictNode << std::endl;
+      //Notice() << "*** Add clique conflict " << conflictNode << std::endl;
+      out->conflict( conflictNode );
+      d_conflict = true;
+      ++( d_th->getStrongSolver()->d_statistics.d_clique_conflicts );
+    }else{
+      Node conflictNode = conflict.size()==1 ? conflict[0] : NodeManager::currentNM()->mkNode( AND, conflict );
+      //add cardinality constraint
+      Node cardNode = d_cardinality_literal[ d_cardinality ];
+      //bool value;
+      //bool hasValue = d_th->getValuation().hasSatValue( cardNode, value );
+      //Assert( hasValue );
+      //Assert( value );
+      conflictNode = NodeManager::currentNM()->mkNode( IMPLIES, conflictNode, cardNode.notNode() );
+      Trace("uf-ss-lemma") << "*** Add clique lemma " << conflictNode << std::endl;
+      out->lemma( conflictNode );
+      ++( d_th->getStrongSolver()->d_statistics.d_clique_lemmas );
+    }
 
-  //DO_THIS: ensure that the same clique is not reported???  Check standard effort after assertDisequal can produce same clique.
+    //DO_THIS: ensure that the same clique is not reported???  Check standard effort after assertDisequal can produce same clique.
+  }
 }
 
 void StrongSolverTheoryUf::SortRepModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){
@@ -1222,7 +1282,7 @@ int StrongSolverTheoryUf::SortRepModel::getNumRegions(){
 }
 
 void StrongSolverTheoryUf::SortRepModel::getRepresentatives( std::vector< Node >& reps ){
-  if( !options::ufssColoringSat() ){
+  //if( !options::ufssColoringSat() ){
     bool foundRegion = false;
     for( int i=0; i<(int)d_regions_index; i++ ){
       //should not have multiple regions at this point
@@ -1235,123 +1295,9 @@ void StrongSolverTheoryUf::SortRepModel::getRepresentatives( std::vector< Node >
         foundRegion = true;
       }
     }
-  }else{
-    Unimplemented("Build representatives for fmf region sat is not implemented");
-  }
-}
-
-
-/** initialize */
-void StrongSolverTheoryUf::InfRepModel::initialize( OutputChannel* out ){
-
-}
-
-/** new node */
-void StrongSolverTheoryUf::InfRepModel::newEqClass( Node n ){
-  d_rep[n] = n;
-  //d_const_rep[n] = n.getMetaKind()==metakind::CONSTANT;
-}
-
-/** merge */
-void StrongSolverTheoryUf::InfRepModel::merge( Node a, Node b ){
-  //d_rep[b] = false;
-  //d_const_rep[a] = d_const_rep[a] || d_const_rep[b];
-  Node repb = d_rep[b];
-  Assert( !repb.isNull() );
-  if( repb.getMetaKind()==metakind::CONSTANT || isBadRepresentative( d_rep[a] ) ){
-    d_rep[a] = repb;
-  }
-  d_rep[b] = Node::null();
-}
-
-/** check */
-void StrongSolverTheoryUf::InfRepModel::check( Theory::Effort level, OutputChannel* out ){
-
-}
-
-/** minimize */
-bool StrongSolverTheoryUf::InfRepModel::minimize( OutputChannel* out ){
-#if 0
-  bool retVal = true;
-#else
-  bool retVal = !addSplit( out );
-#endif
-  if( retVal ){
-    std::vector< Node > reps;
-    getRepresentatives( reps );
-    Trace("uf-ss-fmf") << "Num representatives of type " << d_type << " : " << reps.size() << std::endl;
-    /*
-    for( int i=0; i<(int)reps.size(); i++ ){
-      std::cout << reps[i] << " ";
-    }
-    std::cout << std::endl;
-    for( int i=0; i<(int)reps.size(); i++ ){
-      std::cout << reps[i].getMetaKind() << " ";
-    }
-    std::cout << std::endl;
-    for( NodeNodeMap::iterator it = d_rep.begin(); it != d_rep.end(); ++it ){
-      Node rep = (*it).second;
-      if( !rep.isNull() && !isBadRepresentative( rep ) ){
-        for( NodeNodeMap::iterator it2 = d_rep.begin(); it2 != d_rep.end(); ++it2 ){
-          Node rep2 = (*it2).second;
-          if( !rep2.isNull() && !isBadRepresentative( rep2 ) ){
-            if( d_th->getQuantifiersEngine()->getEqualityQuery()->areDisequal( rep, rep2 ) ){
-              std::cout << "1 ";
-            }else{
-              std::cout << "0 ";
-            }
-          }
-        }
-        //std::cout << " : " << rep;
-        std::cout << std::endl;
-      }
-    }
-    */
-  }
-  return retVal;
-}
-
-/** get representatives */
-void StrongSolverTheoryUf::InfRepModel::getRepresentatives( std::vector< Node >& reps ){
-  for( NodeNodeMap::iterator it = d_rep.begin(); it != d_rep.end(); ++it ){
-    if( !(*it).second.isNull() ){
-      reps.push_back( (*it).first );
-    }
-  }
-}
-
-
-/** add split function */
-bool StrongSolverTheoryUf::InfRepModel::addSplit( OutputChannel* out ){
-  std::vector< Node > visited;
-  for( NodeNodeMap::iterator it = d_rep.begin(); it != d_rep.end(); ++it ){
-    Node rep = (*it).second;
-    if( !rep.isNull() && !isBadRepresentative( rep ) ){
-      bool constRep = rep.getMetaKind()==metakind::CONSTANT;
-      for( size_t i=0; i<visited.size(); i++ ){
-        if( !constRep || !visited[i].getMetaKind()==metakind::CONSTANT ){
-          if( !d_th->getQuantifiersEngine()->getEqualityQuery()->areDisequal( rep, visited[i] ) ){
-            //split on these nodes
-            Node eq = rep.eqNode( visited[i] );
-            Trace("uf-ss-lemma") << "*** Split on " << eq << std::endl;
-            eq = Rewriter::rewrite( eq );
-            Debug("uf-ss-lemma-debug") << "Rewritten " << eq << std::endl;
-            out->split( eq );
-            //explore the equals branch first
-            out->requirePhase( eq, true );
-            ++( d_th->getStrongSolver()->d_statistics.d_split_lemmas );
-            return true;
-          }
-        }
-      }
-      visited.push_back( rep );
-    }
-  }
-  return false;
-}
-
-bool StrongSolverTheoryUf::InfRepModel::isBadRepresentative( Node n ){
-  return n.getKind()==kind::PLUS;
+  //}else{
+  //  Unimplemented("Build representatives for fmf region sat is not implemented");
+  //}
 }
 
 StrongSolverTheoryUf::StrongSolverTheoryUf(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) :
@@ -1438,6 +1384,13 @@ void StrongSolverTheoryUf::check( Theory::Effort level ){
     if( level==Theory::EFFORT_FULL ){
       debugPrint( "uf-ss-debug" );
     }
+    if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){
+      int lemmas =  d_term_amb->disambiguateTerms( d_out );
+      d_statistics.d_disamb_term_lemmas += lemmas;
+      if( lemmas>=0 ){
+        return;
+      }
+    }
     for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
       it->second->check( level, d_out );
       if( it->second->isConflict() ){
@@ -1446,10 +1399,10 @@ void StrongSolverTheoryUf::check( Theory::Effort level ){
       }
     }
     //disambiguate terms if necessary
-    if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){
-      Assert( d_term_amb!=NULL );
-      d_statistics.d_disamb_term_lemmas += d_term_amb->disambiguateTerms( d_out );
-    }
+    //if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){
+    //  Assert( d_term_amb!=NULL );
+    //  d_statistics.d_disamb_term_lemmas += d_term_amb->disambiguateTerms( d_out );
+    //}
     Trace("uf-ss-solver") << "Done StrongSolverTheoryUf: check " << level << std::endl;
   }
 }
@@ -1481,9 +1434,6 @@ void StrongSolverTheoryUf::preRegisterTerm( TNode n ){
     if( tn.isSort() ){
       Trace("uf-ss-register") << "Preregister sort " << tn << "." << std::endl;
       rm  = new SortRepModel( n, d_th->getSatContext(), d_th );
-    }else if( tn.isInteger() ){
-      //rm = new InfRepModel( tn, d_th->getSatContext(), d_th );
-      //rm  = new SortRepModel( tn, d_th->getSatContext(), d_th );
     }else{
       /*
       if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
@@ -1603,12 +1553,14 @@ void StrongSolverTheoryUf::debugModel( TheoryModel* m ){
 }
 
 StrongSolverTheoryUf::Statistics::Statistics():
+  d_clique_conflicts("StrongSolverTheoryUf::Clique_Conflicts", 0),
   d_clique_lemmas("StrongSolverTheoryUf::Clique_Lemmas", 0),
   d_split_lemmas("StrongSolverTheoryUf::Split_Lemmas", 0),
   d_disamb_term_lemmas("StrongSolverTheoryUf::Disambiguate_Term_Lemmas", 0),
   d_totality_lemmas("StrongSolverTheoryUf::Totality_Lemmas", 0),
   d_max_model_size("StrongSolverTheoryUf::Max_Model_Size", 1)
 {
+  StatisticsRegistry::registerStat(&d_clique_conflicts);
   StatisticsRegistry::registerStat(&d_clique_lemmas);
   StatisticsRegistry::registerStat(&d_split_lemmas);
   StatisticsRegistry::registerStat(&d_disamb_term_lemmas);
@@ -1617,6 +1569,7 @@ StrongSolverTheoryUf::Statistics::Statistics():
 }
 
 StrongSolverTheoryUf::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_clique_conflicts);
   StatisticsRegistry::unregisterStat(&d_clique_lemmas);
   StatisticsRegistry::unregisterStat(&d_split_lemmas);
   StatisticsRegistry::unregisterStat(&d_disamb_term_lemmas);
@@ -1667,11 +1620,12 @@ int TermDisambiguator::disambiguateTerms( OutputChannel* out ){
                 }
                 Assert( children.size()>1 );
                 Node lem = NodeManager::currentNM()->mkNode( OR, children );
-                Debug( "uf-ss-lemma" ) << "*** Disambiguate lemma : " << lem << std::endl;
+                Trace( "uf-ss-lemma" ) << "*** Disambiguate lemma : " << lem << std::endl;
                 //Notice() << "*** Disambiguate lemma : " << lem << std::endl;
                 out->lemma( lem );
                 d_term_amb[ eq ] = false;
                 lemmaAdded++;
+                return lemmaAdded;
               }
             }
           }
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index febae2eae..ceb59d5c3 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -213,7 +213,7 @@ public:
     void setSplitScore( Node n, int s );
   private:
     /** check if we need to combine region ri */
-    void checkRegion( int ri, bool rec = true );
+    void checkRegion( int ri, bool checkCombine = true );
     /** force combine region */
     int forceCombineRegion( int ri, bool useDensity = true );
     /** merge regions */
@@ -292,42 +292,6 @@ public:
     /** get number of regions (for debugging) */
     int getNumRegions();
   }; /** class SortRepModel */
-private:
-  /** infinite rep model */
-  class InfRepModel : public RepModel
-  {
-  protected:
-    /** theory uf pointer */
-    TheoryUF* d_th;
-    /** list of representatives */
-    NodeNodeMap d_rep;
-    /** whether representatives are constant */
-    NodeBoolMap d_const_rep;
-    /** add split */
-    bool addSplit( OutputChannel* out );
-    /** is bad representative */
-    bool isBadRepresentative( Node n );
-  public:
-    InfRepModel( TypeNode tn, context::Context* c, TheoryUF* th ) : RepModel( tn ),
-      d_th( th ), d_rep( c ), d_const_rep( c ){}
-    virtual ~InfRepModel(){}
-    /** initialize */
-    void initialize( OutputChannel* out );
-    /** new node */
-    void newEqClass( Node n );
-    /** merge */
-    void merge( Node a, Node b );
-    /** assert terms are disequal */
-    void assertDisequal( Node a, Node b, Node reason ){}
-    /** check */
-    void check( Theory::Effort level, OutputChannel* out );
-    /** minimize */
-    bool minimize( OutputChannel* out );
-    /** get representatives */
-    void getRepresentatives( std::vector< Node >& reps );
-    /** print debug */
-    void debugPrint( const char* c ){}
-  };
 private:
   /** The output channel for the strong solver. */
   OutputChannel* d_out;
@@ -393,6 +357,7 @@ public:
 
   class Statistics {
   public:
+    IntStat d_clique_conflicts;
     IntStat d_clique_lemmas;
     IntStat d_split_lemmas;
     IntStat d_disamb_term_lemmas;
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
index 7e0af3e9f..cab5dac42 100755
--- a/src/util/sort_inference.cpp
+++ b/src/util/sort_inference.cpp
@@ -58,6 +58,14 @@ void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){
       printSort( "sort-inference", it->second );
       Trace("sort-inference") << std::endl;
     }
+    for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){
+      Trace("sort-inference") << "Quantified formula " << it->first << " : " << std::endl;
+      for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+        printSort( "sort-inference", it2->second );
+        Trace("sort-inference") << std::endl;
+      }
+      Trace("sort-inference") << std::endl;
+    }
   }
   if( doRewrite ){
     //simplify all assertions by introducing new symbols wherever necessary (NOTE: this is unsound for quantifiers)
@@ -149,11 +157,11 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){
   if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
     for( size_t i=0; i<n[0].getNumChildren(); i++ ){
       //TODO: try applying sort inference to quantified variables
-      //d_var_types[n][ n[0][i] ] = sortCount;
-      //sortCount++;
+      d_var_types[n][ n[0][i] ] = sortCount;
+      sortCount++;
 
       //type of the quantified variable must be the same
-      d_var_types[n][ n[0][i] ] = getIdForType( n[0][i].getType() );
+      //d_var_types[n][ n[0][i] ] = getIdForType( n[0][i].getType() );
       var_bound[ n[0][i] ] = n;
     }
   }
@@ -404,5 +412,17 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){
   }
 
 }
+int SortInference::getSortId( Node n ) {
+  Node op = n.getKind()==kind::APPLY_UF ? n.getOperator() : n;
+  return getRepresentative( d_op_return_types[op] );
+}
+
+int SortInference::getSortId( Node f, Node v ) {
+  return getRepresentative( d_var_types[f][v] );
+}
 
+void SortInference::setSkolemVar( Node f, Node v, Node sk ){
+  d_op_return_types[sk] = getSortId( f, v );
 }
+
+}
\ No newline at end of file
diff --git a/src/util/sort_inference.h b/src/util/sort_inference.h
index 363dbd84d..1378a266c 100755
--- a/src/util/sort_inference.h
+++ b/src/util/sort_inference.h
@@ -65,6 +65,10 @@ public:
   ~SortInference(){}
 
   void simplify( std::vector< Node >& assertions, bool doRewrite = false );
+  int getSortId( Node n );
+  int getSortId( Node f, Node v );
+  //set that sk is the skolem variable of v for quantifier f
+  void setSkolemVar( Node f, Node v, Node sk );
 };
 
 }
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 938e7e5c1..b81bcf799 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -143,8 +143,8 @@ BUG_TESTS = \
 	bug421.smt2 \
 	bug421b.smt2 \
 	bug425.cvc \
-	bug480.smt2 
-#	bug486.cvc
+	bug480.smt2 \
+	bug486.cvc
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 112da2a6e..3e04c8437 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -36,8 +36,10 @@ TESTS =	\
 	smtlib46f14a.smt2 \
 	smtlibf957ea.smt2 \
 	gauss_init_0030.fof.smt2 \
-	piVC_5581bd.smt2 \
-	set3.smt2
+	piVC_5581bd.smt2 
+	 
+# regression can be solved with --finite-model-find --fmf-inst-engine
+# set3.smt2
 
 # removed because it now reports unknown
 #	symmetric_unsat_7.smt2 \