Merge remote-tracking branch 'origin/master'

31 files changed, 1363 insertions, 654 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 66487e4a4..be3df349a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -85,6 +85,7 @@
 #include "theory/quantifiers/macros.h"
 #include "theory/quantifiers/fun_def_process.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/options.h"
 #include "theory/datatypes/options.h"
 #include "theory/strings/theory_strings_preprocess.h"
@@ -1375,9 +1376,6 @@ void SmtEngine::setDefaults() {
     if( !options::eMatching.wasSetByUser() ){
       options::eMatching.set( options::fmfInstEngine() );
     }
-    if( !options::quantConflictFind.wasSetByUser() ){
-      options::quantConflictFind.set( false );
-    }
     if( ! options::instWhenMode.wasSetByUser()){
       //instantiate only on last call
       if( options::eMatching() ){
@@ -1431,6 +1429,9 @@ void SmtEngine::setDefaults() {
     if( !options::macrosQuant.wasSetByUser()) {
       options::macrosQuant.set( false );
     }
+    if( !options::cbqiPreRegInst.wasSetByUser()) {
+      options::cbqiPreRegInst.set( true );
+    }
   }
 
   //cbqi options
@@ -1440,7 +1441,7 @@ void SmtEngine::setDefaults() {
       options::cbqi2.set( true );
     }
   }
-  if( options::recurseCbqi() || options::cbqi2() ){
+  if( options::cbqi2() ){
     options::cbqi.set( true );
   }
   if( options::cbqi2() ){
@@ -3179,6 +3180,13 @@ void SmtEnginePrivate::processAssertions() {
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
+  if( options::ceGuidedInst() ){
+    //register sygus conjecture pre-rewrite (motivated by solution reconstruction)
+    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+      d_smt.d_theoryEngine->getQuantifiersEngine()->getCegInstantiation()->preregisterAssertion( d_assertions[i] );
+    }
+  }
+  
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
       !d_smt.d_logic.isPure(THEORY_BV)) {
     throw ModalException("Eager bit-blasting does not currently support theory combination. "
@@ -4402,6 +4410,7 @@ void SmtEngine::printSynthSolution( std::ostream& out ) {
 vector<Expr> SmtEngine::getAssertions() throw(ModalException) {
   SmtScope smts(this);
   finalOptionsAreSet();
+  doPendingPops();
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << GetAssertionsCommand();
   }
diff --git a/src/theory/bv/bitblast_strategies_template.h b/src/theory/bv/bitblast_strategies_template.h
index 62c92c0a8..0990c2f29 100644
--- a/src/theory/bv/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast_strategies_template.h
@@ -536,8 +536,8 @@ void DefaultUdivBB (TNode node, std::vector<T>& q, TBitblaster<T>* bb) {
   T b_is_0 = mkAnd(iszero); 
   
   for (unsigned i = 0; i < q.size(); ++i) {
-    q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]);
-    r[i] = mkIte(b_is_0, mkTrue<T>(), r[i]);
+    q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]); // a udiv 0 is 11..11
+    r[i] = mkIte(b_is_0, a[i], r[i]);        // a urem 0 is a
   }
 
   // cache the remainder in case we need it later
@@ -564,8 +564,8 @@ void DefaultUremBB (TNode node, std::vector<T>& rem, TBitblaster<T>* bb) {
   T b_is_0 = mkAnd(iszero); 
   
   for (unsigned i = 0; i < q.size(); ++i) {
-    q[i] = mkIte(b_is_0, a[i], q[i]);
-    rem[i] = mkIte(b_is_0, a[i], rem[i]);
+    q[i] = mkIte(b_is_0, mkTrue<T>(), q[i]); // a udiv 0 is 11..11
+    rem[i] = mkIte(b_is_0, a[i], rem[i]);    // a urem 0 is a
   }
 
   // cache the quotient in case we need it later
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 96b205bb1..e6e3120f5 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -684,16 +684,19 @@ void AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) {
     }
   }
 
+  NodeSet leaf_vars;
   Debug("bitvector-model") << "Substitutions:\n";
   for (unsigned i = 0; i < variables.size(); ++i) {
     TNode current = variables[i];
     TNode subst = Rewriter::rewrite(d_modelMap->apply(current));
     Debug("bitvector-model") << "   " << current << " => " << subst << "\n";
     values[i] = subst;
+    utils::collectVariables(subst, leaf_vars);
   }
 
   Debug("bitvector-model") << "Model:\n";
-  for (BVQuickCheck::vars_iterator it = d_quickSolver->beginVars(); it != d_quickSolver->endVars(); ++it) {
+
+  for (NodeSet::const_iterator it = leaf_vars.begin(); it != leaf_vars.end(); ++it) {
     TNode var = *it;
     Node value = d_quickSolver->getVarValue(var, true);
     Assert (!value.isNull() || !fullModel);
@@ -712,7 +715,7 @@ void AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) {
     TNode subst = Rewriter::rewrite(d_modelMap->apply(current));
     Debug("bitvector-model") << "AlgebraicSolver:   " << variables[i] << " => " << subst << "\n"; 
     // Doesn't have to be constant as it may be irrelevant
-    // Assert (subst.getKind() == kind::CONST_BITVECTOR); 
+    Assert (subst.getKind() == kind::CONST_BITVECTOR); 
     model->assertEquality(variables[i], subst, true);
   }
 
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 13c31463b..6ae0ffb71 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -36,6 +36,7 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
     d_equalityEngine(d_notify, c, "theory::bv::TheoryBV", true),
     d_slicer(new Slicer()),
     d_isComplete(c, true),
+    d_lemmaThreshold(16),
     d_useSlicer(false),
     d_preregisterCalled(false),
     d_checkCalled(false),
@@ -276,16 +277,28 @@ void CoreSolver::buildModel() {
           for (unsigned j = i + 1; j < representatives.size(); ++j) {
             TNode a = representatives[i];
             TNode b = representatives[j];
+            if (a.getKind() == kind::CONST_BITVECTOR &&
+                b.getKind() == kind::CONST_BITVECTOR) {
+              Assert (a != b);
+              continue;
+            }
             if (utils::getSize(a) == utils::getSize(b)) {
               equalities.push_back(utils::mkNode(kind::EQUAL, a, b));
             }
           }
         }
+        // better off letting the SAT solver split on values
+        if (equalities.size() > d_lemmaThreshold) {
+          d_isComplete = false;
+          return;
+        }
+
         Node lemma = utils::mkOr(equalities);
         d_bv->lemma(lemma);
         Debug("bv-core") << "  lemma: " << lemma << "\n";
         return;
       }
+    
       Debug("bv-core-model") << "   " << repr << " => " << val <<"\n" ;
       constants.insert(val);
       d_modelValues[repr] = val;
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 5b9c54095..0ff193b41 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -74,9 +74,10 @@ class CoreSolver : public SubtheorySolver {
 
   Slicer* d_slicer;
   context::CDO<bool> d_isComplete;
+  unsigned d_lemmaThreshold;
   
   /** Used to ensure that the core slicer is used properly*/
-  bool d_useSlicer; 
+  bool d_useSlicer;
   bool d_preregisterCalled;
   bool d_checkCalled;
   
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index eca9f12ab..3f076bd4c 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -187,7 +187,8 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
   TNodeSet::iterator it = d_variables.begin();
   for (; it!= d_variables.end(); ++it) {
     TNode var = *it;
-    if (d_bv->isLeaf(var) || isSharedTerm(var))  {
+    if (d_bv->isLeaf(var) || isSharedTerm(var) ||
+        (var.isVar() && var.getType().isBoolean()))  {
       // only shared terms could not have been bit-blasted
       Assert (hasBBTerm(var) || isSharedTerm(var));
       
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 824dc5b92..d2025b1b8 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -100,3 +100,18 @@ uint64_t CVC4::theory::bv::utils::numNodes(TNode node, NodeSet& seen) {
   seen.insert(node);
   return size;
 }
+
+
+
+void CVC4::theory::bv::utils::collectVariables(TNode node, NodeSet& vars) {
+  if (vars.find(node) != vars.end())
+    return;
+
+  if (Theory::isLeafOf(node, THEORY_BV) && node.getKind() != kind::CONST_BITVECTOR) {
+    vars.insert(node);
+    return;
+  }
+  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+    collectVariables(node[i], vars);
+  }
+}
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index a8b6887e5..ba8074fbb 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -513,6 +513,8 @@ typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
 
 uint64_t numNodes(TNode node, NodeSet& seen);
 
+void collectVariables(TNode node, NodeSet& vars);
+
 }
 }
 }
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 371f27c95..e0a4dc7d8 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1414,11 +1414,15 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
     Node eqc = it->first;
     const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype();
     if( dt.isCodatatype() ){
+      //until models are implemented for codatatypes
+      throw Exception("Models for codatatypes are not supported in this version.");
+      /*
       std::map< Node, Node > vmap;
       std::vector< Node > fv;
       Node v = getCodatatypesValue( it->first, eqc_cons, eqc_mu, vmap, fv );
       Trace("dt-cmi-cdt") << "  EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << ", const = " << v.isConst() << std::endl;
       //m->assertEquality( eqc, v, true );
+      */
     }
   }
 }
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index e10ba0fef..0bc5bb008 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -29,18 +29,18 @@ using namespace std;
 
 namespace CVC4 {
 
-CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){
+CegConjecture::CegConjecture( QuantifiersEngine * qe, context::Context* c ) : d_qe( qe ), d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){
   d_refine_count = 0;
-  d_ceg_si = new CegConjectureSingleInv( this );
+  d_ceg_si = new CegConjectureSingleInv( qe, this );
 }
 
-void CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
+void CegConjecture::assign( Node q ) {
   Assert( d_quant.isNull() );
   Assert( q.getKind()==FORALL );
   d_assert_quant = q;
   //register with single invocation if applicable
-  if( qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) && options::cegqiSingleInv() ){
-    d_ceg_si->initialize( qe, q );
+  if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) && options::cegqiSingleInv() ){
+    d_ceg_si->initialize( q );
     if( q!=d_ceg_si->d_quant ){
       //Node red_lem = NodeManager::currentNM()->mkNode( OR, q.negate(), d_cegqi_si->d_quant );
       //may have rewritten quantified formula (for invariant synthesis)
@@ -53,9 +53,9 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
   }
   Trace("cegqi") << "Base quantified fm is : " << q << std::endl;
   //construct base instantiation
-  d_base_inst = Rewriter::rewrite( qe->getInstantiation( q, d_candidates ) );
+  d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, d_candidates ) );
   Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl;
-  if( qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){
+  if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){
     CegInstantiation::collectDisjuncts( d_base_inst, d_base_disj );
     Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl;
     //store the inner variables for each disjunct
@@ -70,7 +70,7 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
       }
     }
     d_syntax_guided = true;
