From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 10 Nov 2015 13:35:25 +0000 (+0100)
Subject: Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbqi, full... 
X-Git-Tag: cvc5-1.0.0~6172
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=81dca680f6c88d10b56a0ed065d470d907766e21;p=cvc5.git

Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbqi, full saturate. Add option --purify-quant. Use disequality triggers when using relational triggers. Add regressions.
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5dfada655..4136c3163 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1442,7 +1442,8 @@ void SmtEngine::setDefaults() {
   }else{
     //counterexample-guided instantiation for non-sygus
     // enable if any quantifiers with arithmetic or datatypes
-    if( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ){
+    if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ) || 
+        options::cbqiAll() ){
       if( !options::cbqi.wasSetByUser() ){
         options::cbqi.set( true );
       }
@@ -1458,6 +1459,7 @@ void SmtEngine::setDefaults() {
       }
     }
     if( options::cbqi() && d_logic.isPure(THEORY_ARITH) ){
+      options::cbqiAll.set( false );
       if( !options::quantConflictFind.wasSetByUser() ){
         options::quantConflictFind.set( false );
       }
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index 6ff72c1a2..26689c81a 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -167,10 +167,10 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
 
  void DatatypesEnumerator::init(){
    //Assert(type.isDatatype());
-   Debug("te") << "datatype is datatype? " << d_type.isDatatype() << std::endl;
-   Debug("te") << "datatype is kind " << d_type.getKind() << std::endl;
-   Debug("te") << "datatype is " << d_type << std::endl;
-   Debug("te") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton() << " " << d_datatype.isFinite() << std::endl;
+   Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype() << std::endl;
+   Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl;
+   Debug("dt-enum") << "datatype is " << d_type << std::endl;
+   Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton() << " " << d_datatype.isFinite() << std::endl;
 
    if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){
      //start with uninterpreted constant
@@ -181,12 +181,15 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
      d_sel_sum.push_back( -1 );
    }else{
      // find the "zero" constructor via mkGroundTerm
+     Debug("dt-enum-debug") << "make ground term..." << std::endl;
      Node t = d_type.mkGroundTerm();
+     Debug("dt-enum-debug") << "done : " << t << std::endl;
      Assert( t.getKind()==kind::APPLY_CONSTRUCTOR );
      // start with the constructor for which a ground term is constructed
      d_zeroCtor = Datatype::indexOf( t.getOperator().toExpr() );
      d_has_debruijn = 0;
    }
+   Debug("dt-enum") << "zero ctor : " << d_zeroCtor << std::endl;
    d_ctor = d_zeroCtor;
    for( unsigned i=0; i<d_datatype.getNumConstructors(); ++i ){
      d_sel_types.push_back( std::vector< TypeNode >() );
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 0e7b02b53..b67c4bd56 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -154,24 +154,31 @@ Node CandidateGeneratorQELitEq::getNextCandidate(){
 CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) :
   d_match_pattern( mpat ), d_qe( qe ){
 
+  Assert( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF );
+  d_match_pattern_type = d_match_pattern[0].getType();
 }
+
 void CandidateGeneratorQELitDeq::resetInstantiationRound(){
 
 }
+
 void CandidateGeneratorQELitDeq::reset( Node eqc ){
   Node false_term = d_qe->getEqualityQuery()->getEngine()->getRepresentative( NodeManager::currentNM()->mkConst<bool>(false) );
   d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() );
 }
+
 Node CandidateGeneratorQELitDeq::getNextCandidate(){
   //get next candidate term in equivalence class
   while( !d_eqc_false.isFinished() ){
     Node n = (*d_eqc_false);
     ++d_eqc_false;
     if( n.getKind()==d_match_pattern.getKind() ){
-      //found an iff or equality, try to match it
-      //DO_THIS: cache to avoid redundancies?
-      //DO_THIS: do we need to try the symmetric equality for n?  or will it also exist in the eq class of false?
-      return n;
+      if( n[0].getType().isComparableTo( d_match_pattern_type ) ){
+        //found an iff or equality, try to match it
+        //DO_THIS: cache to avoid redundancies?
+        //DO_THIS: do we need to try the symmetric equality for n?  or will it also exist in the eq class of false?
+        return n;
+      }
     }
   }
   return Node::null();
diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h
index 9d4035970..fb120dd08 100644
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/candidate_generator.h
@@ -126,6 +126,8 @@ private:
   eq::EqClassIterator d_eqc_false;
   //equality you are trying to match disequalities for
   Node d_match_pattern;
+  //type of disequality
+  TypeNode d_match_pattern_type;
   //einstantiator pointer
   QuantifiersEngine* d_qe;
 public:
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 3e69a616a..2530402ff 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -202,6 +202,21 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
                     }
                     Node eq = eq_lhs.eqNode( eq_rhs );
                     eq = Rewriter::rewrite( eq );
+                    Node vts_coeff_inf;
+                    Node vts_coeff_delta;
+                    Node val;
+                    Node veq_c;
+                    //isolate pv in the equality
+                    int ires = isolate( pv, eq, veq_c, val, vts_coeff_inf, vts_coeff_delta );
+                    if( ires!=0 ){
+                      if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
+                        subs_proc[val][veq_c] = true;
+                        if( addInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                          return true;
+                        }
+                      }
+                    }
+                    /*
                     //cannot contain infinity?
                     //if( !d_qe->getTermDatabase()->containsVtsInfinity( eq ) ){
                     Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl;
@@ -231,6 +246,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
                         }
                       }
                     }
+                    */
                   }
                 }
                 lhs.push_back( ns );
@@ -787,14 +803,14 @@ bool CegInstantiator::addInstantiationCoeff( SolvedForm& sf, std::vector< Node >
         }
         sf.d_subs[index] = veq[1];
         if( !veq_c.isNull() ){
-          sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c );
+          sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, veq[1], veq_c );
           Trace("cbqi-inst-debug") << "...bound type is : " << btyp[index] << std::endl;
           //intger division rounding up if from a lower bound
           if( btyp[index]==1 && options::cbqiRoundUpLowerLia() ){
             sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index],
               NodeManager::currentNM()->mkNode( ITE,
                 NodeManager::currentNM()->mkNode( EQUAL,
-                  NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ),
+                  NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, veq[1], veq_c ),
                   d_zero ),
                 d_zero, d_one )
             );
@@ -1423,7 +1439,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
 }
 
 //this isolates the monomial sum into solved form (pv k t), ensures t is Int if pv is Int, and t does not contain vts symbols
-int CegInstantiator::isolate( Node pv, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta ) {
+int CegInstantiator::isolate( Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) {
   int ires = 0;
   Trace("cbqi-inst-debug") << "isolate for " << pv << " in " << atom << std::endl;
   std::map< Node, Node > msum;
@@ -1468,6 +1484,12 @@ int CegInstantiator::isolate( Node pv, Node atom, Node & veq_c, Node & val, Node
     if( ires!=0 ){
       Node realPart;
       Trace("cbqi-inst-debug") << "Isolate : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl;
+      if( options::cbqiAll() ){
+        // when not pure LIA/LRA, we must check whether the lhs contains pv
+        if( TermDb::containsTerm( val, pv ) ){
+          return 0;
+        }
+      }
       if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){
         //redo, split integer/non-integer parts
         bool useCoeff = false;
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 47e838f1c..2b4854305 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -67,8 +67,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
     if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){
       //make sure the matching portion of the equality is on the LHS of d_pattern
       //  and record what d_match_pattern is
-      if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) ||
-          d_match_pattern[0].getKind()==INST_CONSTANT ){
+      if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) || d_match_pattern[0].getKind()==INST_CONSTANT ){
         if( d_match_pattern[1].getKind()!=INST_CONSTANT ){
           Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) );
           Node mp = d_match_pattern[1];
@@ -83,8 +82,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
           d_pattern = pat.getKind()==NOT ? d_pattern.negate() : d_pattern;
           d_match_pattern = mp;
         }
