Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts symbols. Move presolve for sygus to cbqi. Enable --cbqi-recurse by default, add option --cbqi-min-bound. Enable qcf for finite model finding by default.

13 files changed, 371 insertions, 295 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index e10ba0fef..dce9c088c 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 );
@@ -150,7 +150,7 @@ bool CegConjecture::needsCheck() {
 }
 
 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 +178,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 ){
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index af3a19d62..9228f11b6 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 */
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index a1aa9dad8..398415ca8 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -45,11 +45,18 @@ 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 ) {
@@ -73,15 +80,9 @@ 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;
-    }
+    //copy variables to instantiator
+    d_cinst->d_vars.clear();
+    d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
 
     return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst );
   }else{
@@ -89,14 +90,9 @@ Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) {
   }
 }
 
-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 +453,8 @@ 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::cbqiSingleInvPreRegInst() && d_single_inv.getKind()==FORALL ){
+      d_cinst->presolve( d_single_inv );
     }
   }
 }
@@ -746,7 +687,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();
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index 2c955db5d..7df859337 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -103,7 +103,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
@@ -116,7 +116,7 @@ public:
   //get the single invocation lemma
   Node getSingleInvLemma( Node guard );
   //initialize
-  void initialize( QuantifiersEngine * qe, Node q );
+  void initialize( Node q );
   //check
   void check( std::vector< Node >& lems );
   //get solution
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index bf0168c64..3d33f01ca 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -195,12 +195,6 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                           }
                         }
                         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 ) ){
@@ -222,9 +216,12 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
 
       //[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++ ){
@@ -277,8 +274,32 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                     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;
                     }
+                    //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() ){
+                            if( itv->second.isNull() || itv->second.getConst<Rational>().sgn()==1 ){
+                              vts_coeff[t] = QuantArith::negate(vts_coeff[t]);
+                              Trace("cbqi-inst-debug") << "negate vts[" << t<< "] coefficient." << std::endl;
+                            }
+                          }
+                          Trace("cbqi-inst-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl;
+                          msum.erase( vts_sym[t] );
+                        }
+                      }
+                    }
+
+                    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 );
@@ -294,12 +315,6 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                           Assert( veq_v==pv );
                         }
                       }
-                      //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();
-                      }
 
                       //disequalities are either strict upper or lower bounds
                       unsigned rmax = ( atom.getKind()==GEQ && options::cbqiModel() ) ? 1 : 2;
@@ -320,29 +335,38 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                             }
                           }
                         }else{
-                          unsigned use_r = r;
+                          bool is_upper = ( r==0 );
                           if( options::cbqiModel() ){
                             // disequality is a disjunction : only consider the bound in the direction of the model
-                            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 );
+                            //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 );
                             }
-                            Assert( lhs_value!=rhs_value );
-                            Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value );
-                            cmp = Rewriter::rewrite( cmp );
-                            Assert( cmp.isConst() );
-                            use_r = cmp==d_true ? 1 : 0;
                           }
                           Assert( atom.getKind()==EQUAL && !pol );
                           if( pvtn.isInteger() ){
-                            uires = use_r==0 ? -1 : 1;
+                            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 = use_r==0 ? -2 : 2;
+                            uires = is_upper ? -2 : 2;
                           }
                         }
                         Trace("cbqi-bound-inf") << "From " << lit << ", got : ";
@@ -350,29 +374,38 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                           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{
+                              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 );
-                          mbp_strict[index].push_back( uires==2 || uires==-2 );
+                          for( unsigned t=0; t<2; t++ ){
+                            mbp_vts_coeff[index][t].push_back( vts_coeff[t] );
+                          }
                           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 );
-                            }
-                          }
+                          //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, subs, vars, coeff, has_coeff, theta, i, effort ) ){
                               return true;
                             }
-                          }else{
-                            Trace("cbqi-inst-debug") << "...already processed." << std::endl;
                           }
                         }
                       }