-  }else if( qe->getTermDatabase()->isQAttrSynthesis( d_assert_quant ) ){
+  }else if( d_qe->getTermDatabase()->isQAttrSynthesis( d_assert_quant ) ){
     d_syntax_guided = false;
   }else{
     Assert( false );
@@ -87,16 +87,17 @@ void CegConjecture::initializeGuard( QuantifiersEngine * qe ){
     if( !d_syntax_guided ){
       //add immediate lemma
       Node lem = NodeManager::currentNM()->mkNode( OR, d_guard.negate(), d_base_inst.negate() );
-      Trace("cegqi") << "Add candidate lemma : " << lem << std::endl;
+      Trace("cegqi-lemma") << "Add candidate lemma : " << lem << std::endl;
       qe->getOutputChannel().lemma( lem );
     }else if( d_ceg_si ){
-      Node lem = d_ceg_si->getSingleInvLemma( d_guard );
-      if( !lem.isNull() ){
-        Trace("cegqi") << "Add single invocation lemma : " << lem << std::endl;
-        qe->getOutputChannel().lemma( lem );
+      std::vector< Node > lems;
+      d_ceg_si->getSingleInvLemma( d_guard, lems );
+      for( unsigned i=0; i<lems.size(); i++ ){
+        Trace("cegqi-lemma") << "Add single invocation lemma " << i << " : " << lems[i] << std::endl;
+        qe->getOutputChannel().lemma( lems[i] );
         if( Trace.isOn("cegqi-debug") ){
-          lem = Rewriter::rewrite( lem );
-          Trace("cegqi-debug") << "...rewritten : " << lem << std::endl;
+          Node rlem = Rewriter::rewrite( lems[i] );
+          Trace("cegqi-debug") << "...rewritten : " << rlem << std::endl;
         }
       }
     }
@@ -149,8 +150,12 @@ bool CegConjecture::needsCheck() {
   return d_active && !d_infeasible && ( !isSingleInvocation() || d_ceg_si->needsCheck() );
 }
 
+void CegConjecture::preregisterConjecture( Node q ) {
+  d_ceg_si->preregisterConjecture( q );
+}
+
 CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){
-  d_conj = new CegConjecture( qe->getSatContext() );
+  d_conj = new CegConjecture( qe, qe->getSatContext() );
   d_last_inst_si = false;
 }
 
@@ -178,7 +183,7 @@ void CegInstantiation::registerQuantifier( Node q ) {
   if( d_quantEngine->getOwner( q )==this ){
     if( !d_conj->isAssigned() ){
       Trace("cegqi") << "Register conjecture : " << q << std::endl;
-      d_conj->assign( d_quantEngine, q );
+      d_conj->assign( q );
 
       //fairness
       if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
@@ -279,7 +284,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
         if( !lems.empty() ){
           d_last_inst_si = true;
           for( unsigned j=0; j<lems.size(); j++ ){
-            Trace("cegqi-lemma") << "Single invocation lemma : " << lems[j] << std::endl;
+            Trace("cegqi-lemma") << "Single invocation instantiation lemma : " << lems[j] << std::endl;
             d_quantEngine->addLemma( lems[j] );
           }
           d_statistics.d_cegqi_si_lemmas += lems.size();
@@ -591,6 +596,24 @@ void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) {
   }
 }
 
+void CegInstantiation::preregisterAssertion( Node n ) {
+  //check if it sygus conjecture
+  if( n.getKind()==FORALL ){
+    if( n.getNumChildren()==3 ){
+      for( unsigned i=0; i<n[2].getNumChildren(); i++ ){
+        if( n[2][i].getKind()==INST_ATTRIBUTE ){
+          Node avar = n[2][i][0];
+          if( avar.getAttribute(SygusAttribute()) ){
+            //this is a sygus conjecture 
+            Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl;
+            d_conj->preregisterConjecture( n );
+          }
+        }
+      }
+    }
+  }
+}
+
 CegInstantiation::Statistics::Statistics():
   d_cegqi_lemmas_ce("CegInstantiation::cegqi_lemmas_ce", 0),
   d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0),
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index af3a19d62..8aa2e2c26 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -29,8 +29,10 @@ namespace quantifiers {
 
 /** a synthesis conjecture */
 class CegConjecture {
+private:
+  QuantifiersEngine * d_qe;
 public:
-  CegConjecture( context::Context* c );
+  CegConjecture( QuantifiersEngine * qe, context::Context* c );
   /** is conjecture active */
   context::CDO< bool > d_active;
   /** is conjecture infeasible */
@@ -65,7 +67,7 @@ public:
   /** refine count */
   unsigned d_refine_count;
   /** assign */
-  void assign( QuantifiersEngine * qe, Node q );
+  void assign( Node q );
   /** is assigned */
   bool isAssigned() { return !d_quant.isNull(); }
   /** current extential quantifeirs whose couterexamples we must refine */
@@ -87,6 +89,8 @@ public:  //for fairness
   bool isSingleInvocation();
   /** needs check */
   bool needsCheck();
+  /** preregister conjecture */
+  void preregisterConjecture( Node q );
 };
 
 
@@ -137,6 +141,8 @@ public:
   void printSynthSolution( std::ostream& out );
   /** collect disjuncts */
   static void collectDisjuncts( Node n, std::vector< Node >& ex );
+  /** preregister assertion (before rewrite) */
+  void preregisterAssertion( Node n );
 public:
   class Statistics {
   public:
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 17d85eb9b..19cf9b008 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -45,14 +45,21 @@ bool CegqiOutputSingleInv::addLemma( Node n ) {
 }
 
 
-CegConjectureSingleInv::CegConjectureSingleInv( CegConjecture * p ) : d_parent( p ){
-  d_sol = NULL;
-  d_c_inst_match_trie = NULL;
-  d_cinst = NULL;
+CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p ) : d_qe( qe ), d_parent( p ){
   d_has_ites = true;
+  if( options::incrementalSolving() ){
+    d_c_inst_match_trie = new inst::CDInstMatchTrie( qe->getUserContext() );
+  }else{
+    d_c_inst_match_trie = NULL;
+  }
+  CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this );
+  //  third and fourth arguments set to (false,false) until we have solution reconstruction for delta and infinity
+  d_cinst = new CegInstantiator( qe, cosi, false, false );
+
+  d_sol = new CegConjectureSingleInvSol( qe );
 }
 
-Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) {
+void CegConjectureSingleInv::getSingleInvLemma( Node guard, std::vector< Node >& lems ) {
   if( !d_single_inv.isNull() ) {
     d_single_inv_var.clear();
     d_single_inv_sk.clear();
@@ -73,30 +80,16 @@ Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) {
     inst = TermDb::simpleNegate( inst );
     Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl;
 
-    //initialize the instantiator for this
-    if( !d_single_inv_sk.empty() ){
-      CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this );
-      //  third and fourth arguments set to (false,false) until we have solution reconstruction for delta and infinity
-      d_cinst = new CegInstantiator( d_qe, cosi, false, false );
-      d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
-    }else{
-      d_cinst = NULL;
-    }
-
-    return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst );
-  }else{
-    return Node::null();
+    //register with the instantiator
+    Node ginst = NodeManager::currentNM()->mkNode( OR, guard.negate(), inst );
+    lems.push_back( ginst );
+    d_cinst->registerCounterexampleLemma( lems, d_single_inv_sk );
   }
 }
 
-void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
+void CegConjectureSingleInv::initialize( Node q ) {
   //initialize data
-  d_sol = new CegConjectureSingleInvSol( qe );
-  d_qe = qe;
   d_quant = q;
-  if( options::incrementalSolving() ){
-    d_c_inst_match_trie = new inst::CDInstMatchTrie( qe->getUserContext() );
-  }
   //process
   Trace("cegqi-si") << "Initialize cegqi-si for " << q << std::endl;
   // conj -> conj*
@@ -457,63 +450,9 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
       exit( 0 );
     }
   }else{
-    if( options::cegqiSingleInvPreRegInst() && d_single_inv.getKind()==FORALL ){
-      Trace("cegqi-si-presolve") << "Check " << d_single_inv << std::endl;
-      //at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing
-      std::vector< Node > vars;
-      std::map< Node, std::vector< Node > > teq;
-      for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
-        vars.push_back( d_single_inv[0][i] );
-        teq[d_single_inv[0][i]].clear();
-      }
-      collectPresolveEqTerms( d_single_inv[1], teq );
-      std::vector< Node > terms;
-      std::vector< Node > conj;
-      getPresolveEqConjuncts( vars, terms, teq, d_single_inv, conj );
-
-      if( !conj.empty() ){
-        Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
-        Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() );
-        lem = NodeManager::currentNM()->mkNode( OR, g, lem );
-        d_qe->getOutputChannel().lemma( lem, false, true );
-      }
-    }
-  }
-}
-
-void CegConjectureSingleInv::collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ) {
-  if( n.getKind()==EQUAL ){
-    for( unsigned i=0; i<2; i++ ){
-      std::map< Node, std::vector< Node > >::iterator it = teq.find( n[i] );
-      if( it!=teq.end() ){
-        Node nn = n[ i==0 ? 1 : 0 ];
-        if( std::find( it->second.begin(), it->second.end(), nn )==it->second.end() ){
-          it->second.push_back( nn );
-          Trace("cegqi-si-presolve") << "  - " << n[i] << " = " << nn << std::endl;
-        }
-      }
-    }
-  }
-  for( unsigned i=0; i<n.getNumChildren(); i++ ){
-    collectPresolveEqTerms( n[i], teq );
-  }
-}
-
-void CegConjectureSingleInv::getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms,
-                                                     std::map< Node, std::vector< Node > >& teq, Node f, std::vector< Node >& conj ) {
-  if( conj.size()<1000 ){
-    if( terms.size()==f[0].getNumChildren() ){
-      Node c = f[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
-      conj.push_back( c );
-    }else{
-      unsigned i = terms.size();
-      Node v = f[0][i];
-      terms.push_back( Node::null() );
-      for( unsigned j=0; j<teq[v].size(); j++ ){
-        terms[i] = teq[v][j];
-        getPresolveEqConjuncts( vars, terms, teq, f, conj );
-      }
-      terms.pop_back();
+    if( options::cbqiPreRegInst() && d_single_inv.getKind()==FORALL ){
+      //just invoke the presolve now
+      d_cinst->presolve( d_single_inv );
     }
   }
 }
@@ -719,10 +658,7 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs ){
   }else{
     Trace("cegqi-engine") << siss.str() << std::endl;
     Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() );
-    Node delta = d_qe->getTermDatabase()->getVtsDelta( false, false );
-    Node inf = d_qe->getTermDatabase()->getVtsInfinity( false, false );
-    if( ( !delta.isNull() && TermDb::containsTerm( lem, delta ) ) || 
-        ( !inf.isNull() && TermDb::containsTerm( lem, inf ) ) ){
+    if( d_qe->getTermDatabase()->containsVtsTerm( lem ) ){
       Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl;
       lem = d_qe->getTermDatabase()->rewriteVtsSymbols( lem );
     }
@@ -749,7 +685,7 @@ bool CegConjectureSingleInv::addLemma( Node n ) {
 }
 
 void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
-  if( !d_single_inv.isNull() && d_cinst!=NULL ) {
+  if( !d_single_inv.isNull() ) {
     d_curr_lemmas.clear();
     //call check for instantiator
     d_cinst->check();
@@ -870,6 +806,7 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec
   //reconstruct the solution into sygus if necessary
   reconstructed = 0;
   if( options::cegqiSingleInvReconstruct() && !dt.getSygusAllowAll() && !stn.isNull() ){
+    d_sol->preregisterConjecture( d_orig_conjecture );
     d_sygus_solution = d_sol->reconstructSolution( s, stn, reconstructed );
     if( reconstructed==1 ){
       Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << d_sygus_solution << std::endl;
@@ -923,5 +860,8 @@ bool CegConjectureSingleInv::needsCheck() {
   return true;
 }
 
+void CegConjectureSingleInv::preregisterConjecture( Node q ) {
+  d_orig_conjecture = q;
+}
 
 }
\ No newline at end of file
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index 2c955db5d..e814df110 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -84,6 +84,8 @@ private:
   //lemmas produced
   inst::InstMatchTrie d_inst_match_trie;
   inst::CDInstMatchTrie * d_c_inst_match_trie;
+  //original conjecture 
+  Node d_orig_conjecture;
   // solution
   std::vector< Node > d_varList;
   Node d_orig_solution;
@@ -103,7 +105,7 @@ private:
   // add lemma
   bool addLemma( Node lem );
 public:
-  CegConjectureSingleInv( CegConjecture * p );
+  CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p );
   // original conjecture
   Node d_quant;
   // single invocation version of quant
@@ -113,10 +115,10 @@ public:
   std::map< Node, Node > d_trans_post;
   std::map< Node, std::vector< Node > > d_prog_templ_vars;
 public:
-  //get the single invocation lemma
-  Node getSingleInvLemma( Node guard );
+  //get the single invocation lemma(s)
+  void getSingleInvLemma( Node guard, std::vector< Node >& lems );
   //initialize
-  void initialize( QuantifiersEngine * qe, Node q );
+  void initialize( Node q );
   //check
   void check( std::vector< Node >& lems );
   //get solution
@@ -129,6 +131,8 @@ public:
   bool isSingleInvocation() { return !d_single_inv.isNull(); }
   //needs check
   bool needsCheck();
+  /** preregister conjecture */
+  void preregisterConjecture( Node q );
 };
 
 }
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
index 413fd9ba2..8fd935368 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
@@ -618,9 +618,27 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st
 }
 
 
-
-
-
+void CegConjectureSingleInvSol::preregisterConjecture( Node q ) {
+  Trace("csi-sol") << "Preregister conjecture : " << q << std::endl;
+  Node n = q;
+  if( n.getKind()==FORALL ){
+    n = n[1];
+  }
+  if( n.getKind()==EXISTS ){
+    if( n[0].getNumChildren()==d_varList.size() ){
+      std::vector< Node > evars;
+      for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
+        evars.push_back( n[0][i] );
+      }
+      n = n[1].substitute( evars.begin(), evars.end(), d_varList.begin(), d_varList.end() );
+    }else{
+      Trace("csi-sol") << "Not the same number of variables, return." << std::endl;
+      return;
+    }
+  }
+  Trace("csi-sol") << "Preregister node for solution reconstruction : " << n << std::endl;
+  registerEquivalentTerms( n );
+}
 
 Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int& reconstructed ) {
   Trace("csi-rcons") << "Solution (pre-reconstruction) is : " << sol << std::endl;
@@ -1054,6 +1072,7 @@ void CegConjectureSingleInvSol::setReconstructed( int id, Node n ) {
 }
 
 void CegConjectureSingleInvSol::getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv ) {
+  Assert( n.getKind()!=k ); //?
   if( k==AND || k==OR ){
     equiv.push_back( NodeManager::currentNM()->mkNode( k, n, n ) );
     equiv.push_back( NodeManager::currentNM()->mkNode( k, n, NodeManager::currentNM()->mkConst( k==AND ) ) );
@@ -1108,7 +1127,68 @@ void CegConjectureSingleInvSol::getEquivalentTerms( Kind k, Node n, std::vector<
       nn = Rewriter::rewrite( nn );
       equiv.push_back( NodeManager::currentNM()->mkNode( MINUS, NodeManager::currentNM()->mkConst( Rational(0) ), nn ) );
     }
-  }  
+  }
+  //inequalities
+  if( k==GEQ || k==LEQ || k==LT || k==GT || k==NOT ){
+    Node atom = n.getKind()==NOT ? n[0] : n;
+    bool pol = n.getKind()!=NOT;
+    Kind ak = atom.getKind();
+    if( ( ak==GEQ || ak==LEQ || ak==LT || ak==GT ) && ( pol || k!=NOT ) ){
+      Node t1 = atom[0];
+      Node t2 = atom[1];
+      if( !pol ){
+        ak = ak==GEQ ? LT : ( ak==LEQ ? GT : ( ak==LT ? GEQ : LEQ ) );
+      }
+      if( k==NOT ){
+        equiv.push_back( NodeManager::currentNM()->mkNode( ak==GEQ ? LT : ( ak==LEQ ? GT : ( ak==LT ? GEQ : LEQ ) ), t1, t2 ).negate() );
+      }else if( k==ak ){
+        equiv.push_back( NodeManager::currentNM()->mkNode( k, t1, t2 ) );
+      }else if( (k==GEQ || k==LEQ)==(ak==GEQ || ak==LEQ) ){
+        equiv.push_back( NodeManager::currentNM()->mkNode( k, t2, t1 ) );
+      }else if( t1.getType().isInteger() && t2.getType().isInteger() ){
+        if( (k==GEQ || k==GT)!=(ak==GEQ || ak==GT) ){
+          Node ts = t1;
+          t1 = t2;
+          t2 = ts;
+          ak = ak==GEQ ? LEQ : ( ak==LEQ ? GEQ : ( ak==LT ? GT : LT ) );
+        }
+        t2 = NodeManager::currentNM()->mkNode( PLUS, t2, NodeManager::currentNM()->mkConst( Rational( (ak==GT || ak==LEQ) ? 1 : -1 ) ) );
+        t2 = Rewriter::rewrite( t2 );
+        equiv.push_back( NodeManager::currentNM()->mkNode( k, t1, t2 ) );
+      }
+    }
+  }
+
+  //based on eqt cache
+  std::map< Node, Node >::iterator itet = d_eqt_rep.find( n );
+  if( itet!=d_eqt_rep.end() ){
+    Node rn = itet->second;
+    for( unsigned i=0; i<d_eqt_eqc[rn].size(); i++ ){
+      if( d_eqt_eqc[rn][i]!=n && d_eqt_eqc[rn][i].getKind()==k ){
+        if( std::find( equiv.begin(), equiv.end(), d_eqt_eqc[rn][i] )==equiv.end() ){
+          equiv.push_back( d_eqt_eqc[rn][i] );
+        }
+      }
+    }
+  }
 }
-  
+
+void CegConjectureSingleInvSol::registerEquivalentTerms( Node n ) {
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    registerEquivalentTerms( n[i] );
+  }
+  Node rn = Rewriter::rewrite( n );
+  if( rn!=n ){
+    Trace("csi-equiv") << "  eq terms : " << n << " " << rn << std::endl;
+    d_eqt_rep[n] = rn;
+    d_eqt_rep[rn] = rn;
+    if( std::find( d_eqt_eqc[rn].begin(), d_eqt_eqc[rn].end(), rn )==d_eqt_eqc[rn].end() ){
+      d_eqt_eqc[rn].push_back( rn );
+    }
+    if( std::find( d_eqt_eqc[rn].begin(), d_eqt_eqc[rn].end(), n )==d_eqt_eqc[rn].end() ){
+      d_eqt_eqc[rn].push_back( n );
+    }
+  }
+}
+
 }
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.h b/src/theory/quantifiers/ce_guided_single_inv_sol.h
index 1d84986b4..adcc7bf85 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.h
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.h
@@ -65,6 +65,10 @@ private:
 
   std::map< int, std::vector< int > > d_eqc;
   std::map< int, int > d_rep;
+  
+  //equivalent terms
+  std::map< Node, Node > d_eqt_rep;
+  std::map< Node, std::vector< Node > > d_eqt_eqc;
 
   //cache when reconstructing solutions
   std::vector< int > d_tmp_fail;
@@ -80,8 +84,11 @@ private:
   void setReconstructed( int id, Node n );
   //get equivalent terms to n with top symbol k
   void getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv );
+  //register equivalent terms
+  void registerEquivalentTerms( Node n );
 public:
   Node reconstructSolution( Node sol, TypeNode stn, int& reconstructed );
+  void preregisterConjecture( Node q );
 public:
   CegConjectureSingleInvSol( QuantifiersEngine * qe );
 };
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index dcbb79a35..073cba525 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -9,7 +9,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Implementation of cbqi instantiation strategies
+ ** \brief Implementation of counterexample-guided quantifier instantiation strategies
  **/
 
 #include "theory/quantifiers/inst_strategy_cbqi.h"
@@ -20,6 +20,7 @@
 #include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "util/ite_removal.h"
 
 using namespace std;
 using namespace CVC4;
@@ -28,13 +29,11 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::arith;
-using namespace CVC4::theory::datatypes;
 
 #define ARITH_INSTANTIATOR_USE_MINUS_DELTA
 //#define MBP_STRICT_ASSERTIONS
 
 