-      }else if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) ||
-                d_match_pattern[1].getKind()==INST_CONSTANT ){
+      }else if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) || d_match_pattern[1].getKind()==INST_CONSTANT ){
         if( d_match_pattern[0].getKind()!=INST_CONSTANT ){
           Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) );
           if( d_pattern.getKind()!=NOT ){   //TEMPORARY until we do better implementation of disequality matching
@@ -463,7 +461,7 @@ bool VarMatchGeneratorTermSubs::getNextMatch( Node q, InstMatch& m, QuantifiersE
     Trace("var-trigger-matching") << "Matching " << d_eq_class << " against " << d_var << " in " << d_subs << std::endl;
     Node s = d_subs.substitute( d_var, d_eq_class );
     s = Rewriter::rewrite( s );
-    Trace("var-trigger-matching") << "...got " << s << std::endl;
+    Trace("var-trigger-matching") << "...got " << s << ", " << s.getKind() << std::endl;
     d_eq_class = Node::null();
     //if( s.getType().isSubtypeOf( d_var_type ) ){
     d_rm_prev = m.get( d_var_num[0] ).isNull();
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 56d5022c4..39cde56e8 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -102,8 +102,13 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
 
 void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) {
   if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
+    double clSet = 0;
+    if( Trace.isOn("cbqi-engine") ){
+      clSet = double(clock())/double(CLOCKS_PER_SEC);
+      Trace("cbqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl;
+    }
+    unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
     for( int ee=0; ee<=1; ee++ ){
-      unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
       for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
         Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
         if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
@@ -114,6 +119,13 @@ void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) {
         break;
       }
     }
+    if( Trace.isOn("cbqi-engine") ){
+      if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
+        Trace("cbqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
+      }
+      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+      Trace("cbqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl;
+    }
   }
 }
 
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 928c15593..09cf9d2eb 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -29,16 +29,11 @@ using namespace CVC4::theory::inst;
 using namespace CVC4::theory::quantifiers;
 
 //priority levels :
-//1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers, or when user-pat={ignore,resort})
+//1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers, or when user-pat={resort,ignore})
 //2 : user patterns (when user-pat=resort), auto gen patterns (for user pattern quantifiers when user-pat=use)
-//3 :
-//4 :
-//5 : full saturate quantifiers
 
 // user-pat=interleave alternates between use and resort
 
-//#define MULTI_TRIGGER_FULL_EFFORT_HALF
-
 struct sortQuantifiersForSymbol {
   QuantifiersEngine* d_qe;
   bool operator() (Node i, Node j) {
@@ -57,7 +52,7 @@ struct sortQuantifiersForSymbol {
 void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){
   //reset triggers
   for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){
-    for( int i=0; i<(int)it->second.size(); i++ ){
+    for( unsigned i=0; i<it->second.size(); i++ ){
       it->second[i]->resetInstantiationRound();
       it->second[i]->reset( Node::null() );
     }
@@ -107,27 +102,27 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
   return STATUS_UNKNOWN;
 }
 
-void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){
+void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){
   Assert( pat.getKind()==INST_PATTERN );
   //add to generators
   bool usable = true;
   std::vector< Node > nodes;
-  for( int i=0; i<(int)pat.getNumChildren(); i++ ){
+  for( unsigned i=0; i<pat.getNumChildren(); i++ ){
     nodes.push_back( pat[i] );
-    if( pat[i].getKind()!=INST_CONSTANT && !Trigger::isUsableTrigger( pat[i], f ) ){
+    if( pat[i].getKind()!=INST_CONSTANT && !Trigger::isUsableTrigger( pat[i], q ) ){
       Trace("trigger-warn") << "User-provided trigger is not usable : " << pat << " because of " << pat[i] << std::endl;
       usable = false;
       break;
     }
   }
   if( usable ){
-    Trace("user-pat") << "Add user pattern: " << pat << " for " << f << std::endl;
+    Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl;
     //check match option
     int matchOption = 0;
     if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){
-      d_user_gen_wait[f].push_back( nodes );
+      d_user_gen_wait[q].push_back( nodes );
     }else{
-      d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW, options::smartTriggers() ) );
+      d_user_gen[q].push_back( Trigger::mkTrigger( d_quantEngine, q, nodes, matchOption, true, Trigger::TR_MAKE_NEW, options::smartTriggers() ) );
     }
   }
 }
@@ -386,18 +381,18 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor
   }
 }
 