@@ -387,8 +420,11 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
       if( options::cbqiModel() ){
         if( pvtn.isInteger() || pvtn.isReal() ){
           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];
+          std::vector< Node > t_values[3];
           //try optimal bounds
           for( unsigned r=0; r<2; r++ ){
             int rr = upper_first ? (1-r) : r;
@@ -397,6 +433,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                 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( pvtn );
+                //TODO : rho value for infinity?
                 if( rr==0 ){
                   val = NodeManager::currentNM()->mkNode( UMINUS, val );
                   val = Rewriter::rewrite( val );
@@ -408,57 +445,116 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
             }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 ) ){
-                  return true;
+                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], subs, vars, coeff, has_coeff, theta, i, effort ) ){
+                      return true;
+                    }
+                  }
                 }
               }
             }
           }
-          //try non-optimal bounds (heuristic)
+          //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], subs, vars, coeff, has_coeff, theta, i, effort ) ){
+                      return true;
+                    }
+                  }
                 }
               }
             }
@@ -468,14 +564,14 @@ 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( !options::cbqiUseInfInt() || !options::cbqiUseInfReal() || pvtn.isBoolean() );
+      Assert( ( pvtn.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() );
 #endif
       if( addInstantiationInc( mv, pv, pv_coeff_m, subs, vars, coeff, has_coeff, theta, i, new_effort ) ){
         return true;
@@ -739,21 +835,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;
@@ -788,6 +873,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;
 }
 
@@ -812,25 +910,67 @@ bool CegInstantiator::check() {
   return false;
 }
 
-void setAuxRep( std::map< Node, Node >& aux_uf, std::map< Node, Node >& aux_subs, Node n1, Node n2 ){
-  Assert( aux_uf.find( n1 )==aux_uf.end() );
-  Assert( aux_uf.find( n2 )==aux_uf.end() );
-  //only merge if not in substitution
-  if( aux_subs.find( n1 )==aux_subs.end() ){
-    aux_uf[n1] = n2;
-  }else if( aux_subs.find( n2 )==aux_subs.end() ){
-    aux_uf[n2] = n1;
+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 );
+    }
   }
 }
 
-Node getAuxRep( std::map< Node, Node >& aux_uf, Node n ){
-  std::map< Node, Node >::iterator it = aux_uf.find( n );
-  if( it!=aux_uf.end() ){
-    Node r = getAuxRep( aux_uf, it->second );
-    aux_uf[n] = r;
-    return r;
-  }else{
-    return n;
+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 );
   }
 }
 
@@ -843,9 +983,7 @@ void CegInstantiator::processAssertions() {
 
   eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
   //to eliminate identified illegal terms
-  std::map< Node, Node > aux_uf;
   std::map< Node, Node > aux_subs;
-  std::map< Node, bool > aux_subs_inelig;
 
   //for each variable
   bool has_arith_var = false;
@@ -875,34 +1013,7 @@ void CegInstantiator::processAssertions() {
                   Trace("cbqi-proc") << "......add substitution : " << itae2->first << " -> " << itae2->second << std::endl;
                 }
               }
-            } 
-            /*
-            if( lit.getKind()==EQUAL ){
-              //check if it is an auxiliary variable (for instance, from ITE removal).  If so, solve for it.
-              for( unsigned k=0; k<2; k++ ){
-                Node s = lit[k];
-                if( std::find( d_aux_vars.begin(), d_aux_vars.end(), s )!=d_aux_vars.end() ){
-                  Node sr = getAuxRep( aux_uf, s );
-                  if( std::find( d_aux_vars.begin(), d_aux_vars.end(), lit[1-k] )!=d_aux_vars.end() ){
-                    Node ssr = getAuxRep( aux_uf, lit[1-k] );
-                    //merge in the union find
-                    if( sr!=ssr ){
-                      Trace("cbqi-proc") << "...merge : " << sr << " = " << ssr << std::endl;
-                      setAuxRep( aux_uf, aux_subs, sr, ssr );
-                    }
-                  //if we don't have yet a substitution yet or the substitution is ineligible
-                  }else if( aux_subs.find( sr )==aux_subs.end() || aux_subs_inelig[sr] ){
-                    computeProgVars( lit[1-k] );
-                    bool isInelig = d_inelig.find( lit[1-k] )!=d_inelig.end();
-                    //equality for auxiliary variable : will add to substitution
-                    Trace("cbqi-proc") << "...add to substitution : " << sr << " -> " << lit[1-k] << std::endl;
-                    aux_subs[sr] = lit[1-k];
-                    aux_subs_inelig[sr] = isInelig;
-                  }
-                }
-              }
             }
-            */
           }
         }
       }