-
 CegInstantiator::CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta, bool use_vts_inf ) :
 d_qe( qe ), d_out( out ), d_use_vts_delta( use_vts_delta ), d_use_vts_inf( use_vts_inf ){
   d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
@@ -65,28 +64,35 @@ void CegInstantiator::computeProgVars( Node n ){
 }
 
 bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars,
-                                        std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node theta,
-                                        unsigned i, unsigned effort ){
+                                        std::vector< Node >& coeff, std::vector< int >& btyp,
+                                        std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort ){
   if( i==d_vars.size() ){
-    return addInstantiationCoeff( subs, vars, coeff, has_coeff, 0 );
+    return addInstantiationCoeff( subs, vars, coeff, btyp, has_coeff, 0 );
   }else{
-    eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
     std::map< Node, std::map< Node, bool > > subs_proc;
     //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]];
     Node pv = d_vars[i];
     TypeNode pvtn = pv.getType();
+    Trace("cbqi-inst-debug") << "[Find instantiation for " << pv << "]" << std::endl;
+    Node pv_value;
+    if( options::cbqiModel() ){
+      pv_value = d_qe->getModel()->getValue( pv );
+      Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
+    }
 
     //if in effort=2, we must choose at least one model value
     if( (i+1)<d_vars.size() || effort!=2 ){
+
       //[1] easy case : pv is in the equivalence class as another term not containing pv
-      if( ee->hasTerm( pv ) ){
-        //std::vector< Node > eqc_sk;
-        Node pvr = ee->getRepresentative( pv );
-        eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee );
-        while( !eqc_i.isFinished() ){
-          Node n = *eqc_i;
+      Trace("cbqi-inst-debug") << "[1] try based on equivalence class." << std::endl;
+      std::map< Node, Node >::iterator itr = d_curr_rep.find( pv );
+      if( itr!=d_curr_rep.end() ){
+        std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( itr->second );
+        Assert( it_eqc!=d_curr_eqc.end() );
+        for( unsigned k=0; k<it_eqc->second.size(); k++ ){
+          Node n = it_eqc->second[k];
           if( n!=pv ){
-            Trace("cbqi-inst-debug") << "[1] " << i << "...try based on equal term " << n << std::endl;
+            Trace("cbqi-inst-debug") << "..[1] " << i << "...try based on equal term " << n << std::endl;
             //compute d_subs_fv, which program variables are contained in n
             computeProgVars( n );
             //must be an eligible term
@@ -108,136 +114,123 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
               if( proc ){
                 //try the substitution
                 subs_proc[ns][pv_coeff] = true;
-                if( addInstantiationInc( ns, pv, pv_coeff, subs, vars, coeff, has_coeff, theta, i, effort ) ){
+                if( addInstantiationInc( ns, pv, pv_coeff, 0, subs, vars, coeff, btyp, has_coeff, theta, i, effort ) ){
                   return true;
                 }
               }
             }
-            //record this as skolem
-            //if( n.getKind()==SKOLEM ){
-            //  eqc_sk.push_back( n );
-            //}
           }
-          ++eqc_i;
         }
       }
 
       //[2] : we can solve an equality for pv
       ///iterate over equivalence classes to find cases where we can solve for the variable
-      Node vts_inf = d_qe->getTermDatabase()->getVtsInfinity( false, false );
       if( pvtn.isInteger() || pvtn.isReal() ){
-        eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
-        while( !eqcs_i.isFinished() ){
-          Node r = *eqcs_i;
-          TypeNode rtn = r.getType();
-          if( rtn.isInteger() || rtn.isReal() ){
-            std::vector< Node > lhs;
-            std::vector< bool > lhs_v;
-            std::vector< Node > lhs_coeff;
-            eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
-            while( !eqc_i.isFinished() ){
-              Node n = *eqc_i;
-              computeProgVars( n );
-              //must be an eligible term
-              if( d_inelig.find( n )==d_inelig.end() ){
-                Node ns;
-                Node pv_coeff;
-                if( !d_prog_var[n].empty() ){
-                  ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff );
-                  if( !ns.isNull() ){
-                    computeProgVars( ns );
-                  }
-                }else{
-                  ns = n;
-                }
+        Trace("cbqi-inst-debug") << "[2] try based on solving in arithmetic equivalence class." << std::endl;
+        for( unsigned k=0; k<d_curr_arith_eqc.size(); k++ ){
+          Node r = d_curr_arith_eqc[k];
+          std::vector< Node > lhs;
+          std::vector< bool > lhs_v;
+          std::vector< Node > lhs_coeff;
+          std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( r );
+          Assert( it_eqc!=d_curr_eqc.end() );
+          for( unsigned kk=0; kk<it_eqc->second.size(); kk++ ){
+            Node n = it_eqc->second[kk];
+            Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl;
+            //compute the variables in n
+            computeProgVars( n );
+            //must be an eligible term
+            if( d_inelig.find( n )==d_inelig.end() ){
+              Node ns;
+              Node pv_coeff;
+              if( !d_prog_var[n].empty() ){
+                ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff );
                 if( !ns.isNull() ){
-                  bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end();
-                  for( unsigned j=0; j<lhs.size(); j++ ){
-                    //if this term or the another has pv in it, try to solve for it
-                    if( hasVar || lhs_v[j] ){
-                      Trace("cbqi-inst-debug") << "[2] " << i << "...try based on equality " << lhs[j] << " = " << ns << std::endl;
-                      Node eq_lhs = lhs[j];
-                      Node eq_rhs = ns;
-                      //make the same coefficient
-                      if( pv_coeff!=lhs_coeff[j] ){
-                        if( !pv_coeff.isNull() ){
-                          Trace("cbqi-inst-debug") << "...mult lhs by " << pv_coeff << std::endl;
-                          eq_lhs = NodeManager::currentNM()->mkNode( MULT, pv_coeff, eq_lhs );
-                          eq_lhs = Rewriter::rewrite( eq_lhs );
-                        }
-                        if( !lhs_coeff[j].isNull() ){
-                          Trace("cbqi-inst-debug") << "...mult rhs by " << lhs_coeff[j] << std::endl;
-                          eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff[j], eq_rhs );
-                          eq_rhs = Rewriter::rewrite( eq_rhs );
-                        }
+                  computeProgVars( ns );
+                }
+              }else{
+                ns = n;
+              }
+              if( !ns.isNull() ){
+                bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end();
+                for( unsigned j=0; j<lhs.size(); j++ ){
+                  //if this term or the another has pv in it, try to solve for it
+                  if( hasVar || lhs_v[j] ){
+                    Trace("cbqi-inst-debug") << "..[2] " << i << "...try based on equality " << lhs[j] << " = " << ns << std::endl;
+                    Node eq_lhs = lhs[j];
+                    Node eq_rhs = ns;
+                    //make the same coefficient
+                    if( pv_coeff!=lhs_coeff[j] ){
+                      if( !pv_coeff.isNull() ){
+                        Trace("cbqi-inst-debug") << "...mult lhs by " << pv_coeff << std::endl;
+                        eq_lhs = NodeManager::currentNM()->mkNode( MULT, pv_coeff, eq_lhs );
+                        eq_lhs = Rewriter::rewrite( eq_lhs );
+                      }
+                      if( !lhs_coeff[j].isNull() ){
+                        Trace("cbqi-inst-debug") << "...mult rhs by " << lhs_coeff[j] << std::endl;
+                        eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff[j], eq_rhs );
+                        eq_rhs = Rewriter::rewrite( eq_rhs );
+                      }
+                    }
+                    Node eq = eq_lhs.eqNode( eq_rhs );
+                    eq = Rewriter::rewrite( eq );
+                    //cannot contain infinity?
+                    //if( !d_qe->getTermDatabase()->containsVtsInfinity( eq ) ){
+                    Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl;
+                    std::map< Node, Node > msum;
+                    if( QuantArith::getMonomialSumLit( eq, msum ) ){
+                      if( Trace.isOn("cbqi-inst-debug") ){
+                        Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl;
+                        QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" );
+                        Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl;
                       }
-                      Node eq = eq_lhs.eqNode( eq_rhs );
-                      eq = Rewriter::rewrite( eq );
-                      //cannot contain infinity
-                      if( vts_inf.isNull() || !TermDb::containsTerm( eq, vts_inf ) ){
-                        Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl;
-                        std::map< Node, Node > msum;
-                        if( QuantArith::getMonomialSumLit( eq, msum ) ){
-                          if( Trace.isOn("cbqi-inst-debug") ){
-                            Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl;
-                            QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" );
-                            Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl;
+                      Node veq;
+                      if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){
+                        Trace("cbqi-inst-debug") << "...isolated equality " << veq << "." << std::endl;
+                        Node veq_c;
+                        if( veq[0]!=pv ){
+                          Node veq_v;
+                          if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){
+                            Assert( veq_v==pv );
                           }
-                          Node veq;
-                          if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){
-                            Trace("cbqi-inst-debug") << "...isolated equality " << veq << "." << std::endl;
-                            Node veq_c;
-                            if( veq[0]!=pv ){
-                              Node veq_v;
-                              if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){
-                                Assert( veq_v==pv );
-                              }
-                            }
-                            Node val = veq[1];
-                            //eliminate coefficient if real
-                            if( !pvtn.isInteger() && !veq_c.isNull() ){
-                              val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) );
-                              val = Rewriter::rewrite( val );
-                              veq_c = Node::null();
-                            }
-                            if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
-                              subs_proc[val][veq_c] = true;
-                              if( addInstantiationInc( val, pv, veq_c, subs, vars, coeff, has_coeff, theta, i, effort ) ){
-                                return true;
-                              }
-                            }
+                        }
+                        Node val = veq[1];
+                        if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
+                          subs_proc[val][veq_c] = true;
+                          if( addInstantiationInc( val, pv, veq_c, 0, subs, vars, coeff, btyp, has_coeff, theta, i, effort ) ){
+                            return true;
                           }
                         }
                       }
                     }
                   }
-                  lhs.push_back( ns );
-                  lhs_v.push_back( hasVar );
-                  lhs_coeff.push_back( pv_coeff );
                 }
+                lhs.push_back( ns );
+                lhs_v.push_back( hasVar );
+                lhs_coeff.push_back( pv_coeff );
               }
-              ++eqc_i;
             }
           }
-          ++eqcs_i;
         }
       }
 
       //[3] directly look at assertions
+      Trace("cbqi-inst-debug") << "[3] try based on assertions." << std::endl;
+      Node vts_sym[2];
+      vts_sym[0] = d_qe->getTermDatabase()->getVtsInfinity( pvtn, false, false );
+      vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta( false, false );
       std::vector< Node > mbp_bounds[2];
       std::vector< Node > mbp_coeff[2];
-      std::vector< bool > mbp_strict[2];
+      std::vector< Node > mbp_vts_coeff[2][2];
       std::vector< Node > mbp_lit[2];
       unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2;
       for( unsigned r=0; r<rmax; r++ ){
         TheoryId tid = r==0 ? Theory::theoryOf( pv ) : Theory::theoryOf( pv.getType() );
-        Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid );
-        Trace("cbqi-inst-debug2") << "Theory of " << pv << " (r=" << r << ") is " << tid << std::endl;
-        if (theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid)) {
-          Trace("cbqi-inst-debug2") << "Look at assertions of " << tid << std::endl;
-          context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
-          for (unsigned j = 0; it != it_end; ++ it, ++j) {
-            Node lit = (*it).assertion;
+        Trace("cbqi-inst-debug2") << "  look at assertions of " << tid << std::endl;
+        std::map< TheoryId, std::vector< Node > >::iterator ita = d_curr_asserts.find( tid );
+        if( ita!=d_curr_asserts.end() ){
+          for (unsigned j = 0; j<ita->second.size(); j++) {
+            Node lit = ita->second[j];
             Trace("cbqi-inst-debug2") << "  look at " << lit << std::endl;
             Node atom = lit.getKind()==NOT ? lit[0] : lit;
             bool pol = lit.getKind()!=NOT;
@@ -272,96 +265,153 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                 //if it contains pv, not infinity
                 if( !atom_lhs.isNull() && d_prog_var[atom_lhs].find( pv )!=d_prog_var[atom_lhs].end() ){
                   Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs );
-                  //cannot contain infinity
-                  if( vts_inf.isNull() || !TermDb::containsTerm( atom_lhs, vts_inf ) ){
-                    Trace("cbqi-inst-debug") << "[3] From assertion : " << atom << ", pol = " << pol << std::endl;
-                    Trace("cbqi-inst-debug") << "       substituted : " << satom << ", pol = " << pol << std::endl;
-                    std::map< Node, Node > msum;
-                    if( QuantArith::getMonomialSumLit( satom, msum ) ){
-                      if( Trace.isOn("cbqi-inst-debug") ){
-                        Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl;
-                        QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" );
-                        Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl;
-                      }
-                      Node vatom;
-                      //isolate pv in the inequality
-                      int ires = QuantArith::isolate( pv, msum, vatom, atom.getKind(), true );
-                      if( ires!=0 ){
-                        Trace("cbqi-inst-debug") << "...isolated atom " << vatom << "." << std::endl;
-                        Node val = vatom[ ires==1 ? 1 : 0 ];
-                        Node pvm = vatom[ ires==1 ? 0 : 1 ];
-                        //get monomial
-                        Node veq_c;
-                        if( pvm!=pv ){
-                          Node veq_v;
-                          if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){
-                            Assert( veq_v==pv );
+                  //cannot contain infinity?
+                  //if( !d_qe->getTermDatabase()->containsVtsInfinity( atom_lhs ) ){
+                  Trace("cbqi-inst-debug") << "..[3] From assertion : " << atom << ", pol = " << pol << std::endl;
+                  Trace("cbqi-inst-debug") << "         substituted : " << satom << ", pol = " << pol << std::endl;
+                  std::map< Node, Node > msum;
+                  if( QuantArith::getMonomialSumLit( satom, msum ) ){
+                    if( Trace.isOn("cbqi-inst-debug") ){
+                      Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl;
+                      QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" );
+                    }
+                    //get the coefficient of infinity and remove it from msum
+                    Node vts_coeff[2];
+                    for( unsigned t=0; t<2; t++ ){
+                      if( !vts_sym[t].isNull() ){
+                        std::map< Node, Node >::iterator itminf = msum.find( vts_sym[t] );
+                        if( itminf!=msum.end() ){
+                          vts_coeff[t] = itminf->second;
+                          if( vts_coeff[t].isNull() ){
+                            vts_coeff[t] = NodeManager::currentNM()->mkConst( Rational( 1 ) );
                           }
+                          //negate if coefficient on variable is positive
+                          std::map< Node, Node >::iterator itv = msum.find( pv );
+                          if( itv!=msum.end() ){
+                            //multiply by the coefficient we will isolate for
+                            if( itv->second.isNull() ){
+                              vts_coeff[t] = QuantArith::negate(vts_coeff[t]);
+                            }else{
+                              if( !pvtn.isInteger() ){
+                                vts_coeff[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) / itv->second.getConst<Rational>() ), vts_coeff[t] );
+                                vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] );
+                              }else if( itv->second.getConst<Rational>().sgn()==1 ){
+                                vts_coeff[t] = QuantArith::negate(vts_coeff[t]);
+                              }
+                            }
+                          }
+                          Trace("cbqi-inst-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl;
+                          msum.erase( vts_sym[t] );
                         }
-                        //eliminate coefficient if real
-                        if( !pvtn.isInteger() && !veq_c.isNull() ){
-                          val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) );
-                          val = Rewriter::rewrite( val );
-                          veq_c = Node::null();
+                      }
+                    }
+
+                    Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl;
+                    Node vatom;
+                    //isolate pv in the inequality
+                    int ires = QuantArith::isolate( pv, msum, vatom, atom.getKind(), true );
+                    if( ires!=0 ){
+                      Trace("cbqi-inst-debug") << "...isolated atom " << vatom << "." << std::endl;
+                      Node val = vatom[ ires==1 ? 1 : 0 ];
+                      Node pvm = vatom[ ires==1 ? 0 : 1 ];
+                      //get monomial
+                      Node veq_c;
+                      if( pvm!=pv ){
+                        Node veq_v;
+                        if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){
+                          Assert( veq_v==pv );
                         }
+                      }
 
-                        //disequalities are both strict upper and lower bounds
-                        unsigned rmax = atom.getKind()==GEQ ? 1 : 2;
-                        for( unsigned r=0; r<rmax; r++ ){
-                          int uires = ires;
-                          Node uval = val;
-                          if( atom.getKind()==GEQ ){
-                            //push negation downwards
-                            if( !pol ){
-                              uires = -ires;
-                              if( pvtn.isInteger() ){
-                                uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
-                                uval = Rewriter::rewrite( uval );
-                              }else{
-                                Assert( pvtn.isReal() );
-                                //now is strict inequality
-                                uires = uires*2;
-                              }
-                            }
-                          }else{
-                            Assert( atom.getKind()==EQUAL && !pol );
+                      //disequalities are either strict upper or lower bounds
+                      unsigned rmax = ( atom.getKind()==GEQ && options::cbqiModel() ) ? 1 : 2;
+                      for( unsigned r=0; r<rmax; r++ ){
+                        int uires = ires;
+                        Node uval = val;
+                        if( atom.getKind()==GEQ ){
+                          //push negation downwards
+                          if( !pol ){
+                            uires = -ires;
                             if( pvtn.isInteger() ){
-                              uires = r==0 ? -1 : 1;
                               uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
                               uval = Rewriter::rewrite( uval );
                             }else{
                               Assert( pvtn.isReal() );
-                              uires = r==0 ? -2 : 2;
+                              //now is strict inequality
+                              uires = uires*2;
                             }
                           }
-                          Trace("cbqi-bound-inf") << "From " << lit << ", got : ";
-                          if( !veq_c.isNull() ){
-                            Trace("cbqi-bound-inf") << veq_c << " * ";
-                          }
-                          Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl;
+                        }else{
+                          bool is_upper = ( r==0 );
                           if( options::cbqiModel() ){
-                            //just store bounds, will choose based on tighest bound
-                            unsigned index = uires>0 ? 0 : 1;
-                            mbp_bounds[index].push_back( uval );
-                            mbp_coeff[index].push_back( veq_c );
-                            mbp_strict[index].push_back( uires==2 || uires==-2 );
-                            mbp_lit[index].push_back( lit );
-                          }else{
-                            //take into account delta
-                            if( uires==2 || uires==-2 ){
-                              if( d_use_vts_delta ){
-                                Node delta = d_qe->getTermDatabase()->getVtsDelta();
-                                uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta );
-                                uval = Rewriter::rewrite( uval );
+                            // disequality is a disjunction : only consider the bound in the direction of the model
+                            //first check if there is an infinity...
+                            if( !vts_coeff[0].isNull() ){
+                              //coefficient or val won't make a difference, just compare with zero
+                              Trace("cbqi-inst-debug") << "Disequality : check infinity polarity " << vts_coeff[0] << std::endl;
+                              Assert( vts_coeff[0].isConst() );
+                              is_upper = ( vts_coeff[0].getConst<Rational>().sgn()==1 );
+                            }else{
+                              Node rhs_value = d_qe->getModel()->getValue( val );
+                              Node lhs_value = pv_value;
+                              if( !veq_c.isNull() ){
+                                lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c );
+                                lhs_value = Rewriter::rewrite( lhs_value );
                               }
+                              Trace("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl;
+                              Assert( lhs_value!=rhs_value );
+                              Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value );
+                              cmp = Rewriter::rewrite( cmp );
+                              Assert( cmp.isConst() );
+                              is_upper = ( cmp!=d_true );
                             }
-                            if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
-                              subs_proc[uval][veq_c] = true;
-                              if( addInstantiationInc( uval, pv, veq_c, subs, vars, coeff, has_coeff, theta, i, effort ) ){
-                                return true;
-                              }
+                          }
+                          Assert( atom.getKind()==EQUAL && !pol );
+                          if( pvtn.isInteger() ){
+                            uires = is_upper ? -1 : 1;
+                            uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
+                            uval = Rewriter::rewrite( uval );
+                          }else{
+                            Assert( pvtn.isReal() );
+                            uires = is_upper ? -2 : 2;
+                          }
+                        }
+                        Trace("cbqi-bound-inf") << "From " << lit << ", got : ";
+                        if( !veq_c.isNull() ){
+                          Trace("cbqi-bound-inf") << veq_c << " * ";
+                        }
+                        Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl;
+                        //take into account delta
+                        if( d_use_vts_delta && ( uires==2 || uires==-2 ) ){
+                          if( options::cbqiModel() ){
+                            Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) );
+                            if( vts_coeff[1].isNull() ){
+                              vts_coeff[1] = delta_coeff;
                             }else{
-                              Trace("cbqi-inst-debug") << "...already processed." << std::endl;
+                              vts_coeff[1] = NodeManager::currentNM()->mkNode( PLUS, vts_coeff[1], delta_coeff );
+                              vts_coeff[1] = Rewriter::rewrite( vts_coeff[1] );
+                            }
+                          }else{
+                            Node delta = d_qe->getTermDatabase()->getVtsDelta();
+                            uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta );
+                            uval = Rewriter::rewrite( uval );
+                          }
+                        }
+                        if( options::cbqiModel() ){
+                          //just store bounds, will choose based on tighest bound
+                          unsigned index = uires>0 ? 0 : 1;
+                          mbp_bounds[index].push_back( uval );
+                          mbp_coeff[index].push_back( veq_c );
+                          for( unsigned t=0; t<2; t++ ){
+                            mbp_vts_coeff[index][t].push_back( vts_coeff[t] );
+                          }
+                          mbp_lit[index].push_back( lit );
+                        }else{
+                          //try this bound
+                          if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
+                            subs_proc[uval][veq_c] = true;
+                            if( addInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, subs, vars, coeff, btyp, has_coeff, theta, i, effort ) ){
+                              return true;
                             }
                           }
                         }
@@ -376,83 +426,160 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
       }
       if( options::cbqiModel() ){
         if( pvtn.isInteger() || pvtn.isReal() ){
+          bool use_inf = d_use_vts_inf && ( pvtn.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() );
           bool upper_first = false;
+          if( options::cbqiMinBounds() ){
+            upper_first = mbp_bounds[1].size()<mbp_bounds[0].size();
+          }
           unsigned best_used[2];
-          std::vector< Node > t_values[2];
-          Node pv_value = d_qe->getModel()->getValue( pv );
-          Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
+          std::vector< Node > t_values[3];
           //try optimal bounds
           for( unsigned r=0; r<2; r++ ){
             int rr = upper_first ? (1-r) : r;
             if( mbp_bounds[rr].empty() ){
-              /*
-              if( d_use_vts_inf ){
+              if( use_inf ){
                 Trace("cbqi-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << pvtn << ")" << std::endl;
                 //no bounds, we do +- infinity
-                Node val = d_qe->getTermDatabase()->getVtsInfinity();
+                Node val = d_qe->getTermDatabase()->getVtsInfinity( pvtn );
+                //TODO : rho value for infinity?
                 if( rr==0 ){
                   val = NodeManager::currentNM()->mkNode( UMINUS, val );
                   val = Rewriter::rewrite( val );
                 }
-                if( addInstantiationInc( val, pv, Node::null(), subs, vars, coeff, has_coeff, theta, i, effort ) ){
+                if( addInstantiationInc( val, pv, Node::null(), 0, subs, vars, coeff, btyp, has_coeff, theta, i, effort ) ){
                   return true;
                 }
               }
-              */
             }else{
               Trace("cbqi-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << pvtn << ") : " << std::endl;
               int best = -1;
-              Node best_bound_value;
+              Node best_bound_value[3];
               for( unsigned j=0; j<mbp_bounds[rr].size(); j++ ){
-                Node t_value = d_qe->getModel()->getValue( mbp_bounds[rr][j] );
-                t_values[rr].push_back( t_value );
-                Trace("cbqi-bound2") << "...M( " << mbp_bounds[rr][j] << " ) = " << t_value << std::endl;
-                Node value = t_value;
-                Trace("cbqi-bound") << "  " << j << ": " << mbp_bounds[rr][j];
-                if( !mbp_coeff[rr][j].isNull() ){
-                  Trace("cbqi-bound") << " (div " << mbp_coeff[rr][j] << ")";
-                  Assert( mbp_coeff[rr][j].isConst() );
-                  value = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / mbp_coeff[rr][j].getConst<Rational>() ), value );
-                  value = Rewriter::rewrite( value );
-                }
-                if( mbp_strict[rr][j] ){
-                  Trace("cbqi-bound") << " (strict)";
+                Node value[3];
+                if( Trace.isOn("cbqi-bound") ){
+                  Assert( !mbp_bounds[rr][j].isNull() );
+                  Trace("cbqi-bound") << "  " << j << ": " << mbp_bounds[rr][j];
+                  if( !mbp_vts_coeff[rr][0][j].isNull() ){
+                    Trace("cbqi-bound") << " (+ " << mbp_vts_coeff[rr][0][j] << " * INF)";
+                  }
+                  if( !mbp_vts_coeff[rr][1][j].isNull() ){
+                    Trace("cbqi-bound") << " (+ " << mbp_vts_coeff[rr][1][j] << " * DELTA)";
+                  }
+                  if( !mbp_coeff[rr][j].isNull() ){
+                    Trace("cbqi-bound") << " (div " << mbp_coeff[rr][j] << ")";
+                  }
+                  Trace("cbqi-bound") << ", value = ";
                 }
-                Trace("cbqi-bound") << ", value = " << value << std::endl;
-                bool new_best = false;
-                if( best==-1 ){
-                  new_best = true;
-                }else{
-                  Kind k = rr==0 ? GEQ : LEQ;
-                  Node cmp_bound = NodeManager::currentNM()->mkNode( k, value, best_bound_value );
-                  cmp_bound = Rewriter::rewrite( cmp_bound );
-                  if( cmp_bound==d_true && ( !mbp_strict[rr][best] || mbp_strict[rr][j] ) ){
-                    new_best = true;
+                t_values[rr].push_back( Node::null() );
+                //check if it is better than the current best bound : lexicographic order infinite/finite/infinitesimal parts
+                bool new_best = true;
+                for( unsigned t=0; t<3; t++ ){
+                  //get the value
+                  if( t==0 ){
+                    value[0] = mbp_vts_coeff[rr][0][j];
+                    if( !value[0].isNull() ){
+                      Trace("cbqi-bound") << "( " << value[0] << " * INF ) + ";
+                    }else{
+                      value[0] = d_zero;
+                    }
+                  }else if( t==1 ){
+                    Node t_value = d_qe->getModel()->getValue( mbp_bounds[rr][j] );
+                    t_values[rr][j] = t_value;
+                    value[1] = t_value;
+                    Trace("cbqi-bound") << value[1];
+                  }else{
+                    value[2] = mbp_vts_coeff[rr][1][j];
+                    if( !value[2].isNull() ){
+                      Trace("cbqi-bound") << " + ( " << value[2] << " * DELTA )";
+                    }else{
+                      value[2] = d_zero;
+                    }
+                  }
+                  //multiply by coefficient
+                  if( value[t]!=d_zero && !mbp_coeff[rr][j].isNull() ){
+                    Assert( mbp_coeff[rr][j].isConst() );
+                    value[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / mbp_coeff[rr][j].getConst<Rational>() ), value[t] );
+                    value[t] = Rewriter::rewrite( value[t] );
+                  }
+                  //check if new best
+                  if( best!=-1 ){
+                    Assert( !value[t].isNull() && !best_bound_value[t].isNull() );
+                    if( value[t]!=best_bound_value[t] ){
+                      Kind k = rr==0 ? GEQ : LEQ;
+                      Node cmp_bound = NodeManager::currentNM()->mkNode( k, value[t], best_bound_value[t] );
+                      cmp_bound = Rewriter::rewrite( cmp_bound );
+                      if( cmp_bound!=d_true ){
+                        new_best = false;
+                        break;
+                      }
+                    }
                   }
                 }
+                Trace("cbqi-bound") << std::endl;
                 if( new_best ){
-                  best_bound_value = value;
+                  for( unsigned t=0; t<3; t++ ){
+                    best_bound_value[t] = value[t];
+                  }
                   best = j;
                 }
               }
               if( best!=-1 ){
-                Trace("cbqi-bound") << "...best bound is " << best << " : " << best_bound_value << std::endl;
+                Trace("cbqi-bound") << "...best bound is " << best << " : ";
+                if( best_bound_value[0]!=d_zero ){
+                  Trace("cbqi-bound") << "( " << best_bound_value[0] << " * INF ) + ";
+                }
+                Trace("cbqi-bound") << best_bound_value[1];
+                if( best_bound_value[2]!=d_zero ){
+                  Trace("cbqi-bound") << " + ( " << best_bound_value[2] << " * DELTA )";
+                }
+                Trace("cbqi-bound") << std::endl;
                 best_used[rr] = (unsigned)best;
-                Node val = getModelBasedProjectionValue( mbp_bounds[rr][best], mbp_strict[rr][best], rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta );
-                if( !val.isNull() && addInstantiationInc( val, pv, mbp_coeff[rr][best], subs, vars, coeff, has_coeff, theta, i, effort ) ){
+                Node val = mbp_bounds[rr][best];
+                val = getModelBasedProjectionValue( val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta,
+                                                    mbp_vts_coeff[rr][0][best], vts_sym[0], mbp_vts_coeff[rr][1][best], vts_sym[1] );
+                if( !val.isNull() ){
+                  if( subs_proc[val].find( mbp_coeff[rr][best] )==subs_proc[val].end() ){
+                    subs_proc[val][mbp_coeff[rr][best]] = true;
+                    if( addInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, subs, vars, coeff, btyp, has_coeff, theta, i, effort ) ){
+                      return true;
+                    }
+                  }
+                }
+              }
+            }
+          }
+          //if not using infinity, use model value of zero
+          if( !use_inf && mbp_bounds[0].empty() && mbp_bounds[1].empty() ){
+            Node val = d_zero;
+            Node c; //null (one) coefficient
+            val = getModelBasedProjectionValue( val, true, c, pv_value, d_zero, theta, Node::null(), vts_sym[0], Node::null(), vts_sym[1] );
+            if( !val.isNull() ){
+              if( subs_proc[val].find( c )==subs_proc[val].end() ){
+                subs_proc[val][c] = true;
+                if( addInstantiationInc( val, pv, c, 0, subs, vars, coeff, btyp, has_coeff, theta, i, effort ) ){
                   return true;
                 }
               }
             }
           }
-          //try non-optimal bounds (heuristic)
+#ifdef MBP_STRICT_ASSERTIONS
+          Assert( false );
+#endif
+          //try non-optimal bounds (heuristic, may help when nested quantification) ?
+          Trace("cbqi-bound") << "Try non-optimal bounds..." << std::endl;
           for( unsigned r=0; r<2; r++ ){
             int rr = upper_first ? (1-r) : r;
             for( unsigned j=0; j<mbp_bounds[rr].size(); j++ ){
               if( j!=best_used[rr] ){
-                Node val = getModelBasedProjectionValue( mbp_bounds[rr][j], mbp_strict[rr][j], rr==0, mbp_coeff[rr][j], pv_value, t_values[rr][j], theta );
-                if( !val.isNull() && addInstantiationInc( val, pv, mbp_coeff[rr][j], subs, vars, coeff, has_coeff, theta, i, effort ) ){
-                  return true;
+                Node val = getModelBasedProjectionValue( mbp_bounds[rr][j], rr==0, mbp_coeff[rr][j], pv_value, t_values[rr][j], theta,
+                                                         mbp_vts_coeff[rr][0][j], vts_sym[0], mbp_vts_coeff[rr][1][j], vts_sym[1] );
+                if( !val.isNull() ){
+                  if( subs_proc[val].find( mbp_coeff[rr][j] )==subs_proc[val].end() ){
+                    subs_proc[val][mbp_coeff[rr][j]] = true;
+                    if( addInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, subs, vars, coeff, btyp, has_coeff, theta, i, effort ) ){
+                      return true;
+                    }
+                  }
                 }
               }
             }
@@ -462,30 +589,33 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
     }
 
     //[4] resort to using value in model
-    if( effort>0 || ( pvtn.isBoolean() && ( (i+1)<d_vars.size() || effort!=2 ) ) ){
+    if( effort>0 || pvtn.isBoolean() ){
       Node mv = d_qe->getModel()->getValue( pv );
       Node pv_coeff_m;
       Trace("cbqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl;
       int new_effort = pvtn.isBoolean() ? effort : 1;
 #ifdef MBP_STRICT_ASSERTIONS
       //we only resort to values in the case of booleans
-      Assert( pvtn.isBoolean() );
+      Assert( ( pvtn.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() );
 #endif
-      return addInstantiationInc( mv, pv, pv_coeff_m, subs, vars, coeff, has_coeff, theta, i, new_effort );
-    }else{
-      return false;
+      if( addInstantiationInc( mv, pv, pv_coeff_m, 0, subs, vars, coeff, btyp, has_coeff, theta, i, new_effort ) ){
+        return true;
+      }
     }
+    Trace("cbqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl;
+    return false;
   }
 }
 
 
-bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, std::vector< Node >& subs, std::vector< Node >& vars,
-                                           std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort ) {
+bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, std::vector< Node >& subs, std::vector< Node >& vars,
+                                           std::vector< Node >& coeff, std::vector< int >& btyp, 
+                                           std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort ) {
   if( Trace.isOn("cbqi-inst") ){
-    for( unsigned i=0; i<subs.size(); i++ ){
+    for( unsigned j=0; j<subs.size(); j++ ){
       Trace("cbqi-inst") << " ";
     }
-    Trace("cbqi-inst") << "i: ";
+    Trace("cbqi-inst") << subs.size() << ": ";
     if( !pv_coeff.isNull() ){
       Trace("cbqi-inst") << pv_coeff << " * ";
     }
@@ -545,14 +675,10 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, std::
     subs.push_back( n );
     vars.push_back( pv );
     coeff.push_back( pv_coeff );
+    btyp.push_back( bt );
     if( !pv_coeff.isNull() ){
       has_coeff.push_back( pv );
     }
-    Trace("cbqi-inst-debug") << i << ": ";
-    if( !pv_coeff.isNull() ){
-      Trace("cbqi-inst-debug") << pv_coeff << "*";
-    }
-    Trace("cbqi-inst-debug") << pv << " -> " << n << std::endl;
     Node new_theta = theta;
     if( !pv_coeff.isNull() ){
       if( new_theta.isNull() ){
@@ -562,11 +688,12 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, std::
         new_theta = Rewriter::rewrite( new_theta );
       }
     }
-    success = addInstantiation( subs, vars, coeff, has_coeff, new_theta, i+1, effort );
+    success = addInstantiation( subs, vars, coeff, btyp, has_coeff, new_theta, i+1, effort );
     if( !success ){
       subs.pop_back();
       vars.pop_back();
       coeff.pop_back();
+      btyp.pop_back();
       if( !pv_coeff.isNull() ){
         has_coeff.pop_back();
       }
@@ -590,7 +717,7 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, std::
 }
 
 bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars,
-                                             std::vector< Node >& coeff, std::vector< Node >& has_coeff, unsigned j ) {
+                                             std::vector< Node >& coeff, std::vector< int >& btyp, std::vector< Node >& has_coeff, unsigned j ) {
   if( j==has_coeff.size() ){
     return addInstantiation( subs, vars );
   }else{
@@ -621,8 +748,9 @@ bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vec
         subs[index] = veq[1];
         if( !veq_c.isNull() ){
           subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c );
-          /*
-          if( subs_typ[index]>=1 && subs_typ[index]<=2 ){
+          Trace("cbqi-inst-debug") << "...bound type is : " << btyp[index] << std::endl;
+          //intger division rounding up if from a lower bound
+          if( btyp[index]==1 ){
             subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index],
               NodeManager::currentNM()->mkNode( ITE,
                 NodeManager::currentNM()->mkNode( EQUAL,
@@ -631,28 +759,11 @@ bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vec
                 d_zero, d_one )
             );
           }
-          */
         }
         Trace("cbqi-inst-debug") << "...normalize integers : " << subs[index] << std::endl;
-        if( addInstantiationCoeff( subs, vars, coeff, has_coeff, j+1 ) ){
+        if( addInstantiationCoeff( subs, vars, coeff, btyp, has_coeff, j+1 ) ){
           return true;
         }
-          //equalities are both upper and lower bounds
-          /*
-          if( subs_typ[index]==0 && !veq_c.isNull() ){
-            subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index],
-              NodeManager::currentNM()->mkNode( ITE,
-                NodeManager::currentNM()->mkNode( EQUAL,
-                  NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ),
-                  NodeManager::currentNM()->mkConst( Rational( 0 ) ) ),
-                NodeManager::currentNM()->mkConst( Rational( 0 ) ),
-                NodeManager::currentNM()->mkConst( Rational( 1 ) ) )
-            );
-            if( addInstantiationCoeff( subs, vars, coeff, has_coeff, j+1 ) ){
-              return true;
-            }
-          }
-          */
       }
     }
     subs[index] = prev;
@@ -671,7 +782,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
 
 
 Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars,
-                                                std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff ) {
+                                                 std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff ) {
   Assert( d_prog_var.find( n )!=d_prog_var.end() );
   Assert( n==Rewriter::rewrite( n ) );
   bool req_coeff = false;
@@ -752,21 +863,10 @@ Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std:
   }
 }
 
-Node CegInstantiator::getModelBasedProjectionValue( Node t, bool strict, bool isLower, Node c, Node me, Node mt, Node theta ) {
+Node CegInstantiator::getModelBasedProjectionValue( Node t, bool isLower, Node c, Node me, Node mt, Node theta,
+                                                    Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta ) {
   Node val = t;
   Trace("cbqi-bound2") << "Value : " << val << std::endl;
-  //take into account strictness
-  if( strict ){
-    if( !d_use_vts_delta ){
-      return Node::null();
-    }else{
-      Node delta = d_qe->getTermDatabase()->getVtsDelta();
-      Kind k = isLower ? PLUS : MINUS;
-      val = NodeManager::currentNM()->mkNode( k, val, delta );
-      val = Rewriter::rewrite( val );
-      Trace("cbqi-bound2") << "(after strict) : " << val << std::endl;
-    }
-  }
   //add rho value
   //get the value of c*e
   Node ceValue = me;
@@ -801,6 +901,19 @@ Node CegInstantiator::getModelBasedProjectionValue( Node t, bool strict, bool is
     val = Rewriter::rewrite( val );
     Trace("cbqi-bound2") << "(after rho) : " << val << std::endl;
   }
+  if( !inf_coeff.isNull() ){
+    Assert( !vts_inf.isNull() );
+    val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, vts_inf ) );
+    val = Rewriter::rewrite( val );
+  }
+  if( !delta_coeff.isNull() ){
+    //create delta here if necessary
+    if( vts_delta.isNull() ){
+      vts_delta = d_qe->getTermDatabase()->getVtsDelta();
+    }
+    val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, vts_delta ) );
+    val = Rewriter::rewrite( val );
+  }
   return val;
 }
 
@@ -809,14 +922,16 @@ bool CegInstantiator::check() {
     Trace("cegqi-engine") << "  CEGQI instantiator : wait until all ground theories are finished." << std::endl;
     return false;
   }
+  processAssertions();
   for( unsigned r=0; r<2; r++ ){
     std::vector< Node > subs;
     std::vector< Node > vars;
     std::vector< Node > coeff;
+    std::vector< int > btyp;
     std::vector< Node > has_coeff;
     Node theta;
     //try to add an instantiation
-    if( addInstantiation( subs, vars, coeff, has_coeff, theta, 0, r==0 ? 0 : 2 ) ){
+    if( addInstantiation( subs, vars, coeff, btyp, has_coeff, theta, 0, r==0 ? 0 : 2 ) ){
       return true;
     }
   }
@@ -824,6 +939,279 @@ bool CegInstantiator::check() {
   return false;
 }
 
+void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ) {
+  if( n.getKind()==FORALL || n.getKind()==EXISTS ){
+    //do nothing
+  }else{
+    if( n.getKind()==EQUAL ){
+      for( unsigned i=0; i<2; i++ ){
+        std::map< Node, std::vector< Node > >::iterator it = teq.find( n[i] );
+        if( it!=teq.end() ){
+          Node nn = n[ i==0 ? 1 : 0 ];
+          if( std::find( it->second.begin(), it->second.end(), nn )==it->second.end() ){
+            it->second.push_back( nn );
+            Trace("cbqi-presolve") << "  - " << n[i] << " = " << nn << std::endl;
+          }
+        }
+      }
+    }
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      collectPresolveEqTerms( n[i], teq );
+    }
+  }
+}
+
+void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms,
+                             std::map< Node, std::vector< Node > >& teq, Node f, std::vector< Node >& conj ) {
+  if( conj.size()<1000 ){
+    if( terms.size()==f[0].getNumChildren() ){
+      Node c = f[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+      conj.push_back( c );
+    }else{
+      unsigned i = terms.size();
+      Node v = f[0][i];
+      terms.push_back( Node::null() );
+      for( unsigned j=0; j<teq[v].size(); j++ ){
+        terms[i] = teq[v][j];
+        getPresolveEqConjuncts( vars, terms, teq, f, conj );
+      }
+      terms.pop_back();
+    }
+  }
+}
+
+void CegInstantiator::presolve( Node q ) {
+  Trace("cbqi-presolve") << "CBQI presolve " << q << std::endl;
+  //at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing
+  std::vector< Node > vars;
+  std::map< Node, std::vector< Node > > teq;
+  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+    vars.push_back( q[0][i] );
+    teq[q[0][i]].clear();
+  }
+  collectPresolveEqTerms( q[1], teq );
+  std::vector< Node > terms;
+  std::vector< Node > conj;
+  getPresolveEqConjuncts( vars, terms, teq, q, conj );
+
+  if( !conj.empty() ){
+    Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
+    Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() );
+    lem = NodeManager::currentNM()->mkNode( OR, g, lem );
+    Trace("cbqi-presolve-debug") << "Presolve lemma : " << lem << std::endl;
+    d_qe->getOutputChannel().lemma( lem, false, true );
+  }
+}
+
+void CegInstantiator::processAssertions() {
+  Trace("cbqi-proc") << "--- Process assertions, #var = " << d_vars.size() << ", #aux-var = " << d_aux_vars.size() << std::endl;
+  d_curr_asserts.clear();
+  d_curr_eqc.clear();
+  d_curr_rep.clear();
+  d_curr_arith_eqc.clear();
+
+  eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
+  //to eliminate identified illegal terms
+  std::map< Node, Node > aux_subs;
+
+  //for each variable
+  bool has_arith_var = false;
+  for( unsigned i=0; i<d_vars.size(); i++ ){
+    Node pv = d_vars[i];
+    TypeNode pvtn = pv.getType();
+    //collect current assertions
+    unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2;
+    for( unsigned r=0; r<rmax; r++ ){
+      TheoryId tid = r==0 ? Theory::theoryOf( pv ) : Theory::theoryOf( pv.getType() );
+      Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid );
+      Trace("cbqi-proc-debug") << "...theory of " << pv << " (r=" << r << ") is " << tid << std::endl;
+      if( d_curr_asserts.find( tid )==d_curr_asserts.end() ){
+        if (theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid)) {
+          Trace("cbqi-proc") << "Collect assertions from " << tid << std::endl;
+          d_curr_asserts[tid].clear();
+          //collect all assertions from theory
+          for( context::CDList<Assertion>::const_iterator it = theory->facts_begin(); it != theory->facts_end(); ++ it) {
+            Node lit = (*it).assertion;
+            d_curr_asserts[tid].push_back( lit );
+            Trace("cbqi-proc-debug") << "...add : " << lit << std::endl;
+            if( lit.getKind()==EQUAL ){
+              std::map< Node, std::map< Node, Node > >::iterator itae = d_aux_eq.find( lit );
+              if( itae!=d_aux_eq.end() ){
+                for( std::map< Node, Node >::iterator itae2 = itae->second.begin(); itae2 != itae->second.end(); ++itae2 ){
+                  aux_subs[ itae2->first ] = itae2->second;
+                  Trace("cbqi-proc") << "......add substitution : " << itae2->first << " -> " << itae2->second << std::endl;
+                }
+              }
+            }
+          }
+        }
+      }
+    }
+    //collect information about eqc
+    if( ee->hasTerm( pv ) ){
+      Node pvr = ee->getRepresentative( pv );
+      d_curr_rep[pv] = pvr;
+      if( d_curr_eqc.find( pvr )==d_curr_eqc.end() ){
+        Trace("cbqi-proc") << "Collect equivalence class " << pvr << std::endl;
+        eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee );
+        while( !eqc_i.isFinished() ){
+          d_curr_eqc[pvr].push_back( *eqc_i );
+          ++eqc_i;
+        }
+      }
+    }
+    //has arith var
+    if( pvtn.isInteger() || pvtn.isReal() ){
+      has_arith_var = true;
+    }
+  }
+  //must process all arithmetic eqc if any arithmetic variable
+  if( has_arith_var ){
+    Trace("cbqi-proc-debug") << "...collect arithmetic equivalence classes" << std::endl;
+    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
+    while( !eqcs_i.isFinished() ){
+      Node r = *eqcs_i;
+      TypeNode rtn = r.getType();
+      if( rtn.isInteger() || rtn.isReal() ){
+        Trace("cbqi-proc-debug") << "...arith eqc: " << r << std::endl;
+        d_curr_arith_eqc.push_back( r );
+        if( d_curr_eqc.find( r )==d_curr_eqc.end() ){
+          Trace("cbqi-proc") << "Collect equivalence class " << r << std::endl;
+          eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+          while( !eqc_i.isFinished() ){
+            d_curr_eqc[r].push_back( *eqc_i );
+            ++eqc_i;
+          }
+        }
+      }
+      ++eqcs_i;
+    }
+  }
+  //construct substitution from union find
+  std::vector< Node > subs_lhs;
+  std::vector< Node > subs_rhs;
+  for( unsigned i=0; i<d_aux_vars.size(); i++ ){
+    Node r = d_aux_vars[i];
+    std::map< Node, Node >::iterator it = aux_subs.find( r );
+    if( it!=aux_subs.end() ){
+      addToAuxVarSubstitution( subs_lhs, subs_rhs, r, it->second );
+    }else{
+      Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << r << "!!!" << std::endl;
+#ifdef MBP_STRICT_ASSERTIONS
+      Assert( false );
+#endif
+    }
+  }
+
+  //apply substitutions to everything, if necessary
+  if( !subs_lhs.empty() ){
+    Trace("cbqi-proc") << "Applying substitution : " << std::endl;
+    for( unsigned i=0; i<subs_lhs.size(); i++ ){
+      Trace("cbqi-proc") << "  " << subs_lhs[i] << " -> " << subs_rhs[i] << std::endl;
+    }
+
+    for( std::map< TheoryId, std::vector< Node > >::iterator it = d_curr_asserts.begin(); it != d_curr_asserts.end(); ++it ){
+      for( unsigned i=0; i<it->second.size(); i++ ){
+        Node lit = it->second[i];
+        lit = lit.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
+        lit = Rewriter::rewrite( lit );
+        it->second[i] = lit;
+      }
+    }
+    for( std::map< Node, std::vector< Node > >::iterator it = d_curr_eqc.begin(); it != d_curr_eqc.end(); ++it ){
+      for( unsigned i=0; i<it->second.size(); i++ ){
+        Node n = it->second[i];
+        n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
+        n = Rewriter::rewrite( n  );
+        it->second[i] = n;
+      }
+    }
+  }
+
+  //remove unecessary assertions
+  for( std::map< TheoryId, std::vector< Node > >::iterator it = d_curr_asserts.begin(); it != d_curr_asserts.end(); ++it ){
+    std::vector< Node > akeep;
+    for( unsigned i=0; i<it->second.size(); i++ ){
+      Node n = it->second[i];
+      //compute the variables in assertion
+      computeProgVars( n );
+      //must be an eligible term
+      if( d_inelig.find( n )==d_inelig.end() ){
+        //must contain at least one variable
+        if( !d_prog_var[n].empty() ){
+          Trace("cbqi-proc") << "...literal[" << it->first << "] : " << n << std::endl;
+          akeep.push_back( n );
+        }else{
+          Trace("cbqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains no relevant variables." << std::endl;
+        }
+      }else{
+        Trace("cbqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains ineligible terms." << std::endl;
+      }
+    }
+    it->second.clear();
+    it->second.insert( it->second.end(), akeep.begin(), akeep.end() );
+  }
+
+  //remove duplicate terms from eqc
+  for( std::map< Node, std::vector< Node > >::iterator it = d_curr_eqc.begin(); it != d_curr_eqc.end(); ++it ){
+    std::vector< Node > new_eqc;
+    for( unsigned i=0; i<it->second.size(); i++ ){
+      if( std::find( new_eqc.begin(), new_eqc.end(), it->second[i] )==new_eqc.end() ){
+        new_eqc.push_back( it->second[i] );
+      }
+    }
+    it->second.clear();
+    it->second.insert( it->second.end(), new_eqc.begin(), new_eqc.end() );
+  }
+}
+
+void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ) {
+  r = r.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
+
+  std::vector< Node > cl;
+  cl.push_back( l );
+  std::vector< Node > cr;
+  cr.push_back( r );
+  for( unsigned i=0; i<subs_lhs.size(); i++ ){
+    Node nr = subs_rhs[i].substitute( cl.begin(), cl.end(), cr.begin(), cr.end() );
+    nr = Rewriter::rewrite( nr );
+    subs_rhs[i] = nr;
+  }
+
+  subs_lhs.push_back( l );
+  subs_rhs.push_back( r );
+}
+
+void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
+  Assert( d_vars.empty() );
+  d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() );
+  IteSkolemMap iteSkolemMap;
+  d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap);
+  Assert( d_aux_vars.empty() );
+  for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) {
+    Trace("cbqi-debug") << "  Auxiliary var (from ITE) : " << i->first << std::endl;
+    d_aux_vars.push_back( i->first );
+  }
+  for( unsigned i=0; i<lems.size(); i++ ){
+    Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite)  " << i << " : " << lems[i] << std::endl;
+    Node rlem = lems[i];
+    rlem = Rewriter::rewrite( rlem );
+    Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl;
+    //record the literals that imply auxiliary variables to be equal to terms
+    if( lems[i].getKind()==ITE && rlem.getKind()==ITE ){
+      if( lems[i][1].getKind()==EQUAL && lems[i][2].getKind()==EQUAL && lems[i][1][0]==lems[i][2][0] ){
+        if( std::find( d_aux_vars.begin(), d_aux_vars.end(), lems[i][1][0] )!=d_aux_vars.end() ){
+          Node v = lems[i][1][0];
+          for( unsigned r=1; r<=2; r++ ){
+            d_aux_eq[rlem[r]][v] = lems[i][r][1];
+            Trace("cbqi-debug") << "  " << rlem[r] << " implies " << v << " = " << lems[i][r][1] << std::endl;
+          }
+        }
+      }
+    }
+    lems[i] = rlem;
+  }
+}
 
 //old implementation
 