-bool InstStrategyAutoGenTriggers::hasUserPatterns( Node f ) {
-  if( f.getNumChildren()==3 ){
-    std::map< Node, bool >::iterator it = d_hasUserPatterns.find( f );
+bool InstStrategyAutoGenTriggers::hasUserPatterns( Node q ) {
+  if( q.getNumChildren()==3 ){
+    std::map< Node, bool >::iterator it = d_hasUserPatterns.find( q );
     if( it==d_hasUserPatterns.end() ){
       bool hasPat = false;
-      for( unsigned i=0; i<f[2].getNumChildren(); i++ ){
-        if( f[2][i].getKind()==INST_PATTERN ){
+      for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
+        if( q[2][i].getKind()==INST_PATTERN ){
           hasPat = true;
           break;
         }
       }
-      d_hasUserPatterns[f] = hasPat;
+      d_hasUserPatterns[q] = hasPat;
       return hasPat;
     }else{
       return it->second;
@@ -407,11 +402,11 @@ bool InstStrategyAutoGenTriggers::hasUserPatterns( Node f ) {
   }
 }
 
-void InstStrategyAutoGenTriggers::addUserNoPattern( Node f, Node pat ) {
+void InstStrategyAutoGenTriggers::addUserNoPattern( Node q, Node pat ) {
   Assert( pat.getKind()==INST_NO_PATTERN && pat.getNumChildren()==1 );
-  if( std::find( d_user_no_gen[f].begin(), d_user_no_gen[f].end(), pat[0] )==d_user_no_gen[f].end() ){
-    Trace("user-pat") << "Add user no-pattern: " << pat[0] << " for " << f << std::endl;
-    d_user_no_gen[f].push_back( pat[0] );
+  if( std::find( d_user_no_gen[q].begin(), d_user_no_gen[q].end(), pat[0] )==d_user_no_gen[q].end() ){
+    Trace("user-pat") << "Add user no-pattern: " << pat[0] << " for " << q << std::endl;
+    d_user_no_gen[q].push_back( pat[0] );
   }
 }
 
@@ -493,7 +488,7 @@ void FullSaturation::check( Theory::Effort e, unsigned quant_e ) {
     for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
       if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
-        if( process( q, e ) ){
+        if( process( q, e, quant_e ) ){
           //added lemma
           addedLemmas++;
         }
@@ -507,101 +502,110 @@ void FullSaturation::check( Theory::Effort e, unsigned quant_e ) {
   }
 }
 
-bool FullSaturation::process( Node f, Theory::Effort effort ){
+bool FullSaturation::process( Node f, Theory::Effort effort, unsigned quant_e ){
   //first, try from relevant domain
   RelevantDomain * rd = d_quantEngine->getRelevantDomain();
   unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1;
-  for( unsigned r=rstart; r<2; r++ ){
-    if( rd || r>0 ){
-      if( r==0 ){
-        Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl;
-      }else{
-        Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl;
+  unsigned rend = quant_e==QuantifiersEngine::QEFFORT_STANDARD ? rstart : 2;
+  for( unsigned r=rstart; r<=rend; r++ ){
+    if( r==1 ){
+      //complete guess
+      if( d_guessed.find( f )==d_guessed.end() ){
+        Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
+        d_guessed[f] = true;
+        InstMatch m( f );
+        if( d_quantEngine->addInstantiation( f, m ) ){
+          ++(d_quantEngine->d_statistics.d_instantiations_guess);
+          return true;
+        }
       }
-      rd->compute();
-      unsigned final_max_i = 0;
-      std::vector< unsigned > maxs;
-      for(unsigned i=0; i<f[0].getNumChildren(); i++ ){
-        unsigned ts;
+    }else{
+      if( rd || r>0 ){
         if( r==0 ){
-          ts = rd->getRDomain( f, i )->d_terms.size();
+          Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl;
         }else{
-          ts = d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()].size();
+          Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl;
+        }
+        rd->compute();
+        bool max_zero = false;
+        unsigned final_max_i = 0;
+        std::vector< unsigned > maxs;
+        for(unsigned i=0; i<f[0].getNumChildren(); i++ ){
+          unsigned ts;
+          if( r==0 ){
+            ts = rd->getRDomain( f, i )->d_terms.size();
+          }else{
+            ts = d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()].size();
+          }
+          maxs.push_back( ts );
+          Trace("inst-alg-rd") << "Variable " << i << " has " << ts << " in relevant domain." << std::endl;
+          if( ts>final_max_i ){
+            final_max_i = ts;
+          }
+          if( ts==0 ){
+            max_zero = true;
+          }
         }
-        maxs.push_back( ts );
-        Trace("inst-alg-rd") << "Variable " << i << " has " << ts << " in relevant domain." << std::endl;
-        if( ts>final_max_i ){
-          final_max_i = ts;
+        if( max_zero ){
+          final_max_i = 0;
         }
-      }
-      Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl;
+        Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl;
 
-      unsigned max_i = 0;
-      bool success;
-      while( max_i<=final_max_i ){
-        Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl;
-        std::vector< unsigned > childIndex;
-        int index = 0;
-        do {
-          while( index>=0 && index<(int)f[0].getNumChildren() ){
-            if( index==(int)childIndex.size() ){
-              childIndex.push_back( -1 );
-            }else{
-              Assert( index==(int)(childIndex.size())-1 );
-              unsigned nv = childIndex[index]+1;
-              if( options::cbqi() ){
-                //skip inst constant nodes
-                while( nv<maxs[index] && nv<=max_i &&
-                        r==1 && quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){
-                  nv++;
-                }
-              }
-              if( nv<maxs[index] && nv<=max_i ){
-                childIndex[index] = nv;
-                index++;
+        unsigned max_i = 0;
+        bool success;
+        while( max_i<=final_max_i ){
+          Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl;
+          std::vector< unsigned > childIndex;
+          int index = 0;
+          do {
+            while( index>=0 && index<(int)f[0].getNumChildren() ){
+              if( index==(int)childIndex.size() ){
+                childIndex.push_back( -1 );
               }else{
-                childIndex.pop_back();
-                index--;
+                Assert( index==(int)(childIndex.size())-1 );
+                unsigned nv = childIndex[index]+1;
+                if( options::cbqi() ){
+                  //skip inst constant nodes
+                  while( nv<maxs[index] && nv<=max_i &&
+                          r==1 && quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){
+                    nv++;
+                  }
+                }
+                if( nv<maxs[index] && nv<=max_i ){
+                  childIndex[index] = nv;
+                  index++;
+                }else{
+                  childIndex.pop_back();
+                  index--;
+                }
               }
             }
-          }
-          success = index>=0;
-          if( success ){
-            Trace("inst-alg-rd") << "Try instantiation { ";
-            for( unsigned j=0; j<childIndex.size(); j++ ){
-              Trace("inst-alg-rd") << childIndex[j] << " ";
-            }
-            Trace("inst-alg-rd") << "}" << std::endl;
-            //try instantiation
-            std::vector< Node > terms;
-            for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
-              if( r==0 ){
-                terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
+            success = index>=0;
+            if( success ){
+              Trace("inst-alg-rd") << "Try instantiation { ";
+              for( unsigned j=0; j<childIndex.size(); j++ ){
+                Trace("inst-alg-rd") << childIndex[j] << " ";
+              }
+              Trace("inst-alg-rd") << "}" << std::endl;
+              //try instantiation
+              std::vector< Node > terms;
+              for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+                if( r==0 ){
+                  terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
+                }else{
+                  terms.push_back( d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()][childIndex[i]] );
+                }
+              }
+              if( d_quantEngine->addInstantiation( f, terms, false ) ){
+                Trace("inst-alg-rd") << "Success!" << std::endl;
+                ++(d_quantEngine->d_statistics.d_instantiations_guess);
+                return true;
               }else{
-                terms.push_back( d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()][childIndex[i]] );
+                index--;
               }
             }
-            if( d_quantEngine->addInstantiation( f, terms, false ) ){
-              Trace("inst-alg-rd") << "Success!" << std::endl;
-              ++(d_quantEngine->d_statistics.d_instantiations_guess);
-              return true;
-            }else{
-              index--;
-            }
-          }
-        }while( success );
-        max_i++;
-      }
-    }
-    if( r==0 ){
-      //complete guess
-      if( d_guessed.find( f )==d_guessed.end() ){
-        Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
-        d_guessed[f] = true;
-        InstMatch m( f );
-        if( d_quantEngine->addInstantiation( f, m ) ){
-          ++(d_quantEngine->d_statistics.d_instantiations_guess);
-          return true;
+          }while( success );
+          max_i++;
         }
       }
     }
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index f02339e2e..e9eed800e 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -49,11 +49,11 @@ public:
   ~InstStrategyUserPatterns(){}
 public:
   /** add pattern */
-  void addUserPattern( Node f, Node pat );
+  void addUserPattern( Node q, Node pat );
   /** get num patterns */
-  int getNumUserGenerators( Node f ) { return (int)d_user_gen[f].size(); }
+  int getNumUserGenerators( Node q ) { return (int)d_user_gen[q].size(); }
   /** get user pattern */
-  inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; }
+  inst::Trigger* getUserGenerator( Node q, int i ) { return d_user_gen[q][ i ]; }
   /** identify */
   std::string identify() const { return std::string("UserPatterns"); }
 };/* class InstStrategyUserPatterns */
@@ -85,12 +85,12 @@ private:
 private:
   /** process functions */
   void processResetInstantiationRound( Theory::Effort effort );
-  int process( Node f, Theory::Effort effort, int e );
+  int process( Node q, Theory::Effort effort, int e );
   /** generate triggers */
-  void generateTriggers( Node f, Theory::Effort effort, int e, int& status );
+  void generateTriggers( Node q, Theory::Effort effort, int e, int& status );
   //bool addTrigger( inst::Trigger * tr, Node f, unsigned r );
   /** has user patterns */
-  bool hasUserPatterns( Node f );
+  bool hasUserPatterns( Node q );
   /** has user patterns */
   std::map< Node, bool > d_hasUserPatterns;
 public:
@@ -98,11 +98,11 @@ public:
   ~InstStrategyAutoGenTriggers(){}
 public:
   /** get auto-generated trigger */
-  inst::Trigger* getAutoGenTrigger( Node f );
+  inst::Trigger* getAutoGenTrigger( Node q );
   /** identify */
   std::string identify() const { return std::string("AutoGenTriggers"); }
   /** add pattern */
-  void addUserNoPattern( Node f, Node pat );
+  void addUserNoPattern( Node q, Node pat );
 };/* class InstStrategyAutoGenTriggers */
 
 class FullSaturation : public QuantifiersModule {
@@ -110,7 +110,7 @@ private:
   /** guessed instantiations */
   std::map< Node, bool > d_guessed;
   /** process functions */
-  bool process( Node f, Theory::Effort effort );
+  bool process( Node q, Theory::Effort effort, unsigned quant_e );
 public:
   FullSaturation( QuantifiersEngine* qe );
   ~FullSaturation(){}
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 49f561234..16cecb657 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -100,7 +100,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   if( !d_quantEngine->hasAddedLemma() ){
     return false;
   }else{
-    Trace("inst-engine") << "Added lemmas = " << (int)(d_quantEngine->d_lemmas_waiting.size()-lastWaiting)  << std::endl;
+    Trace("inst-engine") << "Added lemmas = " << (int)(d_quantEngine->getNumLemmasWaiting()-lastWaiting)  << std::endl;
     return true;
   }
 }
@@ -186,14 +186,14 @@ void InstantiationEngine::registerQuantifier( Node f ){
   }
 }
 
-void InstantiationEngine::addUserPattern( Node f, Node pat ){
+void InstantiationEngine::addUserPattern( Node q, Node pat ){
   if( d_isup ){
-    d_isup->addUserPattern( f, pat );
+    d_isup->addUserPattern( q, pat );
   }
 }
 
-void InstantiationEngine::addUserNoPattern( Node f, Node pat ){
+void InstantiationEngine::addUserNoPattern( Node q, Node pat ){
   if( d_i_ag ){
-    d_i_ag->addUserNoPattern( f, pat );
+    d_i_ag->addUserNoPattern( q, pat );
   }
 }
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 4a990ff6b..bfa610369 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -82,8 +82,8 @@ public:
   void registerQuantifier( Node q );
   Node explain(TNode n){ return Node::null(); }
   /** add user pattern */
-  void addUserPattern( Node f, Node pat );
-  void addUserNoPattern( Node f, Node pat );
+  void addUserPattern( Node q, Node pat );
+  void addUserNoPattern( Node q, Node pat );
 public:
   /** Identify this module */
   std::string identify() const { return "InstEngine"; }
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 2578d0b7f..d7b66d52d 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -55,6 +55,8 @@ option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
  perform aggressive miniscoping for quantifiers
 option elimTautQuant --elim-taut-quant bool :default true
  eliminate tautological disjuncts of quantified formulas
+option purifyQuant --purify-quant bool :default false
+ purify quantified formulas
  
 #### E-matching options
  
@@ -241,7 +243,7 @@ option cbqiSat --cbqi-sat bool :read-write :default true
  answer sat when quantifiers are asserted with counterexample-based quantifier instantiation
 option cbqiModel --cbqi-model bool :read-write :default true
  guide instantiations by model values for counterexample-based quantifier instantiation
-option cbqiAll --cbqi-all bool :default false
+option cbqiAll --cbqi-all bool :read-write :default false
  apply counterexample-based instantiation to all quantified formulas
 option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false
  use integer infinity for vts in counterexample-based quantifier instantiation
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 0b212d696..d289e3938 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -79,7 +79,7 @@ bool QuantArith::getMonomialSumLit( Node lit, std::map< Node, Node >& msum ) {
                                                                 it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it->second );
               msum[it->first] = Rewriter::rewrite( r );
             }else{
-              msum[it->first] = negate( it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it->second );
+              msum[it->first] = it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(-1) ) : negate( it->second );
             }
           }
           return true;
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 895408269..dcf58e692 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -16,6 +16,7 @@
 #include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/quantifiers/trigger.h"
 
 using namespace std;
 using namespace CVC4;
@@ -82,6 +83,16 @@ bool QuantifiersRewriter::isCube( Node n ){
   }
 }
 
+int QuantifiersRewriter::getPurifyId( Node n ){
+  if( inst::Trigger::isAtomicTriggerKind( n.getKind() ) ){
+    return 1;
+  }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL ){
+    return 0;
+  }else{
+    return -1;
+  }
+}
+
 void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){
   if( n.getKind()==OR ){
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
@@ -758,70 +769,106 @@ Node QuantifiersRewriter::computeProcessIte( Node body, Node ipl ){
   return body;
 }
 
+bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent ) {
+  if( TermDb::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){
+    return false;
+  }else{
+    if( !var_parent.empty() ){
+      std::map< Node, std::vector< int > >::iterator it = var_parent.find( v );
+      if( it!=var_parent.end() ){
+        Assert( !it->second.empty() );
+        int id = getPurifyId( s );
+        return it->second.size()==1 && it->second[0]==id;
+      }
+    }
+    return true;
+  }
+}
 
-Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){
-  Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl;
-  QuantPhaseReq qpr( body );
-  std::vector< Node > vars;
-  std::vector< Node > subs;
-  for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
-    //Notice() << "   " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl;
-    if( it->first.getKind()==EQUAL ){
-      if( it->second && options::varElimQuant() ){
-        TypeNode types[2];
-        for( int i=0; i<2; i++ ){
-          types[i] = it->first[i].getType();
+bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vector< Node >& args, std::vector< Node >& vars, std::vector< Node >& subs,
+                                                  std::map< Node, std::vector< int > >& var_parent ) {
+  if( lit.getKind()==EQUAL && pol ){
+    for( unsigned i=0; i<2; i++ ){
+      std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit[i] );
+      if( ita!=args.end() ){
+        if( isVariableElim( lit[i], lit[1-i], var_parent ) ){
+          vars.push_back( lit[i] );
+          subs.push_back( lit[1-i] );
+          args.erase( ita );
+          return true;
         }
-        for( int i=0; i<2; i++ ){
-          std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[i] );
+      }
+    }
+    //for arithmetic, solve the equality
+    if( lit[0].getType().isReal() ){
+      std::map< Node, Node > msum;
+      if( QuantArith::getMonomialSumLit( lit, msum ) ){
+        for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){
+          std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), itm->first );
           if( ita!=args.end() ){
-            if( !TermDb::containsTerm( it->first[1-i], it->first[i] ) && types[1-i].isSubtypeOf( types[i] ) ){
-              vars.push_back( it->first[i] );
-              subs.push_back( it->first[1-i] );
+            Node veq_c;
+            Node val;
+            int ires = QuantArith::isolate( itm->first, msum, veq_c, val, EQUAL );
+            if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val, var_parent ) ){
+              vars.push_back( itm->first );
+              subs.push_back( val );
               args.erase( ita );
-              break;
+              return true;
             }
           }
         }
-        if( !vars.empty() ){
-          break;
-        }
       }
-    }else if( it->first.getKind()==APPLY_TESTER ){
-      if( options::dtVarExpandQuant() && it->second && it->first[0].getKind()==BOUND_VARIABLE ){
-        Trace("var-elim-dt") << "Expand datatype variable based on : " << it->first << std::endl;
-        std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[0] );
-        if( ita!=args.end() ){
-          vars.push_back( it->first[0] );
-          Expr testerExpr = it->first.getOperator().toExpr();
-          int index = Datatype::indexOf( testerExpr );
-          const Datatype& dt = Datatype::datatypeOf(testerExpr);
-          const DatatypeConstructor& c = dt[index];
-          std::vector< Node > newChildren;
-          newChildren.push_back( Node::fromExpr( c.getConstructor() ) );
-          std::vector< Node > newVars;
-          for( unsigned j=0; j<c.getNumArgs(); j++ ){
-            TypeNode tn = TypeNode::fromType( c[j].getSelector().getType() );
-            tn = tn[1];
-            Node v = NodeManager::currentNM()->mkBoundVar( tn );
-            newChildren.push_back( v );
-            newVars.push_back( v );
-          }
-          subs.push_back( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, newChildren ) );
-          Trace("var-elim-dt") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl;
-          args.erase( ita );
-          args.insert( args.end(), newVars.begin(), newVars.end() );
-        }
-      }
-    }else if( it->first.getKind()==BOUND_VARIABLE ){
-      if( options::varElimQuant() ){
-        std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first );
-        if( ita!=args.end() ){
-          Trace("var-elim-bool") << "Variable eliminate : " << it->first << " in " << body << std::endl;
-          vars.push_back( it->first );
-          subs.push_back( NodeManager::currentNM()->mkConst( it->second ) );
-          args.erase( ita );
-        }
+    }
+  }else if( lit.getKind()==APPLY_TESTER && pol && lit[0].getKind()==BOUND_VARIABLE ){
+    Trace("var-elim-dt") << "Expand datatype variable based on : " << lit << std::endl;
+    std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit[0] );
+    if( ita!=args.end() ){
+      vars.push_back( lit[0] );
+      Expr testerExpr = lit.getOperator().toExpr();
+      int index = Datatype::indexOf( testerExpr );
+      const Datatype& dt = Datatype::datatypeOf(testerExpr);
+      const DatatypeConstructor& c = dt[index];
+      std::vector< Node > newChildren;
+      newChildren.push_back( Node::fromExpr( c.getConstructor() ) );
+      std::vector< Node > newVars;
+      for( unsigned j=0; j<c.getNumArgs(); j++ ){
+        TypeNode tn = TypeNode::fromType( c[j].getSelector().getType() );
+        tn = tn[1];
+        Node v = NodeManager::currentNM()->mkBoundVar( tn );
+        newChildren.push_back( v );
+        newVars.push_back( v );
+      }
+      subs.push_back( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, newChildren ) );
+      Trace("var-elim-dt") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl;
+      args.erase( ita );
+      args.insert( args.end(), newVars.begin(), newVars.end() );
+      return true;
+    }
+  }else if( lit.getKind()==BOUND_VARIABLE ){
+    std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit );
+    if( ita!=args.end() ){
+      Trace("var-elim-bool") << "Variable eliminate : " << lit << std::endl;
+      vars.push_back( lit );
+      subs.push_back( NodeManager::currentNM()->mkConst( pol ) );
+      args.erase( ita );
+      return true;
+    }
+  }
+  return false;
+}
+
+Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >& args, Node& ipl, std::map< Node, std::vector< int > >& var_parent ){
+  Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl;
+  QuantPhaseReq qpr( body );
+  std::vector< Node > vars;
+  std::vector< Node > subs;
+  for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
+    //Notice() << "   " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl;
+    if( ( it->first.getKind()==EQUAL && it->second && options::varElimQuant() ) ||
+        ( it->first.getKind()==APPLY_TESTER && it->second && it->first[0].getKind()==BOUND_VARIABLE && options::dtVarExpandQuant() ) ||
+        ( it->first.getKind()==BOUND_VARIABLE && options::varElimQuant() ) ){
+      if( computeVariableElimLit( it->first, it->second, args, vars, subs, var_parent ) ){
+        break;
       }
     }
   }