@@ -951,20 +1062,18 @@ void CegInstantiator::processAssertions() {
   std::vector< Node > subs_lhs;
   std::vector< Node > subs_rhs;
   for( unsigned i=0; i<d_aux_vars.size(); i++ ){
-    Node l = d_aux_vars[i];
-    Node r = getAuxRep( aux_uf, l );
+    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, l, it->second );
+      addToAuxVarSubstitution( subs_lhs, subs_rhs, r, it->second );
     }else{
-      Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << l << "!!!" << std::endl;
+      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;
@@ -1407,14 +1516,14 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
       //heuristic for now, until we know how to do nested quantification
       Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( true, false );
       if( !delta.isNull() ){
-        Trace("cegqi") << "Delta lemma for " << d_small_const << std::endl;
+        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("cegqi") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl;
+        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 );
       }
@@ -1457,11 +1566,10 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
   }
 }
 
-
-
-
-
-
-
-
+void InstStrategyCegqi::registerQuantifier( Node q ) {
+  if( options::cbqiSingleInvPreRegInst() ){
+    CegInstantiator * cinst = getInstantiator( q );
+    cinst->presolve( q );
+  }
+}
 
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index f7cb290b2..c7c046e51 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -79,7 +79,8 @@ private:
   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:
@@ -92,6 +93,8 @@ public:
   std::map< Node, std::map< Node, Node > > d_aux_eq;
   //check : add instantiations based on valuation of d_vars
   bool check();
+  //presolve for quantified formula
+  void presolve( Node q );
 };
 
 class InstStrategySimplex : public InstStrategy{
@@ -170,9 +173,11 @@ 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 );
 };
 
 }
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 3dad74044..6cf64407f 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -102,7 +102,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
           //add counterexample lemma
           lem = Rewriter::rewrite( lem );
           Trace("cbqi") << "Counterexample lemma : " << lem << std::endl;
-          
+
           //must explicitly remove ITEs so that we record dependencies
           IteSkolemMap iteSkolemMap;
           std::vector< Node > lems;
@@ -140,7 +140,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
               }
             }
           }
-          
+
           addedLemma = true;
         }
       }
@@ -289,6 +289,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..d6cde9e7f 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -49,6 +49,8 @@ public:
   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
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 66de51f39..c693adef5 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -208,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
@@ -236,7 +234,7 @@ 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
@@ -246,7 +244,10 @@ 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 cbqiSingleInvPreRegInst --cbqi-prereg-inst bool :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 938245871..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 ){
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 58f0a265e..52aee392b 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1312,7 +1312,7 @@ void TermDb::getVtsTerms( std::vector< Node >& t, bool isFree, bool create, bool
 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 );
     }
@@ -1326,7 +1326,7 @@ Node TermDb::getVtsDelta( bool isFree, bool create ) {
 Node TermDb::getVtsInfinity( TypeNode tn, bool isFree, bool create ) {
   if( create ){
     if( d_vts_inf_free[tn].isNull() ){
-      d_vts_inf_free[tn] = NodeManager::currentNM()->mkSkolem( "inf", tn, "free infinity for virtual term substitution" );
+      d_vts_inf_free[tn] = NodeManager::currentNM()->mkSkolem( "inf_free", tn, "free 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" );
@@ -1346,6 +1346,19 @@ Node TermDb::getVtsInfinityIndex( int i, bool isFree, bool create ) {
   }
 }
 
+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;
@@ -1379,63 +1392,58 @@ Node TermDb::rewriteVtsSymbols( Node n ) {
       }
     }
     if( !rew_vts_inf.isNull()  || 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" );
-          }
-          Node vts_sym = !rew_vts_inf.isNull() ? rew_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_vts_inf.isNull() ){
-                nlit = d_true;
-              }else{
-                nlit = NodeManager::currentNM()->mkNode( GEQ, d_zero, slv );
-              }
+      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_vts_inf.isNull() ){
+              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;
-    getVtsTerms( vars, false );
-    std::vector< Node > vars_free;
-    getVtsTerms( vars_free, true );
-    Assert( vars.size()==vars_free.size() );
-    if( !vars.empty() ){
-      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;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 529207390..9c5a7cc56 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -353,6 +353,8 @@ private:
   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 );
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 649d34922..373a8a0da 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -169,7 +169,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 );
   }
 }