@@ -1173,17 +1561,7 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
   if( e<1 ){
     return STATUS_UNFINISHED;
   }else if( e==1 ){
-    CegInstantiator * cinst;
-    std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( f );
-    if( it==d_cinst.end() ){
-      cinst = new CegInstantiator( d_quantEngine, d_out );
-      for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
-        cinst->d_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) );
-      }
-      d_cinst[f] = cinst;
-    }else{
-      cinst = it->second;
-    }
+    CegInstantiator * cinst = getInstantiator( f );
     Trace("inst-alg") << "-> Run cegqi for " << f << std::endl;
     d_curr_quant = f;
     bool addedLemma = cinst->check();
@@ -1192,23 +1570,22 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
   }else if( e==2 ){
     //minimize the free delta heuristically on demand
     if( d_check_vts_lemma_lc ){
+      d_check_vts_lemma_lc = false;
+      d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const );
+      d_small_const = Rewriter::rewrite( d_small_const );
+      //heuristic for now, until we know how to do nested quantification
       Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( true, false );
-      Node inf = d_quantEngine->getTermDatabase()->getVtsInfinity( true, false );
-      if( !delta.isNull() || !inf.isNull() ){
-        d_check_vts_lemma_lc = false;
-        d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const );
-        d_small_const = Rewriter::rewrite( d_small_const );
-        //heuristic for now, until we know how to do nested quantification
-        if( !delta.isNull() ){
-          Trace("cegqi") << "Delta lemma for " << d_small_const << std::endl;
-          Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const );
-          d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
-        }
-        if( !inf.isNull() ){
-          Trace("cegqi") << "Infinity lemma for " << d_small_const << std::endl;
-          Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf, NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) );
-          d_quantEngine->getOutputChannel().lemma( inf_lem_lb );
-        }
+      if( !delta.isNull() ){
+        Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl;
+        Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const );
+        d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
+      }
+      std::vector< Node > inf;
+      d_quantEngine->getTermDatabase()->getVtsTerms( inf, true, false, false );
+      for( unsigned i=0; i<inf.size(); i++ ){
+        Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl;
+        Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) );
+        d_quantEngine->getOutputChannel().lemma( inf_lem_lb );
       }
     }
   }