@@ -838,6 +885,22 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
   return body;
 }
 
+Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){
+  //the parent id's for each variable, if using purifyQuant
+  std::map< Node, std::vector< int > > var_parent;
+  if( options::purifyQuant() ){
+    body = computePurify( body, args, var_parent );
+  }
+  if( options::varElimQuant() || options::dtVarExpandQuant() ){
+    Node prev;
+    do{
+      prev = body;
+      body = computeVarElimination2( body, args, ipl, var_parent );
+    }while( prev!=body && !args.empty() );
+  }
+  return body;
+}
+
 Node QuantifiersRewriter::computeClause( Node n ){
   Assert( isClause( n ) );
   if( isLiteral( n ) ){
@@ -1348,7 +1411,7 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
   }else if( computeOption==COMPUTE_PRENEX ){
     return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
-    return options::varElimQuant() || options::dtVarExpandQuant();
+    return options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant();
   //}else if( computeOption==COMPUTE_CNF ){
   //  return options::cnfQuant();
   }else{
@@ -1394,11 +1457,7 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp
     }else if( computeOption==COMPUTE_PRENEX ){
       n = computePrenex( n, args, true );
     }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
-      Node prev;
-      do{
-        prev = n;
-        n = computeVarElimination( n, args, ipl );
-      }while( prev!=n && !args.empty() );
+      n = computeVarElimination( n, args, ipl );
     //}else if( computeOption==COMPUTE_CNF ){
       //n = computeCNF( n, args, defs, false );
       //ipl = Node::null();
@@ -1620,3 +1679,83 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
   }
   return n;
 }