@@ -1217,31 +1594,8 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
 
 bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs ) {
   Assert( !d_curr_quant.isNull() );
-  /*
-  std::stringstream siss;
-  if( Trace.isOn("inst-cegqi") || Trace.isOn("inst-cegqi-debug") ){
-    for( unsigned j=0; j<d_single_inv_sk.size(); j++ ){
-      Node v = d_single_inv_map_to_prog[d_single_inv[0][j]];
-      siss << "    * " << v;
-      siss << " (" << d_single_inv_sk[j] << ")";
-      siss << " -> " << ( subs_typ[j]==9 ? "M:" : "") << subs[j] << std::endl;
-    }
-  }
-  */
-  //check if we need virtual term substitution (if used delta)
-  bool used_vts = false;
-  Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( false, false );
-  Node inf = d_quantEngine->getTermDatabase()->getVtsInfinity( false, false );
-  if( !delta.isNull() || !inf.isNull() ){
-    for( unsigned i=0; i<subs.size(); i++ ){
-      if( !delta.isNull() && TermDb::containsTerm( subs[i], delta ) ){
-        used_vts = true;
-      }
-      if( !inf.isNull() && TermDb::containsTerm( subs[i], inf ) ){
-        used_vts = true;
-      }
-    }
-  }
+  //check if we need virtual term substitution (if used delta or infinity)
+  bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false );
   return d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts );
 }
 
@@ -1258,15 +1612,28 @@ bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
   }
 }
 
+CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
+  std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( q );
+  if( it==d_cinst.end() ){
+    CegInstantiator * cinst = new CegInstantiator( d_quantEngine, d_out, true, true );
+    d_cinst[q] = cinst;
+    return cinst;
+  }else{
+   return it->second;
+  }
+}
 
+void InstStrategyCegqi::registerQuantifier( Node q ) {
+  if( options::cbqiPreRegInst() ){
+    //just get the instantiator
+    getInstantiator( q );
+  }
+}
 
-
-
-
-
-
-
-
-
-
-
+void InstStrategyCegqi::presolve() {
+  if( options::cbqiPreRegInst() ){
+    for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){
+      it->second->presolve( it->first );
+    }
+  }
+}
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 4f5049cd8..f882da110 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -9,14 +9,14 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief instantiator_arith_instantiator
+ ** \brief counterexample-guided quantifier instantiation
  **/
 
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__INST_STRATEGT_CBQI_H
-#define __CVC4__INST_STRATEGT_CBQI_H
+#ifndef __CVC4__INST_STRATEGY_CBQI_H
+#define __CVC4__INST_STRATEGY_CBQI_H
 
 #include "theory/quantifiers/instantiation_engine.h"
 #include "theory/arith/arithvar.h"
@@ -30,10 +30,6 @@ namespace arith {
   class TheoryArith;
 }
 
-namespace datatypes {
-  class TheoryDatatypes;
-}
-
 namespace quantifiers {
 
 class CegqiOutput
@@ -59,28 +55,46 @@ private:
   //program variable contains cache
   std::map< Node, std::map< Node, bool > > d_prog_var;
   std::map< Node, bool > d_inelig;
+  //current assertions
+  std::map< TheoryId, std::vector< Node > > d_curr_asserts;
+  std::map< Node, std::vector< Node > > d_curr_eqc;
+  std::map< Node, Node > d_curr_rep;
+  std::vector< Node > d_curr_arith_eqc;
+  //auxiliary variables
+  std::vector< Node > d_aux_vars;
+  //literals to equalities for aux vars
+  std::map< Node, std::map< Node, Node > > d_aux_eq;
+  //the CE variables
+  std::vector< Node > d_vars;
 private:
   //for adding instantiations during check
   void computeProgVars( Node n );
   // effort=0 : do not use model value, 1: use model value, 2: one must use model value
   bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars,
-                         std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node theta,
+                         std::vector< Node >& coeff, std::vector< int >& btyp, 
+                         std::vector< Node >& has_coeff, Node theta,
                          unsigned i, unsigned effort );
-  bool addInstantiationInc( Node n, Node pv, Node pv_coeff, std::vector< Node >& subs, std::vector< Node >& vars,
-                            std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort );
+  bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, std::vector< Node >& subs, std::vector< Node >& vars,
+                            std::vector< Node >& coeff, std::vector< int >& btyp, 
+                            std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort );
   bool addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars,
-                              std::vector< Node >& coeff, std::vector< Node >& has_coeff,
-                              unsigned j );
+                              std::vector< Node >& coeff, std::vector< int >& btyp, 
+                              std::vector< Node >& has_coeff, unsigned j );
   bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars );
   Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars,
                           std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff = true );
-  Node getModelBasedProjectionValue( Node t, bool strict, bool isLower, Node c, Node me, Node mt, Node theta );
+  Node getModelBasedProjectionValue( Node t, bool isLower, Node c, Node me, Node mt, Node theta, 
+                                     Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta );
+  void processAssertions();
+  void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r );
 public:
   CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true );
-  //the CE variables
-  std::vector< Node > d_vars;
   //check : add instantiations based on valuation of d_vars
   bool check();
+  //presolve for quantified formula
+  void presolve( Node q );
+  //register the counterexample lemma (stored in lems), modify vector 
+  void registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars );
 };
 
 class InstStrategySimplex : public InstStrategy{
@@ -159,6 +173,13 @@ public:
   bool addLemma( Node lem );
   /** identify */
   std::string identify() const { return std::string("Cegqi"); }
+
+  //get instantiator for quantifier
+  CegInstantiator * getInstantiator( Node q );
+  //register quantifier
+  void registerQuantifier( Node q );
+  //presolve
+  void presolve();
 };
 
 }
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index b686ddb3b..699208fba 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -76,6 +76,11 @@ void InstantiationEngine::finishInit(){
   }
 }
 
+void InstantiationEngine::presolve() {
+  for( unsigned i=0; i<d_instStrategies.size(); ++i ){
+    d_instStrategies[i]->presolve();
+  }
+}
 
 bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   unsigned lastWaiting = d_quantEngine->d_lemmas_waiting.size();
@@ -101,7 +106,26 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
           //add counterexample lemma
           lem = Rewriter::rewrite( lem );
           Trace("cbqi") << "Counterexample lemma : " << lem << std::endl;
-          d_quantEngine->addLemma( lem, false );
+
+          if( d_i_cegqi ){
+            //must register with the instantiator
+            //must explicitly remove ITEs so that we record dependencies
+            std::vector< Node > ce_vars;
+            for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
+              ce_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) );
+            }
+            std::vector< Node > lems;
+            lems.push_back( lem );
+            CegInstantiator * cinst = d_i_cegqi->getInstantiator( f );
+            cinst->registerCounterexampleLemma( lems, ce_vars );
+            for( unsigned i=0; i<lems.size(); i++ ){
+              Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i] << std::endl;
+              d_quantEngine->addLemma( lems[i], false );
+            }
+          }else{
+            Trace("cbqi-debug") << "Counterexample lemma  : " << lem << std::endl;
+            d_quantEngine->addLemma( lem, false );
+          }
           addedLemma = true;
         }
       }