+
+
+Node QuantifiersRewriter::computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term,
+                                          std::map< Node, std::vector< int > >& var_parent, int parentId ){
+  std::map< Node, Node >::iterator it = visited.find( body );
+  if( it!=visited.end() ){
+    return it->second;
+  }else{
+    Node ret = body;
+    if( body.getNumChildren()>0 && body.getKind()!=FORALL ){
+      std::vector< Node > children;
+      bool childrenChanged = false;
+      int id = getPurifyId( body );
+      for( unsigned i=0; i<body.getNumChildren(); i++ ){
+        Node bi = computePurify2( body[i], args, visited, var_to_term, var_parent, id );
+        childrenChanged = childrenChanged || bi!=body[i];
+        children.push_back( bi );
+        if( id!=0 && bi.getKind()==BOUND_VARIABLE ){
+          if( std::find( var_parent[bi].begin(), var_parent[bi].end(), id )==var_parent[bi].end() ){
+            var_parent[bi].push_back( id );
+          }
+        }
+      }
+      if( childrenChanged ){
+        if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
+          children.insert( children.begin(), body.getOperator() );
+        }
+        ret = NodeManager::currentNM()->mkNode( body.getKind(), children );
+      }
+      if( parentId!=0 && parentId!=id ){
+        //must purify if this has a bound variable
+        if( TermDb::containsTerms( ret, args ) ){
+          Node v = NodeManager::currentNM()->mkBoundVar( ret.getType() );
+          var_to_term[v] = Rewriter::rewrite( v.eqNode( ret ) );
+          ret = v;
+          args.push_back( v );
+        }
+      }
+    }
+    visited[body] = ret;
+    return ret;
+  }
+}
+
+Node QuantifiersRewriter::computePurify( Node body, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ) {
+  std::map< Node, Node > visited;
+  std::map< Node, Node > var_to_term;
+  Node pbody = computePurify2( body, args, visited, var_to_term, var_parent, 0 );
+  if( pbody==body ){
+    return body;
+  }else{
+    Trace("quantifiers-rewrite-purify") << "Purify : " << body << std::endl;
+    Trace("quantifiers-rewrite-purify") << "   Got : " << pbody << std::endl;
+    for( std::map< Node, Node >::iterator it = var_to_term.begin(); it != var_to_term.end(); ++it ){
+      Trace("quantifiers-rewrite-purify") << "         " << it->first << " : " << it->second << std::endl;
+    }
+    Trace("quantifiers-rewrite-purify") << "Variable parents : " << std::endl;
+    for( std::map< Node, std::vector< int > >::iterator it = var_parent.begin(); it != var_parent.end(); ++it ){
+      Trace("quantifiers-rewrite-purify") << "  " << it->first << " -> ";
+      for( unsigned i=0; i<it->second.size(); i++ ){
+        Trace("quantifiers-rewrite-purify") << it->second[i] << " ";
+      }
+      Trace("quantifiers-rewrite-purify") << std::endl;
+    }
+    Trace("quantifiers-rewrite-purify") << std::endl;
+    std::vector< Node > disj;
+    for( std::map< Node, Node >::iterator it = var_to_term.begin(); it != var_to_term.end(); ++it ){
+      disj.push_back( it->second.negate() );
+    }
+    Node res;
+    if( disj.empty() ){
+      res = pbody;
+    }else{
+      disj.push_back( pbody );
+      res = NodeManager::currentNM()->mkNode( OR, disj );
+    }
+    Trace("quantifiers-rewrite-purify") << "Constructed : " << res << std::endl << std::endl;
+    return res;
+  }
+}
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 0ad79587a..daf5a8bad 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -31,6 +31,7 @@ public:
   static bool isClause( Node n );
   static bool isLiteral( Node n );
   static bool isCube( Node n );