@@ -250,6 +274,9 @@ bool InstantiationEngine::checkComplete() {
 
 void InstantiationEngine::registerQuantifier( Node f ){
   if( d_quantEngine->hasOwnership( f, this ) ){
+    for( unsigned i=0; i<d_instStrategies.size(); ++i ){
+      d_instStrategies[i]->registerQuantifier( f );
+    }
     //Notice() << "do cbqi " << f << " ? " << std::endl;
     if( options::cbqi() ){
       Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 44612a85c..1f321917b 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -43,12 +43,16 @@ protected:
 public:
   InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
   virtual ~InstStrategy(){}
+  /** presolve */
+  virtual void presolve() {}
   /** reset instantiation */
   virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
   /** process method, returns a status */
   virtual int process( Node f, Theory::Effort effort, int e ) = 0;
   /** identify */
   virtual std::string identify() const { return std::string("Unknown"); }
+  /** register quantifier */
+  virtual void registerQuantifier( Node q ) {}
 };/* class InstStrategy */
 
 class InstantiationEngine : public QuantifiersModule
@@ -96,7 +100,7 @@ public:
   ~InstantiationEngine();
   /** initialize */
   void finishInit();
-
+  void presolve();
   bool needsCheck( Theory::Effort e );
   unsigned needsModel( Theory::Effort e );
   void reset_round( Theory::Effort e );
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 48a9fdea2..ec71e5348 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -17,7 +17,8 @@ option miniscopeQuant --miniscope-quant bool :default true :read-write
 # ( forall x. P( x ) ) V Q
 option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write
  disable miniscope quantifiers for ground subformulas
-# Whether to prenex (nested universal) quantifiers
+option clauseSplit --clause-split bool :default true
+ apply clause splitting to quantified formulas
 option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToPrenexQuantMode :handler-include "theory/quantifiers/options_handlers.h"
  prenex mode for quantified formulas
 # Whether to variable-eliminate quantifiers.
@@ -37,11 +38,8 @@ option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default fal
 # Whether to CNF quantifier bodies
 # option cnfQuant --cnf-quant bool :default false
 #  apply CNF conversion to quantified formulas
-# Whether to NNF quantifier bodies
 option nnfQuant --nnf-quant bool :default true
  apply NNF conversion to quantified formulas
-option clauseSplit --clause-split bool :default true
- apply clause splitting to quantified formulas
 # Whether to pre-skolemize quantifier bodies.
 # For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
 #   forall x. P( x ) => f( S( x ) ) = x
@@ -51,10 +49,8 @@ option preSkolemQuantNested --pre-skolem-quant-nested bool :read-write :default
  apply skolemization to nested quantified formulass
 option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true
  apply skolemization to quantified formulas aggressively
-# Whether to perform agressive miniscoping
 option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
  perform aggressive miniscoping for quantifiers
-# Whether to CNF quantifier bodies
 option elimTautQuant --elim-taut-quant bool :default true
  eliminate tautological disjuncts of quantified formulas
  
@@ -212,8 +208,6 @@ option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true
   reconstruct solutions for single invocation conjectures in original grammar
 option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true
   include constants when reconstruct solutions for single invocation conjectures in original grammar
-option cegqiSingleInvPreRegInst --cegqi-si-prereg-inst bool :default true
-  preregister ground instantiations when single invocation
 option cegqiSingleInvAbort --cegqi-si-abort bool :default false
   abort if synthesis conjecture is not single invocation
 option cegqiSingleInvMultiInstAbort --cegqi-si-multi-inst-abort bool :default false
@@ -240,12 +234,20 @@ option cbqi --cbqi bool :read-write :default false
  turns on counterexample-based quantifier instantiation
 option cbqi2 --cbqi2 bool :read-write :default false
  turns on new implementation of counterexample-based quantifier instantiation
-option recurseCbqi --cbqi-recurse bool :default false
+option recurseCbqi --cbqi-recurse bool :default true
  turns on recursive counterexample-based quantifier instantiation
 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 cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false
+ use integer infinity for vts in counterexample-based quantifier instantiation
+option cbqiUseInfReal --cbqi-use-inf-real bool :read-write :default false
+ use real infinity for vts in counterexample-based quantifier instantiation
+option cbqiPreRegInst --cbqi-prereg-inst bool :read-write :default false
+  preregister ground instantiations in counterexample-based quantifier instantiation
+option cbqiMinBounds --cbqi-min-bounds bool :default false
+  use minimally constrained lower/upper bound for counterexample-based quantifier instantiation
  
 ### local theory extensions options 
 
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 2c65b62b3..ebeb4b871 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -115,10 +115,14 @@ int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind
                                 (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) ));
       Node vc = v;
       if( !r.isOne() && !r.isNegativeOne() ){
-        if( doCoeff ){
-          vc = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( r.abs() ), vc );
+        if( vc.getType().isInteger() ){
+          if( doCoeff ){
+            vc = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( r.abs() ), vc );
+          }else{
+            return 0;
+          }
         }else{
-          return 0;
+          veq = NodeManager::currentNM()->mkNode( MULT, veq, NodeManager::currentNM()->mkConst( Rational(1) / r.abs() ) );
         }
       }
       if( r.sgn()==1 ){
@@ -313,15 +317,20 @@ void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int
 }
 
 void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) {
-  newHasPol = hasPol;
-  newPol = pol;
-  if( n.getKind()==NOT || ( n.getKind()==IMPLIES && child==0 ) ){
+  if( n.getKind()==AND || n.getKind()==OR ){
+    newHasPol = hasPol;
+    newPol = pol;
+  }else if( n.getKind()==IMPLIES ){
+    newHasPol = hasPol;
+    newPol = child==0 ? !pol : pol;
+  }else if( n.getKind()==NOT ){
+    newHasPol = hasPol;
     newPol = !pol;
-  }else if( n.getKind()==IFF || n.getKind()==XOR ){
-    newHasPol = false;
   }else if( n.getKind()==ITE ){
-    if( child==0 ){
-      newHasPol = false;
-    }
+    newHasPol = (child!=0) && hasPol;
+    newPol = pol;
+  }else{
+    newHasPol = false;
+    newPol = pol;
   }
 }
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index d6cbe386c..c32aeeb78 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -415,89 +415,105 @@ void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node
   }
 }
 
-Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol ) {
-  if( body.getType().isBoolean() ){
-    if( body.getKind()==EQUAL && options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE ){
-      for( size_t i=0; i<2; i++ ){
-        if( body[i].getKind()==ITE ){
-          Node no = i==0 ? body[1] : body[0];
-          if( no.getKind()!=ITE ){
-            bool doRewrite = options::iteLiftQuant()==ITE_LIFT_QUANT_MODE_ALL;
-            std::vector< Node > children;
-            children.push_back( body[i][0] );
-            for( size_t j=1; j<=2; j++ ){
-              //check if it rewrites to a constant
-              Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] );
-              nn = Rewriter::rewrite( nn );
-              children.push_back( nn );
-              if( nn.isConst() ){
-                doRewrite = true;
-              }
-            }
-            if( doRewrite ){
-              return NodeManager::currentNM()->mkNode( ITE, children );
+Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond ) {
+  if( body.getKind()==EQUAL && options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE ){
+    for( size_t i=0; i<2; i++ ){
+      if( body[i].getKind()==ITE ){
+        Node no = i==0 ? body[1] : body[0];
+        if( no.getKind()!=ITE ){
+          bool doRewrite = options::iteLiftQuant()==ITE_LIFT_QUANT_MODE_ALL;
+          std::vector< Node > children;
+          children.push_back( body[i][0] );
+          for( size_t j=1; j<=2; j++ ){
+            //check if it rewrites to a constant
+            Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] );
+            nn = Rewriter::rewrite( nn );
+            children.push_back( nn );
+            if( nn.isConst() ){
+              doRewrite = true;
             }
           }
+          if( doRewrite ){
+            return NodeManager::currentNM()->mkNode( ITE, children );
+          }
         }
       }
-    }else if( body.getKind()==ITE && hasPol ){
-      if( options::iteCondVarSplitQuant() ){
-        Trace("quantifiers-rewrite-ite-debug") << "Conditional var eq split " << body << std::endl;
-        for( unsigned r=0; r<2; r++ ){
-          //check if there is a variable elimination
-          Node b = r==0 ? body[0] : body[0].negate();
-          QuantPhaseReq qpr( b );
-          std::vector< Node > vars;
-          std::vector< Node > subs;
-          Trace("quantifiers-rewrite-ite-debug") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl;
-          for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
-            Trace("quantifiers-rewrite-ite-debug") << "phase req " << it->first << " -> " << it->second << std::endl;
-            if( it->second ){
-              if( it->first.getKind()==EQUAL ){
-                for( unsigned i=0; i<2; i++ ){
-                  if( it->first[i].getKind()==BOUND_VARIABLE ){
-                    unsigned j = i==0 ? 1 : 0;
-                    if( !hasArg1( it->first[i], it->first[j] ) ){
-                      vars.push_back( it->first[i] );
-                      subs.push_back( it->first[j] );
-                      break;
-                    }
+    }
+  }else if( body.getKind()==ITE ){
+    if( body.getType().isBoolean() && hasPol && options::iteCondVarSplitQuant() ){
+      Trace("quantifiers-rewrite-ite-debug") << "Conditional var eq split " << body << std::endl;
+      for( unsigned r=0; r<2; r++ ){
+        //check if there is a variable elimination
+        Node b = r==0 ? body[0] : body[0].negate();
+        QuantPhaseReq qpr( b );
+        std::vector< Node > vars;
+        std::vector< Node > subs;
+        Trace("quantifiers-rewrite-ite-debug") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl;
+        for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
+          Trace("quantifiers-rewrite-ite-debug") << "phase req " << it->first << " -> " << it->second << std::endl;
+          if( it->second ){
+            if( it->first.getKind()==EQUAL ){
+              for( unsigned i=0; i<2; i++ ){
+                if( it->first[i].getKind()==BOUND_VARIABLE ){
+                  unsigned j = i==0 ? 1 : 0;
+                  if( !hasArg1( it->first[i], it->first[j] ) ){
+                    vars.push_back( it->first[i] );
+                    subs.push_back( it->first[j] );
+                    break;
                   }
                 }
               }
             }
           }
-          if( !vars.empty() ){
-            //bool cpol = (r==1);
-            Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] );
-            //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-            //pos = Rewriter::rewrite( pos );
-            Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] );
-            Trace("quantifiers-rewrite-ite") << "*** Split ITE (conditional variable eq) " << body << " into : " << std::endl;
-            Trace("quantifiers-rewrite-ite") << "   " << pos << std::endl;
-            Trace("quantifiers-rewrite-ite") << "   " << neg << std::endl;
-            return NodeManager::currentNM()->mkNode( AND, pos, neg );
-          }
+        }
+        if( !vars.empty() ){
+          //bool cpol = (r==1);
+          Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] );
+          //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+          //pos = Rewriter::rewrite( pos );
+          Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] );
+          Trace("quantifiers-rewrite-ite") << "*** Split ITE (conditional variable eq) " << body << " into : " << std::endl;
+          Trace("quantifiers-rewrite-ite") << "   " << pos << std::endl;
+          Trace("quantifiers-rewrite-ite") << "   " << neg << std::endl;
+          return NodeManager::currentNM()->mkNode( AND, pos, neg );
         }
       }
     }
-    if( body.getKind()!=EQUAL && body.getKind()!=APPLY_UF ){
-      bool changed = false;
-      std::vector< Node > children;
-      for( size_t i=0; i<body.getNumChildren(); i++ ){
-        bool newHasPol;
-        bool newPol;
-        QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
-        Node nn = computeProcessIte( body[i], newHasPol, newPol );
-        children.push_back( nn );
-        changed = changed || nn!=body[i];
-      }
-      if( changed ){
-        return NodeManager::currentNM()->mkNode( body.getKind(), children );
+  }
+  bool changed = false;
+  std::vector< Node > children;
+  for( size_t i=0; i<body.getNumChildren(); i++ ){
+    bool newHasPol;
+    bool newPol;
+    QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
+    if( body.getKind()==ITE && i>0 ){
+      currCond[children[0]] = (i==1);
+    }
+    Node nn = computeProcessIte( body[i], newHasPol, newPol, currCond );
+    if( body.getKind()==ITE && i==0 ){
+      std::map< Node, bool >::iterator itc = currCond.find( nn );
+      if( itc!=currCond.end() ){
+        if( itc->second ){
+          return computeProcessIte( body[1], hasPol, pol, currCond );
+        }else{
+          return computeProcessIte( body[2], hasPol, pol, currCond );
+        }
       }
     }
+    children.push_back( nn );
+    changed = changed || nn!=body[i];
+  }
+  if( body.getKind()==ITE ){
+    currCond.erase( children[0] );
+  }
+  if( changed ){
+    if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
+      children.insert( children.begin(), body.getOperator() );
+    }
+    return NodeManager::currentNM()->mkNode( body.getKind(), children );
+  }else{
+    return body;
   }
-  return body;
 }
 
 Node QuantifiersRewriter::computeProcessIte2( Node body ){
@@ -1140,7 +1156,9 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
   }else if( computeOption==COMPUTE_NNF ){
     return options::nnfQuant();
   }else if( computeOption==COMPUTE_PROCESS_ITE ){
-    return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant();
+    //always eliminate redundant conditions in ITE
+    return true;
+    //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant();
   }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){
     return options::iteDtTesterSplitQuant();
   }else if( computeOption==COMPUTE_PRENEX ){
@@ -1182,7 +1200,8 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp
     }else if( computeOption==COMPUTE_NNF ){
       n = computeNNF( n );
     }else if( computeOption==COMPUTE_PROCESS_ITE ){
-      n = computeProcessIte( n, true, true );
+      std::map< Node, bool > curr_cond;
+      n = computeProcessIte( n, true, true, curr_cond );
     }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){
       n = computeProcessIte2( n );
     }else if( computeOption==COMPUTE_PRENEX ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index d01677171..7db80c84b 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -46,7 +46,7 @@ private:
   static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl );
   static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
   static Node computeNNF( Node body );
-  static Node computeProcessIte( Node body, bool hasPol, bool pol );
+  static Node computeProcessIte( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond );
   static Node computeProcessIte2( Node body );
   static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl );
   static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index eefa45770..52aee392b 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1294,11 +1294,25 @@ Node TermDb::getCanonicalTerm( TNode n, bool apply_torder ){
   return getCanonicalTerm( n, var_count, subs, apply_torder );
 }
 
+void TermDb::getVtsTerms( std::vector< Node >& t, bool isFree, bool create, bool inc_delta ) {
+  if( inc_delta ){
+    Node delta = getVtsDelta( isFree, create );
+    if( !delta.isNull() ){
+      t.push_back( delta );
+    }
+  }
+  for( unsigned r=0; r<2; r++ ){
+    Node inf = getVtsInfinityIndex( r, isFree, create );
+    if( !inf.isNull() ){
+      t.push_back( inf );
+    }
+  }
+}
 
 Node TermDb::getVtsDelta( bool isFree, bool create ) {
   if( create ){
     if( d_vts_delta_free.isNull() ){
-      d_vts_delta_free = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "free delta for virtual term substitution" );
+      d_vts_delta_free = NodeManager::currentNM()->mkSkolem( "delta_free", NodeManager::currentNM()->realType(), "free delta for virtual term substitution" );
       Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_vts_delta_free, NodeManager::currentNM()->mkConst( Rational( 0 ) ) );
       d_quantEngine->getOutputChannel().lemma( delta_lem );
     }
@@ -1309,90 +1323,127 @@ Node TermDb::getVtsDelta( bool isFree, bool create ) {
   return isFree ? d_vts_delta_free : d_vts_delta;
 }
 