+  static int getPurifyId( Node n );
 private:
   static void addNodeToOrBuilder( Node n, NodeBuilder<>& t );
   static Node mkForAll( std::vector< Node >& args, Node body, Node ipl );
@@ -40,6 +41,12 @@ private:
   static Node computeClause( Node n );
   static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj );
   static bool isConditionalVariableElim( Node n, int pol=0 );
+  static bool isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent );
+  static bool computeVariableElimLit( Node n, bool pol, std::vector< Node >& args, std::vector< Node >& var, std::vector< Node >& subs,
+                                      std::map< Node, std::vector< int > >& var_parent );
+  static Node computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term,
+                              std::map< Node, std::vector< int > >& var_parent, int parentId );
+  static Node computeVarElimination2( Node body, std::vector< Node >& args, Node& ipl, std::map< Node, std::vector< int > >& var_parent );
 private:
   static Node computeElimSymbols( Node body );
   static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl );
@@ -50,10 +57,11 @@ private:
                                    std::map< Node, Node >& cache, std::map< Node, Node >& icache,
                                    std::vector< Node >& new_vars, std::vector< Node >& new_conds );
   static Node computeProcessIte( Node body, Node ipl );
-  static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl );
   static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred );
   static Node computePrenex( Node body, std::vector< Node >& args, bool pol );
   static Node computeSplit( Node f, std::vector< Node >& args, Node body );
+  static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl );
+  static Node computePurify( Node body, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent );
 private:
   enum{
     COMPUTE_ELIM_SYMBOLS = 0,
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index e513666a4..e41af5e2d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -699,19 +699,6 @@ bool TermDb::hasInstConstAttr( Node n ) {
   return !getInstConstAttr(n).isNull();
 }
 
-void TermDb::getBoundVars( Node n, std::vector< Node >& bvs) {
-  if (n.getKind()==BOUND_VARIABLE ){
-    if ( std::find( bvs.begin(), bvs.end(), n)==bvs.end() ){
-      bvs.push_back( n );
-    }
-  }else{
-    for( unsigned i=0; i<n.getNumChildren(); i++) {
-      getBoundVars(n[i], bvs);
-    }
-  }
-}
-
-
 /** get the i^th instantiation constant of q */
 Node TermDb::getInstantiationConstant( Node q, int i ) const {
   std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q );
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index bc8851195..f809aa5b8 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -262,10 +262,6 @@ public:
 
   static Node getInstConstAttr( Node n );
   static bool hasInstConstAttr( Node n );
-//for bound variables
-public:
-  //get bound variables in n
-  static void getBoundVars( Node n, std::vector< Node >& bvs );
 
 
 //for skolem
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index de3c503b5..1f332e909 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -212,11 +212,11 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOpt
   return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers );
 }
 