-Node TermDb::getVtsInfinity( bool isFree, bool create ) {
+Node TermDb::getVtsInfinity( TypeNode tn, bool isFree, bool create ) {
   if( create ){
-    if( d_vts_inf_free.isNull() ){
-      d_vts_inf_free = NodeManager::currentNM()->mkSkolem( "inf", NodeManager::currentNM()->integerType(), "free infinity for virtual term substitution" );
+    if( d_vts_inf_free[tn].isNull() ){
+      d_vts_inf_free[tn] = NodeManager::currentNM()->mkSkolem( "inf_free", tn, "free infinity for virtual term substitution" );
     }
-    if( d_vts_inf.isNull() ){
-      d_vts_inf = NodeManager::currentNM()->mkSkolem( "inf", NodeManager::currentNM()->integerType(), "infinity for virtual term substitution" );
+    if( d_vts_inf[tn].isNull() ){
+      d_vts_inf[tn] = NodeManager::currentNM()->mkSkolem( "inf", tn, "infinity for virtual term substitution" );
     }
   }
-  return isFree ? d_vts_inf_free : d_vts_inf;
+  return isFree ? d_vts_inf_free[tn] : d_vts_inf[tn];
+}
+
+Node TermDb::getVtsInfinityIndex( int i, bool isFree, bool create ) {
+  if( i==0 ){
+    return getVtsInfinity( NodeManager::currentNM()->realType(), isFree, create );
+  }else if( i==1 ){
+    return getVtsInfinity( NodeManager::currentNM()->integerType(), isFree, create );
+  }else{
+    Assert( false );
+    return Node::null();
+  }
+}
+
+Node TermDb::substituteVtsFreeTerms( Node n ) {
+  std::vector< Node > vars;
+  getVtsTerms( vars, false, false );
+  std::vector< Node > vars_free;
+  getVtsTerms( vars_free, true, false );
+  Assert( vars.size()==vars_free.size() );
+  if( !vars.empty() ){
+    return n.substitute( vars.begin(), vars.end(), vars_free.begin(), vars_free.end() );
+  }else{
+    return n;
+  }
 }
 
 Node TermDb::rewriteVtsSymbols( Node n ) {
   if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) ){
     Trace("quant-vts-debug") << "VTS : process " << n << std::endl;
-    bool rew_inf = false;
+    Node rew_vts_inf;
     bool rew_delta = false;
     //rewriting infinity always takes precedence over rewriting delta
-    if( !d_vts_inf.isNull() && containsTerm( n, d_vts_inf ) ){
-      rew_inf = true;
-    }else if( !d_vts_delta.isNull() && containsTerm( n, d_vts_delta ) ){
-      rew_delta = true;
-    }
-    if( rew_inf || rew_delta ){
-      if( n.getKind()==EQUAL ){
-        return d_false;
-      }else{
-        std::map< Node, Node > msum;
-        if( QuantArith::getMonomialSumLit( n, msum ) ){
-          if( Trace.isOn("quant-vts-debug") ){
-            Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl;
-            QuantArith::debugPrintMonomialSum( msum, "quant-vts-debug" );
+    for( unsigned r=0; r<2; r++ ){
+      Node inf = getVtsInfinityIndex( r, false, false );
+      if( !inf.isNull() && containsTerm( n, inf ) ){
+        if( rew_vts_inf.isNull() ){
+          rew_vts_inf = inf;
+        }else{
+          //for mixed int/real with multiple infinities
+          Trace("quant-vts-debug") << "Multiple infinities...equate " << inf << " = " << rew_vts_inf << std::endl;
+          std::vector< Node > subs_lhs;
+          subs_lhs.push_back( inf );
+          std::vector< Node > subs_rhs;
+          subs_lhs.push_back( rew_vts_inf );
+          n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
+          n = Rewriter::rewrite( n );
+          //may have cancelled
+          if( !containsTerm( n, rew_vts_inf ) ){
+            rew_vts_inf = Node::null();
           }
-          Node vts_sym = rew_inf ? d_vts_inf : d_vts_delta;
-          Assert( !vts_sym.isNull() );
-          Node iso_n;
-          int res = QuantArith::isolate( vts_sym, msum, iso_n, n.getKind(), true );
-          if( res!=0 ){
-            Trace("quant-vts-debug") << "VTS isolated :  -> " << iso_n << ", res = " << res << std::endl;
-            int index = res==1 ? 0 : 1;
-            Node slv = iso_n[res==1 ? 1 : 0];
-            if( iso_n[index]!=vts_sym ){
-              if( iso_n[index].getKind()==MULT && iso_n[index].getNumChildren()==2 && iso_n[index][0].isConst() && iso_n[index][1]==vts_sym ){
-                slv = NodeManager::currentNM()->mkNode( MULT, slv, NodeManager::currentNM()->mkConst( Rational(1)/iso_n[index][0].getConst<Rational>() ) );
-              }else{
-                Trace("quant-vts-debug") << "Failed, return " << n << std::endl;
-                return n;
-              }
-            }
-            Node nlit;
-            if( res==1 ){
-              if( rew_inf ){
-                nlit = d_true;
-              }else{
-                nlit = NodeManager::currentNM()->mkNode( GEQ, d_zero, slv );
-              }
+        }
+      }
+    }
+    if( rew_vts_inf.isNull() ){
+      if( !d_vts_delta.isNull() && containsTerm( n, d_vts_delta ) ){
+        rew_delta = true;
+      }
+    }
+    if( !rew_vts_inf.isNull()  || rew_delta ){
+      std::map< Node, Node > msum;
+      if( QuantArith::getMonomialSumLit( n, msum ) ){
+        if( Trace.isOn("quant-vts-debug") ){
+          Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl;
+          QuantArith::debugPrintMonomialSum( msum, "quant-vts-debug" );
+        }
+        Node vts_sym = !rew_vts_inf.isNull() ? rew_vts_inf : d_vts_delta;
+        Assert( !vts_sym.isNull() );
+        Node iso_n;
+        Node nlit;
+        int res = QuantArith::isolate( vts_sym, msum, iso_n, n.getKind(), true );
+        if( res!=0 ){
+          Trace("quant-vts-debug") << "VTS isolated :  -> " << iso_n << ", res = " << res << std::endl;
+          Node slv = iso_n[res==1 ? 1 : 0];
+          //ensure the vts terms have been eliminated
+          if( containsVtsTerm( slv ) ){
+            Trace("quant-vts-warn") << "Bad vts literal : " << n << ", contains " << vts_sym << " but bad solved form " << slv << "." << std::endl;
+            nlit = substituteVtsFreeTerms( n );
+            Trace("quant-vts-debug") << "...return " << nlit << std::endl;
+            //Assert( false );
+            //safe case: just convert to free symbols
+            return nlit;
+          }else{
+            if( !rew_vts_inf.isNull() ){
+              nlit = ( n.getKind()==GEQ && res==1 ) ? d_true : d_false;
             }else{
-              if( rew_inf ){
+              Assert( iso_n[res==1 ? 0 : 1]==d_vts_delta );
+              if( n.getKind()==EQUAL ){
                 nlit = d_false;
+              }else if( res==1 ){
+                nlit = NodeManager::currentNM()->mkNode( GEQ, d_zero, slv );
               }else{
                 nlit = NodeManager::currentNM()->mkNode( GT, slv, d_zero );
               }
             }
-            Trace("quant-vts-debug") << "Return " << nlit << std::endl;
-            return nlit;
           }
+          Trace("quant-vts-debug") << "Return " << nlit << std::endl;
+          return nlit;
+        }else{
+          Trace("quant-vts-warn") << "Bad vts literal : " << n << ", contains " << vts_sym << " but could not isolate." << std::endl;
+          //safe case: just convert to free symbols
+          nlit = substituteVtsFreeTerms( n );
+          Trace("quant-vts-debug") << "...return " << nlit << std::endl;
+          //Assert( false );
+          return nlit;
         }
       }
     }
     return n;
   }else if( n.getKind()==FORALL ){
     //cannot traverse beneath quantifiers
-    std::vector< Node > vars;
-    std::vector< Node > vars_free;
-    if( !d_vts_inf.isNull() ){
-      vars.push_back( d_vts_inf );
-      vars_free.push_back( d_vts_inf_free );
-    }
-    if( !d_vts_delta.isNull() ){
-      vars.push_back( d_vts_delta );
-      vars_free.push_back( d_vts_delta_free );
-    }
-    n = n.substitute( vars.begin(), vars.end(), vars_free.begin(), vars_free.end() );
-    return n;
+    return substituteVtsFreeTerms( n );
   }else{
     bool childChanged = false;
     std::vector< Node > children;
@@ -1414,19 +1465,77 @@ Node TermDb::rewriteVtsSymbols( Node n ) {
   }
 }
 
-bool TermDb::containsTerm( Node n, Node t ) {
+bool TermDb::containsVtsTerm( Node n, bool isFree ) {
+  std::vector< Node > t;
+  getVtsTerms( t, isFree, false );
+  return containsTerms( n, t );
+}
+
+bool TermDb::containsVtsTerm( std::vector< Node >& n, bool isFree ) {
+  std::vector< Node > t;
+  getVtsTerms( t, isFree, false );
+  if( !t.empty() ){
+    for( unsigned i=0; i<n.size(); i++ ){
+      if( containsTerms( n[i], t ) ){
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+bool TermDb::containsVtsInfinity( Node n, bool isFree ) {
+  std::vector< Node > t;
+  getVtsTerms( t, isFree, false, false );
+  return containsTerms( n, t );
+}
+
+bool TermDb::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) {
   if( n==t ){
     return true;
   }else{
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( containsTerm( n[i], t ) ){
-        return true;
+    if( visited.find( n )==visited.end() ){
+      visited[n] = true;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        if( containsTerm2( n[i], t, visited ) ){
+          return true;
+        }
       }
     }
     return false;
   }
 }
 
+bool TermDb::containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ) {
+  if( std::find( t.begin(), t.end(), n )!=t.end() ){
+    return true;
+  }else{
+    if( visited.find( n )==visited.end() ){
+      visited[n] = true;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        if( containsTerms2( n[i], t, visited ) ){
+          return true;
+        }
+      }
+    }
+    return false;
+  }
+}
+
+bool TermDb::containsTerm( Node n, Node t ) {
+  std::map< Node, bool > visited;
+  return containsTerm2( n, t, visited );
+}
+
+bool TermDb::containsTerms( Node n, std::vector< Node >& t ) {
+  if( t.empty() ){
+    return false;
+  }else{
+    std::map< Node, bool > visited;
+    return containsTerms2( n, t, visited );
+  }
+}
+
 Node TermDb::simpleNegate( Node n ){
   if( n.getKind()==OR || n.getKind()==AND ){
     std::vector< Node > children;
@@ -1457,7 +1566,8 @@ void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
 
 bool TermDb::isInductionTerm( Node n ) {
   if( options::dtStcInduction() && datatypes::DatatypesRewriter::isTermDatatype( n ) ){
-    return true;
+    const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
+    return !dt.isCodatatype();
   }
   if( options::intWfInduction() && n.getType().isInteger() ){
     return true;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 416761ce8..9c5a7cc56 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -348,21 +348,39 @@ public:
 //for virtual term substitution
 private:
   Node d_vts_delta;
-  Node d_vts_inf;
+  std::map< TypeNode, Node > d_vts_inf;
   Node d_vts_delta_free;
-  Node d_vts_inf_free;
+  std::map< TypeNode, Node > d_vts_inf_free;
+  /** get vts infinity index */
+  Node getVtsInfinityIndex( int i, bool isFree = false, bool create = true  );
+  /** substitute vts free terms */
+  Node substituteVtsFreeTerms( Node n );
 public:
   /** get vts delta */
   Node getVtsDelta( bool isFree = false, bool create = true );
   /** get vts infinity */
-  Node getVtsInfinity( bool isFree = false, bool create = true );
+  Node getVtsInfinity( TypeNode tn, bool isFree = false, bool create = true );
+  /** get all vts terms */
+  void getVtsTerms( std::vector< Node >& t, bool isFree = false, bool create = true, bool inc_delta = true );
   /** rewrite delta */
   Node rewriteVtsSymbols( Node n );
-
+  /** simple check for contains term */
+  bool containsVtsTerm( Node n, bool isFree = false );
+  /** simple check for contains term */
+  bool containsVtsTerm( std::vector< Node >& n, bool isFree = false );
+  /** simple check for contains term */
+  bool containsVtsInfinity( Node n, bool isFree = false );
+  
+private:
+  //helper for contains term
+  static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited );
+  static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited );
 //general utilities
 public:
   /** simple check for contains term */
   static bool containsTerm( Node n, Node t );
+  /** simple check for contains term */
+  static bool containsTerms( Node n, std::vector< Node >& t );
   /** simple negate */
   static Node simpleNegate( Node n );
   /** is assoc */
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 649d34922..48891732b 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -77,6 +77,9 @@ void TheoryQuantifiers::preRegisterTerm(TNode n) {
 
 void TheoryQuantifiers::presolve() {
   Debug("quantifiers-presolve") << "TheoryQuantifiers::presolve()" << endl;
+  if( getQuantifiersEngine() ){
+    getQuantifiersEngine()->presolve();
+  }
 }
 
 Node TheoryQuantifiers::getValue(TNode n) {
@@ -169,7 +172,7 @@ Node TheoryQuantifiers::getNextDecisionRequest(){
 
 void TheoryQuantifiers::assertUniversal( Node n ){
   Assert( n.getKind()==FORALL );
-  if( options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){
+  if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){
     getQuantifiersEngine()->assertQuantifier( n, true );
   }
 }
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 13c408d85..1a5be5a57 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -252,6 +252,7 @@ Valuation& QuantifiersEngine::getValuation(){
 }
 
 void QuantifiersEngine::finishInit(){
+  Trace("quant-engine-debug") << "QuantifiersEngine : finishInit " << std::endl;
   for( int i=0; i<(int)d_modules.size(); i++ ){
     d_modules[i]->finishInit();
   }
@@ -281,6 +282,13 @@ bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) {
   return mo==m || mo==NULL;
 }
 
+void QuantifiersEngine::presolve() {
+  Trace("quant-engine-debug") << "QuantifiersEngine : presolve " << std::endl;
+  for( unsigned i=0; i<d_modules.size(); i++ ){
+    d_modules[i]->presolve();
+  }
+}
+
 void QuantifiersEngine::check( Theory::Effort e ){
   CodeTimer codeTimer(d_time);
   if( !getMasterEqualityEngine()->consistent() ){
@@ -329,6 +337,10 @@ void QuantifiersEngine::check( Theory::Effort e ){
       Trace("quant-engine-ee") << "Equality engine : " << std::endl;
       debugPrintEqualityEngine( "quant-engine-ee" );
     }
+    if( Trace.isOn("quant-engine-assert") ){
+      Trace("quant-engine-assert") << "Assertions : " << std::endl;
+      getTheoryEngine()->printAssertions("quant-engine-assert");
+    }
 
     //reset relevant information
     d_conflict = false;
@@ -616,9 +628,9 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
   //do virtual term substitution
   if( doVts ){
     body = Rewriter::rewrite( body );
-    Trace("inst-debug") << "Rewrite vts symbols in " << body << std::endl;
+    Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl;
     Node body_r = d_term_db->rewriteVtsSymbols( body );
-    Trace("inst-debug") << "            ...result: " << body_r << std::endl;
+    Trace("quant-vts-debug") << "            ...result: " << body_r << std::endl;
     body = body_r;
   }
   Trace("inst-assert") << "(assert " << body << ")" << std::endl;
@@ -800,15 +812,15 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b
 bool QuantifiersEngine::addLemma( Node lem, bool doCache ){
   if( doCache ){
     lem = Rewriter::rewrite(lem);
-    Trace("inst-add-debug2") << "Adding lemma : " << lem << std::endl;
+    Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl;
     if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
       //d_curr_out->lemma( lem, false, true );
       d_lemmas_produced_c[ lem ] = true;
       d_lemmas_waiting.push_back( lem );
-      Trace("inst-add-debug2") << "Added lemma" << std::endl;
+      Trace("inst-add-debug") << "Added lemma" << std::endl;
       return true;
     }else{
-      Trace("inst-add-debug2") << "Duplicate." << std::endl;
+      Trace("inst-add-debug") << "Duplicate." << std::endl;
       return false;
     }
   }else{
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 101aa43cd..2658d09f0 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -53,6 +53,8 @@ public:
   QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
   /** initialize */
   virtual void finishInit() {}
+  /** presolve */
+  virtual void presolve() {}
   /* whether this module needs to check this round */
   virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
   /* whether this module needs a model built */
@@ -251,6 +253,8 @@ public:
 public:
   /** initialize */
   void finishInit();
+  /** presolve */
+  void presolve();
   /** check at level */
   void check( Theory::Effort e );
   /** register quantifier */
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 7023f7c41..872933cbd 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -948,8 +948,9 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
         bool flag = false;
         unsigned n1 = node[0].getNumChildren();
         unsigned n2 = node[1].getNumChildren();
-        if(n1 - n2) {
-          for(unsigned i=0; i<=n1 - n2; i++) {
+        if( n1>n2 ){
+          unsigned diff = n1-n2;
+          for(unsigned i=0; i<diff; i++) {
             if(node[0][i] == node[1][0]) {
               flag = true;
               for(unsigned j=1; j<n2; j++) {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 0c1a7c081..b28a73b9d 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -798,9 +798,6 @@ private:
   /** Visitor for collecting shared terms */
   SharedTermsVisitor d_sharedTermsVisitor;
 
-  /** Prints the assertions to the debug stream */
-  void printAssertions(const char* tag);
-
   /** Dump the assertions to the dump */
   void dumpAssertions(const char* tag);
 
@@ -830,8 +827,14 @@ public:
   SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; }
 
   theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
+  
+  RemoveITE* getIteRemover() { return &d_iteRemover; }
 
   SortInference* getSortInference() { return &d_sortInfer; }
+  
+  /** Prints the assertions to the debug stream */
+  void printAssertions(const char* tag);
+
 private:
   std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;
 public:
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index c15074d8c..d913cb76a 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1047,6 +1047,7 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
     //add splitting lemma for cardinality constraint
     Assert( !d_cardinality_term.isNull() );
     Node lem = getCardinalityLiteral( d_aloc_cardinality );
+    Trace("uf-ss-lemma") << "*** Cardinality split on : " << lem << std::endl;
     lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() );
     d_cardinality_lemma[ d_aloc_cardinality ] = lem;
     //add as lemma to output channel