-bool Trigger::isUsable( Node n, Node f ){
-  if( quantifiers::TermDb::getInstConstAttr(n)==f ){
+bool Trigger::isUsable( Node n, Node q ){
+  if( quantifiers::TermDb::getInstConstAttr(n)==q ){
     if( isAtomicTrigger( n ) ){
       for( int i=0; i<(int)n.getNumChildren(); i++ ){
-        if( !isUsable( n[i], f ) ){
+        if( !isUsable( n[i], q ) ){
           return false;
         }
       }
@@ -227,8 +227,7 @@ bool Trigger::isUsable( Node n, Node f ){
       std::map< Node, Node > coeffs;
       if( isBooleanTermTrigger( n ) ){
         return true;
-      }
-      if( options::purifyTriggers() ){
+      }else if( options::purifyTriggers() ){
         Node x = getInversionVariable( n );
         if( !x.isNull() ){
           return true;
@@ -241,41 +240,39 @@ bool Trigger::isUsable( Node n, Node f ){
   }
 }
 
-bool nodeContainsVar( Node n, Node v ){
-  if( n==v) {
-    return true;
-  }else{
-    for( unsigned i=0; i<n.getNumChildren(); i++) {
-      if( nodeContainsVar(n[i], v) ){
-        return true;
-      }
-    }
-    return false;
-  }
-}
-
 Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
   Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
+  if( n.getKind()==NOT ){
+    pol = !pol;
+    n = n[0];
+  }
   if( options::relationalTriggers() ){
     if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){
       Node rtr;
+      bool do_negate = hasPol && pol;
       for( unsigned i=0; i<2; i++) {
-        unsigned j = (i==0) ? 1 : 0;
-        if( n[j].getKind()==INST_CONSTANT && isUsableTrigger(n[i], f) && !nodeContainsVar( n[i], n[j] ) ) {
-          rtr = n;
-          break;
+        if( n[1-i].getKind()==INST_CONSTANT ){
+          if( isUsableTrigger(n[i], f) && !quantifiers::TermDb::containsTerm( n[i], n[1-i] ) ){
+            rtr = n;
+            break;
+          }
+          if( n[i].getKind()==INST_CONSTANT && ( !hasPol || pol ) ){
+            do_negate = true;
+            rtr = n;
+            break;
+          }
         }
       }
       if( n[0].getType().isInteger() ){
         //try to rearrange?
         std::map< Node, Node > m;
-        if (QuantArith::getMonomialSumLit(n, m) ){
+        if( QuantArith::getMonomialSumLit(n, m) ){
           for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){
             if( !it->first.isNull() && it->first.getKind()==INST_CONSTANT ){
               Node veq;
               if( QuantArith::isolate( it->first, m, veq, n.getKind() )!=0 ){
                 int vti = veq[0]==it->first ? 1 : 0;
-                if( isUsableTrigger(veq[vti], f) && !nodeContainsVar( veq[vti], veq[vti==0 ? 1 : 0]) ){
+                if( isUsableTrigger( veq[vti], f ) && !quantifiers::TermDb::containsTerm( veq[vti], veq[1-vti] ) ){
                   rtr = veq;
                 }
               }
@@ -290,7 +287,8 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
         if( hasPol ){
           Trace("relational-trigger") << "    polarity : " << pol << std::endl;
         }
-        Node rtr2 = (hasPol && pol) ? rtr.negate() : rtr;
+        Node rtr2 = do_negate ? rtr.negate() : rtr;
+        Trace("relational-trigger") << "    return : " << rtr2 << std::endl;
         return rtr2;
       }
     }
@@ -304,8 +302,8 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
   }
 }
 
-bool Trigger::isUsableTrigger( Node n, Node f ){
-  Node nu = getIsUsableTrigger(n,f);
+bool Trigger::isUsableTrigger( Node n, Node q ){
+  Node nu = getIsUsableTrigger( n, q );
   return !nu.isNull();
 }
 
@@ -346,16 +344,15 @@ bool Trigger::isSimpleTrigger( Node n ){
 bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ){
   if( patMap.find( n )==patMap.end() ){
     patMap[ n ] = false;
-    bool newHasPol = n.getKind()==IFF ? false : hasPol;
-    bool newPol = n.getKind()==NOT ? !pol : pol;
     if( tstrt==TS_MIN_TRIGGER ){
       if( n.getKind()==FORALL ){
         return false;
       }else{
         bool retVal = false;
-        for( int i=0; i<(int)n.getNumChildren(); i++ ){
-          bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol;
-          if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          bool newHasPol, newPol;
+          QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
+          if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol ) ){
             retVal = true;
           }
         }
@@ -389,9 +386,10 @@ bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap,
         }
       }
       if( n.getKind()!=FORALL ){
-        for( int i=0; i<(int)n.getNumChildren(); i++ ){
-          bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol;
-          if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          bool newHasPol, newPol;
+          QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
+          if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol ) ){
             retVal = true;
           }
         }
@@ -558,13 +556,19 @@ Node Trigger::getInversion( Node n, Node x ) {
         }else if( n.getKind()==MULT ){
           Assert( n[i].isConst() );
           if( x.getType().isInteger() ){
-            Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst<Rational>() );
-            x = NodeManager::currentNM()->mkNode( INTS_DIVISION, x, coeff );
+            Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst<Rational>().abs() );
+            if( !n[i].getConst<Rational>().abs().isOne() ){
+              x = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, x, coeff );
+            }
+            if( n[i].getConst<Rational>().sgn()<0 ){
+              x = NodeManager::currentNM()->mkNode( UMINUS, x );
+            }
           }else{
             Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst<Rational>() );
             x = NodeManager::currentNM()->mkNode( MULT, x, coeff );
           }
         }
+        x = Rewriter::rewrite( x );
       }else{
         Assert( cindex==-1 );
         cindex = i;
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 1817ebe56..11962008e 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -91,7 +91,7 @@ public:
                              bool smartTriggers = false );
 private:
   /** is subterm of trigger usable */
-  static bool isUsable( Node n, Node f );
+  static bool isUsable( Node n, Node q );
   static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false );
   /** collect all APPLY_UF pattern terms for f in n */
   static bool collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol );
@@ -105,7 +105,7 @@ public:
   static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst = false );
 public:
   /** is usable trigger */
-  static bool isUsableTrigger( Node n, Node f );
+  static bool isUsableTrigger( Node n, Node q );
   static bool isAtomicTrigger( Node n );
   static bool isAtomicTriggerKind( Kind k );
   static bool isCbqiKind( Kind k );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index aab04c32c..990d3389e 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -901,7 +901,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
   Assert( terms.size()==q[0].getNumChildren() );
   Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl;
   for( unsigned i=0; i<terms.size(); i++ ){
-    Trace("inst-add-debug") << "  " << q[0][i] << " -> " << terms[i];
+    Trace("inst-add-debug") << "  " << q[0][i] << " -> " << terms[i] << std::endl;
     //make it representative, this is helpful for recognizing duplication
     if( mkRep ){
       //pick the best possible representative for instantiation, based on past use and simplicity of term
@@ -910,7 +910,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
       //ensure the type is correct
       terms[i] = quantifiers::TermDb::mkNodeType( terms[i], q[0][i].getType() );
     }
-    Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
+    Trace("inst-add-debug2") << " -> " << terms[i] << std::endl;
     Assert( !terms[i].isNull() );
   }
 
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 138fb4bb0..a53759c08 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -334,6 +334,20 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
   }
 }
 
+Expr getSubtermWithType( Expr e, Type t, bool isTop ){
+  if( !isTop && e.getType()==t ){
+    return e;
+  }else{
+    for( unsigned i=0; i<e.getNumChildren(); i++ ){
+      Expr se = getSubtermWithType( e[i], t, false );
+      if( !se.isNull() ){
+        return se;
+      }
+    }
+    return Expr();
+  }
+}
+
 Expr Datatype::computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException) {
   if( std::find( processing.begin(), processing.end(), d_self )==processing.end() ){
     processing.push_back( d_self );
@@ -342,8 +356,14 @@ Expr Datatype::computeGroundTerm( Type t, std::vector< Type >& processing ) cons
         //do nullary constructors first
         if( ((*i).getNumArgs()==0)==(r==0)){
           Debug("datatypes") << "Try constructing for " << (*i).getName() << ", processing = " << processing.size() << std::endl;
-          Expr e = (*i).computeGroundTerm( t, processing );
+          Expr e = (*i).computeGroundTerm( t, processing, d_ground_term );
           if( !e.isNull() ){
+            //must check subterms for the same type to avoid infinite loops in type enumeration
+            Expr se = getSubtermWithType( e, t, true );
+            if( !se.isNull() ){
+              Debug("datatypes") << "Take subterm " << se << std::endl;
+              e = se;
+            }
             processing.pop_back();
             return e;
           }else{
@@ -780,7 +800,7 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) {
   return true;
 }
 
-Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException) {
+Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& processing, std::map< Type, Expr >& gt ) const throw(IllegalArgumentException) {
 // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_constructor);
 
@@ -801,8 +821,13 @@ Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& proces
     }
     Expr arg;
     if( selType.isDatatype() ){
-      const Datatype & dt = DatatypeType(selType).getDatatype();
-      arg = dt.computeGroundTerm( selType, processing );
+      std::map< Type, Expr >::iterator itgt = gt.find( selType );
+      if( itgt != gt.end() ){
+        arg = itgt->second;
+      }else{
+        const Datatype & dt = DatatypeType(selType).getDatatype();
+        arg = dt.computeGroundTerm( selType, processing );
+      }
     }else{
       arg = selType.mkGroundTerm();
     }
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 0b8b8c61f..85668cd55 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -218,7 +218,7 @@ private:
   /** compute whether this datatype is well-founded */
   bool computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException);
   /** compute ground term */
-  Expr computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException);
+  Expr computeGroundTerm( Type t, std::vector< Type >& processing, std::map< Type, Expr >& gt ) const throw(IllegalArgumentException);
 public:
   /**
    * Create a new Datatype constructor with the given name for the
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 45a9d6f30..d06fb1b9b 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -67,7 +67,8 @@ TESTS =	\
 	manos-model.smt2 \
 	bug625.smt2 \
 	cdt-model-cade15.smt2 \
-	sc-cdt1.smt2
+	sc-cdt1.smt2  \
+	conqueue-dt-enum-iloop.smt2
 
 FAILING_TESTS = \
 	datatype-dump.cvc
diff --git a/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 b/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2
new file mode 100644
index 000000000..6f82cd842
--- /dev/null
+++ b/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2
@@ -0,0 +1,75 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-fun start!13 () Bool)
+
+(assert start!13)
+
+(declare-fun b!39 () Bool)
+
+(declare-sort T!14 0)
+
+(declare-datatypes () ( 
+(LazyConQ!5 
+  (Lazyarg1!5 (carry!37 Conc!6) (srear!9 LazyConQ!5)) 
+  (Lazyarg2!5 (t!270 ConQ!6)) 
+  (Lazyarg3!5 (carry!38 Conc!6) (t!271 ConQ!6)) 
+  (Lazyarg4!5 (tree!19 Conc!6) (carry!39 Conc!6)) 
+  (Lazyarg5!5 (tree!20 Conc!6) (carry!40 Conc!6)) 
+  (PushLeft!5 (ys!22 Conc!6) (xs!60 LazyConQ!5)) 
+  (PushLeftLazy!5 (ys!23 Conc!6) (xs!61 LazyConQ!5)))  
+(Conc!6 
+  (CC!5 (left!9 Conc!6) (right!9 Conc!6)) 
+  (Empty!5) 
+  (Single!5 (x!106 T!14)))  
+(ConQ!6 
+  (Spine!5 (head!10 Conc!6) (rear!5 LazyConQ!5)) 
+  (Tip!5 (t!272 Conc!6))) 
+))
+
+(declare-fun e!41 () LazyConQ!5)
+
+(declare-fun l!2 () LazyConQ!5)
+
+(declare-fun st!3 () (Set LazyConQ!5))
+
+(declare-fun firstUnevaluated!3 (LazyConQ!5 (Set LazyConQ!5)) LazyConQ!5)
+
+(declare-fun evalLazyConQ2!7 (LazyConQ!5) ConQ!6)
+
+(assert (=> b!39 (= e!41 (firstUnevaluated!3 (rear!5 (evalLazyConQ2!7 l!2)) st!3))))
+
+(declare-fun b!40 () Bool)
+
+(declare-fun e!42 () LazyConQ!5)
+
+(assert (=> b!40 (= e!42 e!41)))
+
+(assert (=> b!40 (= b!39 (is-Spine!5 (evalLazyConQ2!7 l!2)))))
+
+(declare-fun b!41 () Bool)
+
+(assert (=> b!40 (or (not b!39) (not b!41))))
+
+(assert (=> b!40 (or b!39 b!41)))
+
+(assert (=> b!41 (= e!41 l!2)))
+
+(declare-fun b!42 () Bool)
+
+(assert (=> b!42 (= e!42 l!2)))
+
+(declare-fun lt!14 () LazyConQ!5)
+
+(declare-fun isTip!5 (ConQ!6) Bool)
+
+(assert (=> start!13 (and (not (isTip!5 (evalLazyConQ2!7 lt!14))) (member lt!14 st!3))))
+
+(assert (=> start!13 (= lt!14 e!42)))
+
+(assert (=> start!13 (= b!40 (member l!2 st!3))))
+
+(assert (=> start!13 (or (not b!40) (not b!42))))
+
+(assert (=> start!13 (or b!40 b!42)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index e6b0a59fc..939b0d22c 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -61,7 +61,9 @@ TESTS =	\
 	mix-simp.smt2 \
 	mix-coeff.smt2 \
 	mix-match.smt2 \
-	ari056.smt2
+	ari056.smt2 \
+	ext-ex-deq-trigger.smt2 \
+	matching-lia-1arg.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2 b/test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2
new file mode 100644
index 000000000..f6f96fe02
--- /dev/null
+++ b/test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2
@@ -0,0 +1,26 @@
+; COMMAND-LINE: --relational-triggers
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-sort U 0)
+
+(declare-const k U)
+(declare-const ff U) 
+(declare-const ffk U)
+(declare-fun fun1 (Int) Int)
+(declare-fun fun2 (Int) Int)
+(declare-fun c (U U) U)
+(declare-fun app (U Int) Int)
+
+(assert (forall ((f U) (g U)) (=> (forall ((x Int)) (= (app f x) (app g x))) (= f g))  ))
+
+(assert (forall ((x Int)) (= (app ff x) (+ (fun1 x) (fun2 x)))))
+(assert (forall ((x Int)) (= (app ffk x) (+ (fun1 (app k x)) (fun2 (app k x))))))
+
+(assert (forall ((f U) (g U) (x Int)) (= (app (c f g) x) (app f (app g x)))))
+
+(assert (not (= (c ff k) ffk)))
+
+(check-sat)
+
diff --git a/test/regress/regress0/quantifiers/matching-lia-1arg.smt2 b/test/regress/regress0/quantifiers/matching-lia-1arg.smt2
new file mode 100644
index 000000000..aaf9b2c1f
--- /dev/null
+++ b/test/regress/regress0/quantifiers/matching-lia-1arg.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --purify-triggers
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(declare-fun P (Int) Bool)
+(assert (forall ((x Int)) (P (* 2 x))))
+(assert (not (P 38)))
+(check-sat)
+
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index a1f91a6ce..71ca64aea 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -45,7 +45,8 @@ TESTS = commutative.sy \
         sygus-dt.sy \
         dt-no-syntax.sy \
         list-head-x.sy \
-        clock-inc-tuple.sy
+        clock-inc-tuple.sy \
+        dt-test-ns.sy
 
 # sygus tests currently taking too long for make regress
 EXTRA_DIST = $(TESTS) \
diff --git a/test/regress/regress0/sygus/dt-test-ns.sy b/test/regress/regress0/sygus/dt-test-ns.sy
new file mode 100644
index 000000000..ed17f4ff2
--- /dev/null
+++ b/test/regress/regress0/sygus/dt-test-ns.sy
@@ -0,0 +1,14 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si --no-dump-synth
+(set-logic LIA)
+
+(declare-datatypes () ((List (cons (head Int) (tail List)) (nil))))
+
+(synth-fun f ((x Int)) List)
+
+(declare-var x Int)
+
+(constraint (is-cons (f x)))
+(constraint (and (= (head (f x)) x) (= (head (f x)) (+ 5 (head (tail (f x)))))))
+(check-synth)
+