Enable counterexample-guided quantifier instantiation by default for quantified logics that include at least one relevant theory. Enforce restriction on model building to last call. Update options, refactor. Update regressions.

12 files changed, 1863 insertions, 1712 deletions

diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
new file mode 100644
index 000000000..90639d68c
--- /dev/null
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -0,0 +1,1402 @@
+/*********************                                                        */
+/*! \file ceg_instantiator.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of counterexample-guided quantifier instantiation
+ **/
+
+#include "theory/quantifiers/ceg_instantiator.h"
+#include "theory/arith/theory_arith.h"
+#include "theory/arith/partial_model.h"
+#include "theory/arith/theory_arith_private.h"
+#include "theory/theory_engine.h"
+#include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "util/ite_removal.h"
+
+//#define MBP_STRICT_ASSERTIONS
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+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 ) );
+  d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
+  d_true = NodeManager::currentNM()->mkConst( true );
+  d_is_nested_quant = false;
+}
+
+void CegInstantiator::computeProgVars( Node n ){
+  if( d_prog_var.find( n )==d_prog_var.end() ){
+    d_prog_var[n].clear();
+    if( std::find( d_vars.begin(), d_vars.end(), n )!=d_vars.end() ){
+      d_prog_var[n][n] = true;
+    }else if( !d_out->isEligibleForInstantiation( n ) ){
+      d_inelig[n] = true;
+      return;
+    }
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      computeProgVars( n[i] );
+      if( d_inelig.find( n[i] )!=d_inelig.end() ){
+        d_inelig[n] = true;
+        return;
+      }
+      for( std::map< Node, bool >::iterator it = d_prog_var[n[i]].begin(); it != d_prog_var[n[i]].end(); ++it ){
+        d_prog_var[n][it->first] = true;
+      }
+      //selectors applied to program variables are also variables
+      if( n.getKind()==APPLY_SELECTOR_TOTAL && d_prog_var[n].find( n[0] )!=d_prog_var[n].end() ){
+        d_prog_var[n][n] = true;
+      }
+    }
+  }
+}
+
+bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
+                                        std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
+                                        std::map< Node, Node >& cons, std::vector< Node >& curr_var ){
+  if( i==d_vars.size() ){
+    //solved for all variables, now construct instantiation
+    if( !sf.d_has_coeff.empty() ){
+      if( options::cbqiSymLia() ){
+        //use symbolic solved forms
+        SolvedForm csf;
+        csf.copy( ssf );
+        return addInstantiationCoeff( csf, vars, btyp, 0, cons );
+      }else{
+        return addInstantiationCoeff( sf, vars, btyp, 0, cons );
+      }
+    }else{
+      return addInstantiation( sf.d_subs, vars, cons );
+    }
+  }else{
+    std::map< Node, std::map< Node, bool > > subs_proc;
+    //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]];
+    bool is_cv = false;
+    Node pv;
+    if( curr_var.empty() ){
+      pv = d_vars[i];
+    }else{
+      pv = curr_var.back();
+      is_cv = true;
+    }
+    TypeNode pvtn = pv.getType();
+    Trace("cbqi-inst-debug") << "[Find instantiation for " << pv << "]" << std::endl;
+    Node pv_value;
+    if( options::cbqiModel() ){
+      pv_value = getModelValue( pv );
+      Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
+    }
+    Node pvr = pv;
+    if( d_qe->getMasterEqualityEngine()->hasTerm( pv ) ){
+      pvr = d_qe->getMasterEqualityEngine()->getRepresentative( pv );
+    }
+
+    //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
+      Trace("cbqi-inst-debug") << "[1] try based on equivalence class." << std::endl;
+      std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( pvr );
+      if( it_eqc!=d_curr_eqc.end() ){
+        Trace("cbqi-inst-debug2") << "...eqc has size " << it_eqc->second.size() << std::endl;
+        for( unsigned k=0; k<it_eqc->second.size(); k++ ){
+          Node n = it_eqc->second[k];
+          if( n!=pv ){
+            Trace("cbqi-inst-debug") << "...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
+            if( d_inelig.find( n )==d_inelig.end() ){
+              Node ns;
+              Node pv_coeff;  //coefficient of pv in the equality we solve (null is 1)
+              bool proc = false;
+              if( !d_prog_var[n].empty() ){
+                ns = applySubstitution( n, sf, vars, pv_coeff, false );
+                if( !ns.isNull() ){
+                  computeProgVars( ns );
+                  //substituted version must be new and cannot contain pv
+                  proc = subs_proc[pv_coeff].find( ns )==subs_proc[pv_coeff].end() && d_prog_var[ns].find( pv )==d_prog_var[ns].end();
+                }
+              }else{
+                ns = n;
+                proc = true;
+              }
+              if( proc ){
+                //try the substitution
+                subs_proc[ns][pv_coeff] = true;
+                if( addInstantiationInc( ns, pv, pv_coeff, 0, sf, ssf, vars,  btyp, theta, i, effort, cons, curr_var ) ){
+                  return true;
+                }
+              }
+            }
+          }
+        }
+      }else{
+        Trace("cbqi-inst-debug2") << "...eqc not found." << std::endl;
+      }
+
+      //[2] : we can solve an equality for pv
+      if( pvtn.isInteger() || pvtn.isReal() ){
+        ///iterate over equivalence classes to find cases where we can solve for the variable
+        TypeNode pvtnb = pvtn.getBaseType();
+        Trace("cbqi-inst-debug") << "[2] try based on solving arithmetic equivalence classes." << std::endl;
+        for( unsigned k=0; k<d_curr_type_eqc[pvtnb].size(); k++ ){
+          Node r = d_curr_type_eqc[pvtnb][k];
+          std::map< Node, std::vector< Node > >::iterator it_reqc = d_curr_eqc.find( r );
+          std::vector< Node > lhs;
+          std::vector< bool > lhs_v;
+          std::vector< Node > lhs_coeff;
+          Assert( it_reqc!=d_curr_eqc.end() );
+          for( unsigned kk=0; kk<it_reqc->second.size(); kk++ ){
+            Node n = it_reqc->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, sf, vars, pv_coeff );
+                if( !ns.isNull() ){
+                  computeProgVars( ns );
+                }
+              }else{
+                ns = n;
+              }
+              if( !ns.isNull() ){
+                bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end();
+                Trace("cbqi-inst-debug2") << "... " << ns << " has var " << pv << " : " << hasVar << std::endl;
+                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") << "... " << 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 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];
+                        if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
+                          subs_proc[val][veq_c] = true;
+                          if( addInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                            return true;
+                          }
+                        }
+                      }
+                    }
+                  }
+                }
+                lhs.push_back( ns );
+                lhs_v.push_back( hasVar );
+                lhs_coeff.push_back( pv_coeff );
+              }else{
+                Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible after substitution." << std::endl;
+              }
+            }else{
+              Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible." << std::endl;
+            }
+          }
+        }
+      }else if( pvtn.isDatatype() ){
+        Trace("cbqi-inst-debug") << "[2] try based on constructors in equivalence class." << std::endl;
+        //look in equivalence class for a constructor
+        if( it_eqc!=d_curr_eqc.end() ){
+          for( unsigned k=0; k<it_eqc->second.size(); k++ ){
+            Node n = it_eqc->second[k];
+            if( n.getKind()==APPLY_CONSTRUCTOR ){
+              Trace("cbqi-inst-debug") << "... " << i << "...try based on constructor term " << n << std::endl;
+              cons[pv] = n.getOperator();
+              const Datatype& dt = ((DatatypeType)(pvtn).toType()).getDatatype();
+              unsigned cindex = Datatype::indexOf( n.getOperator().toExpr() );
+              if( is_cv ){
+                curr_var.pop_back();
+              }
+              //now must solve for selectors applied to pv
+              for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){
+                curr_var.push_back( NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ) );
+              }
+              if( addInstantiation( sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                return true;
+              }else{
+                //cleanup
+                cons.erase( pv );
+                Assert( curr_var.size()>=dt[cindex].getNumArgs() );
+                for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){
+                  curr_var.pop_back();
+                }
+                if( is_cv ){
+                  curr_var.push_back( pv );
+                }
+                break;
+              }
+            }
+          }
+        }else{
+          Trace("cbqi-inst-debug2") << "... " << i << " does not have an eqc." << std::endl;
+        }
+      }
+
+      //[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< 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() );
+        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;
+            if( tid==THEORY_ARITH ){
+              //arithmetic inequalities and disequalities
+              if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol ) ){
+                Assert( atom[0].getType().isInteger() || atom[0].getType().isReal() );
+                Assert( atom.getKind()!=GEQ || atom[1].isConst() );
+                Node atom_lhs;
+                Node atom_rhs;
+                if( atom.getKind()==GEQ ){
+                  atom_lhs = atom[0];
+                  atom_rhs = atom[1];
+                }else{
+                  atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] );
+                  atom_lhs = Rewriter::rewrite( atom_lhs );
+                  atom_rhs = d_zero;
+                }
+
+                computeProgVars( atom_lhs );
+                //must be an eligible term
+                if( d_inelig.find( atom_lhs )==d_inelig.end() ){
+                  //apply substitution to LHS of atom
+                  if( !d_prog_var[atom_lhs].empty() ){
+                    Node atom_lhs_coeff;
+                    atom_lhs = applySubstitution( atom_lhs, sf, vars, atom_lhs_coeff );
+                    if( !atom_lhs.isNull() ){
+                      computeProgVars( atom_lhs );
+                      if( !atom_lhs_coeff.isNull() ){
+                        atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) );
+                      }
+                    }
+                  }
+                  //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( !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] );
+                          }
+                        }
+                      }
+
+                      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 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() ){
+                                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{
+                            bool is_upper = ( r==0 );
+                            if( options::cbqiModel() ){
+                              // 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 = getModelValue( 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( 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{
+                                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, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                                return true;
+                              }
+                            }
+                          }
+                        }
+                      }
+                    }
+                  }
+                }
+              }
+            }
+          }
+        }
+      }
+      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[3];
+          //try optimal bounds
+          for( unsigned r=0; r<2; r++ ){
+            int rr = upper_first ? (1-r) : r;
+            if( mbp_bounds[rr].empty() ){
+              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( 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(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                  return true;
+                }
+              }
+            }else{
+              Trace("cbqi-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << pvtn << ") : " << std::endl;
+              int best = -1;
+              Node best_bound_value[3];
+              for( unsigned j=0; j<mbp_bounds[rr].size(); j++ ){
+                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 = ";
+                }
+                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 = getModelValue( 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 ){
+                  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 << " : ";
+                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 = 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, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                      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, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                  return true;
+                }
+              }
+            }
+          }
+#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], 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, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                      return true;
+                    }
+                  }
+                }
+              }
+            }
+          }
+        }
+      }
+    }
+
+    //[4] resort to using value in model
+    // do so if we are in effort=1, or if the variable is boolean, or if we are solving for a subfield of a datatype
+    if( effort>0 || pvtn.isBoolean() || !curr_var.empty() ){
+      Node mv = getModelValue( 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.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() );
+#endif
+      if( addInstantiationInc( mv, pv, pv_coeff_m, 0, sf, ssf, vars, btyp, theta, i, new_effort, cons, curr_var ) ){
+        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, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
+                                           std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
+                                           std::map< Node, Node >& cons, std::vector< Node >& curr_var ) {
+  if( Trace.isOn("cbqi-inst") ){
+    for( unsigned j=0; j<sf.d_subs.size(); j++ ){
+      Trace("cbqi-inst") << " ";
+    }
+    Trace("cbqi-inst") << sf.d_subs.size() << ": ";
+    if( !pv_coeff.isNull() ){
+      Trace("cbqi-inst") << pv_coeff << " * ";
+    }
+    Trace("cbqi-inst") << pv << " -> " << n << std::endl;
+  }
+  //must ensure variables have been computed for n
+  computeProgVars( n );
+
+  //substitute into previous substitutions, when applicable
+  std::vector< Node > a_subs;
+  a_subs.push_back( n );
+  std::vector< Node > a_var;
+  a_var.push_back( pv );
+  std::vector< Node > a_coeff;
+  std::vector< Node > a_has_coeff;
+  if( !pv_coeff.isNull() ){
+    a_coeff.push_back( pv_coeff );
+    a_has_coeff.push_back( pv );
+  }
+  bool success = true;
+  std::map< int, Node > prev_subs;
+  std::map< int, Node > prev_coeff;
+  std::map< int, Node > prev_sym_subs;
+  std::vector< Node > new_has_coeff;
+  for( unsigned j=0; j<sf.d_subs.size(); j++ ){
+    Assert( d_prog_var.find( sf.d_subs[j] )!=d_prog_var.end() );
+    if( d_prog_var[sf.d_subs[j]].find( pv )!=d_prog_var[sf.d_subs[j]].end() ){
+      prev_subs[j] = sf.d_subs[j];
+      TNode tv = pv;
+      TNode ts = n;
+      Node a_pv_coeff;
+      Node new_subs = applySubstitution( sf.d_subs[j], a_subs, a_coeff, a_has_coeff, a_var, a_pv_coeff, true );
+      if( !new_subs.isNull() ){
+        sf.d_subs[j] = new_subs;
+        if( !a_pv_coeff.isNull() ){
+          prev_coeff[j] = sf.d_coeff[j];
+          if( sf.d_coeff[j].isNull() ){
+            Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), vars[j] )==sf.d_has_coeff.end() );
+            //now has coefficient
+            new_has_coeff.push_back( vars[j] );
+            sf.d_has_coeff.push_back( vars[j] );
+            sf.d_coeff[j] = a_pv_coeff;
+          }else{
+            sf.d_coeff[j] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[j], a_pv_coeff ) );
+          }
+        }
+        if( sf.d_subs[j]!=prev_subs[j] ){
+          computeProgVars( sf.d_subs[j] );
+        }
+      }else{
+        Trace("cbqi-inst-debug") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl;
+        success = false;
+        break;
+      }
+    }
+    if( options::cbqiSymLia() && pv_coeff.isNull() ){
+      //apply simple substitutions also to sym_subs
+      prev_sym_subs[j] = ssf.d_subs[j];
+      ssf.d_subs[j] = ssf.d_subs[j].substitute( a_var.begin(), a_var.end(), a_subs.begin(), a_subs.end() );
+      ssf.d_subs[j] = Rewriter::rewrite( ssf.d_subs[j] );
+    }
+  }
+  if( success ){
+    vars.push_back( pv );
+    btyp.push_back( bt );
+    sf.push_back( pv, n, pv_coeff );
+    ssf.push_back( pv, n, pv_coeff );
+    Node new_theta = theta;
+    if( !pv_coeff.isNull() ){
+      if( new_theta.isNull() ){
+        new_theta = pv_coeff;
+      }else{
+        new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, pv_coeff );
+        new_theta = Rewriter::rewrite( new_theta );
+      }
+    }
+    bool is_cv = false;
+    if( !curr_var.empty() ){
+      Assert( curr_var.back()==pv );
+      curr_var.pop_back();
+      is_cv = true;
+    }
+    success = addInstantiation( sf, ssf, vars, btyp, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var );
+    if( !success ){
+      if( is_cv ){
+        curr_var.push_back( pv );
+      }
+      sf.pop_back( pv, n, pv_coeff );
+      ssf.pop_back( pv, n, pv_coeff );
+      vars.pop_back();
+      btyp.pop_back();
+    }
+  }
+  if( success ){
+    return true;
+  }else{
+    //revert substitution information
+    for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){
+      sf.d_subs[it->first] = it->second;
+    }
+    for( std::map< int, Node >::iterator it = prev_coeff.begin(); it != prev_coeff.end(); it++ ){
+      sf.d_coeff[it->first] = it->second;
+    }
+    for( unsigned i=0; i<new_has_coeff.size(); i++ ){
+      sf.d_has_coeff.pop_back();
+    }
+    for( std::map< int, Node >::iterator it = prev_sym_subs.begin(); it != prev_sym_subs.end(); it++ ){
+      ssf.d_subs[it->first] = it->second;
+    }
+    return false;
+  }
+}
+
+bool CegInstantiator::addInstantiationCoeff( SolvedForm& sf, std::vector< Node >& vars, std::vector< int >& btyp,
+                                             unsigned j, std::map< Node, Node >& cons ) {
+
+
+  if( j==sf.d_has_coeff.size() ){
+    return addInstantiation( sf.d_subs, vars, cons );
+  }else{
+    Assert( std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )!=vars.end() );
+    unsigned index = std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )-vars.begin();
+    Node prev = sf.d_subs[index];
+    Assert( !sf.d_coeff[index].isNull() );
+    Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_coeff[index] << " * " << vars[index] << " = " << sf.d_subs[index] << std::endl;
+    Assert( vars[index].getType().isInteger() );
+    //must ensure that divisibility constraints are met
+    //solve updated rewritten equality for vars[index], if coefficient is one, then we are successful
+    Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[index], vars[index] );
+    Node eq_rhs = sf.d_subs[index];
+    Node eq = eq_lhs.eqNode( eq_rhs );
+    eq = Rewriter::rewrite( eq );
+    Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl;
+    std::map< Node, Node > msum;
+    if( QuantArith::getMonomialSumLit( eq, msum ) ){
+      Node veq;
+      if( QuantArith::isolate( vars[index], msum, veq, EQUAL, true )!=0 ){
+        Node veq_c;
+        if( veq[0]!=vars[index] ){
+          Node veq_v;
+          if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){
+            Assert( veq_v==vars[index] );
+          }
+        }
+        sf.d_subs[index] = veq[1];
+        if( !veq_c.isNull() ){
+          sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c );
+          Trace("cbqi-inst-debug") << "...bound type is : " << btyp[index] << std::endl;
+          //intger division rounding up if from a lower bound
+          if( btyp[index]==1 && options::cbqiRoundUpLowerLia() ){
+            sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index],
+              NodeManager::currentNM()->mkNode( ITE,
+                NodeManager::currentNM()->mkNode( EQUAL,
+                  NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ),
+                  d_zero ),
+                d_zero, d_one )
+            );
+          }
+        }
+        Trace("cbqi-inst-debug") << "...normalize integers : " << vars[index] << " -> " << sf.d_subs[index] << std::endl;
+        if( options::cbqiSymLia() ){
+          //must apply substitution to previous subs
+          std::vector< Node > curr_var;
+          std::vector< Node > curr_subs;
+          curr_var.push_back( vars[index] );
+          curr_subs.push_back( sf.d_subs[index] );
+          for( unsigned k=0; k<index; k++ ){
+            Node prevs = sf.d_subs[k];
+            sf.d_subs[k] = sf.d_subs[k].substitute( curr_var.begin(), curr_var.end(), curr_subs.begin(), curr_subs.end() );
+            if( prevs!=sf.d_subs[k] ){
+              Trace("cbqi-inst-debug2") << "      rewrite " << vars[k] << " -> " << prevs << " to ";
+              sf.d_subs[k] = Rewriter::rewrite( sf.d_subs[k] );
+              Trace("cbqi-inst-debug2") << sf.d_subs[k] << std::endl;
+            }
+          }
+        }
+        if( addInstantiationCoeff( sf, vars, btyp, j+1, cons ) ){
+          return true;
+        }
+      }
+    }
+    sf.d_subs[index] = prev;
+    Trace("cbqi-inst-debug") << "...failed." << std::endl;
+    return false;
+  }
+}
+
+bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ) {
+  if( vars.size()>d_vars.size() ){
+    Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl;
+    std::map< Node, Node > subs_map;
+    for( unsigned i=0; i<subs.size(); i++ ){
+      subs_map[vars[i]] = subs[i];
+    }
+    subs.clear();
+    for( unsigned i=0; i<d_vars.size(); i++ ){
+      Node n = constructInstantiation( d_vars[i], subs_map, cons );
+      Trace("cbqi-inst-debug") << "  " << d_vars[i] << " -> " << n << std::endl;
+      subs.push_back( n );
+    }
+  }
+  bool ret = d_out->addInstantiation( subs );
+#ifdef MBP_STRICT_ASSERTIONS
+  Assert( ret );
+#endif
+  return ret;
+}
+
+Node CegInstantiator::constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons ) {
+  std::map< Node, Node >::iterator it = subs_map.find( n );
+  if( it!=subs_map.end() ){
+    return it->second;
+  }else{
+    it = cons.find( n );
+    Assert( it!=cons.end() );
+    std::vector< Node > children;
+    children.push_back( it->second );
+    const Datatype& dt = Datatype::datatypeOf( it->second.toExpr() );
+    unsigned cindex = Datatype::indexOf( it->second.toExpr() );
+    for( unsigned i=0; i<dt[cindex].getNumArgs(); i++ ){
+      Node nn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][i].getSelector() ), n );
+      Node nc = constructInstantiation( nn, subs_map, cons );
+      children.push_back( nc );
+    }
+    return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
+  }
+}
+
+Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff,
+                                         std::vector< Node >& vars, 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;
+  if( !has_coeff.empty() ){
+    for( std::map< Node, bool >::iterator it = d_prog_var[n].begin(); it != d_prog_var[n].end(); ++it ){
+      if( std::find( has_coeff.begin(), has_coeff.end(), it->first )!=has_coeff.end() ){
+        req_coeff = true;
+        break;
+      }
+    }
+  }
+  if( !req_coeff ){
+    Node nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+    if( n!=nret ){
+      nret = Rewriter::rewrite( nret );
+    }
+    //result is nret
+    return nret;
+  }else{
+    if( try_coeff ){
+      //must convert to monomial representation
+      std::map< Node, Node > msum;
+      if( QuantArith::getMonomialSum( n, msum ) ){
+        std::map< Node, Node > msum_coeff;
+        std::map< Node, Node > msum_term;
+        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+          //check if in substitution
+          std::vector< Node >::iterator its = std::find( vars.begin(), vars.end(), it->first );
+          if( its!=vars.end() ){
+            int index = its-vars.begin();
+            if( coeff[index].isNull() ){
+              //apply substitution
+              msum_term[it->first] = subs[index];
+            }else{
+              //apply substitution, multiply to ensure no divisibility conflict
+              msum_term[it->first] = subs[index];
+              //relative coefficient
+              msum_coeff[it->first] = coeff[index];
+              if( pv_coeff.isNull() ){
+                pv_coeff = coeff[index];
+              }else{
+                pv_coeff = NodeManager::currentNM()->mkNode( MULT, pv_coeff, coeff[index] );
+              }
+            }
+          }else{
+            msum_term[it->first] = it->first;
+          }
+        }
+        //make sum with normalized coefficient
+        Assert( !pv_coeff.isNull() );
+        pv_coeff = Rewriter::rewrite( pv_coeff );
+        Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_coeff << std::endl;
+        std::vector< Node > children;
+        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+          Node c_coeff;
+          if( !msum_coeff[it->first].isNull() ){
+            c_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkConst( pv_coeff.getConst<Rational>() / msum_coeff[it->first].getConst<Rational>() ) );
+          }else{
+            c_coeff = pv_coeff;
+          }
+          if( !it->second.isNull() ){
+            c_coeff = NodeManager::currentNM()->mkNode( MULT, c_coeff, it->second );
+          }
+          Node c = NodeManager::currentNM()->mkNode( MULT, c_coeff, msum_term[it->first] );
+          children.push_back( c );
+          Trace("cegqi-si-apply-subs-debug") << "Add child : " << c << std::endl;
+        }
+        Node nret = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children );
+        nret = Rewriter::rewrite( nret );
+        //result is ( nret / pv_coeff )
+        return nret;
+      }else{
+        Trace("cegqi-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl;
+      }
+    }
+    // failed to apply the substitution
+    return Node::null();
+  }
+}
+
+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;
+  //add rho value
+  //get the value of c*e
+  Node ceValue = me;
+  Node new_theta = theta;
+  if( !c.isNull() ){
+    ceValue = NodeManager::currentNM()->mkNode( MULT, ceValue, c );
+    ceValue = Rewriter::rewrite( ceValue );
+    if( new_theta.isNull() ){
+      new_theta = c;
+    }else{
+      new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, c );
+      new_theta = Rewriter::rewrite( new_theta );
+    }
+    Trace("cbqi-bound2") << "...c*e = " << ceValue << std::endl;
+    Trace("cbqi-bound2") << "...theta = " << new_theta << std::endl;
+  }
+  if( !new_theta.isNull() ){
+    Node rho;
+    if( isLower ){
+      rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt );
+    }else{
+      rho = NodeManager::currentNM()->mkNode( MINUS, mt, ceValue );
+    }
+    rho = Rewriter::rewrite( rho );
+    Trace("cbqi-bound2") << "...rho = " << me << " - " << mt << " = " << rho << std::endl;
+    Trace("cbqi-bound2") << "..." << rho << " mod " << new_theta << " = ";
+    rho = NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, rho, new_theta );
+    rho = Rewriter::rewrite( rho );
+    Trace("cbqi-bound2") << rho << std::endl;
+    Kind rk = isLower ? PLUS : MINUS;
+    val = NodeManager::currentNM()->mkNode( rk, val, rho );
+    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;
+}
+
+bool CegInstantiator::check() {
+  if( d_qe->getTheoryEngine()->needCheck() ){
+    Trace("cegqi-engine") << "  CEGQI instantiator : wait until all ground theories are finished." << std::endl;
+    return false;
+  }
+  processAssertions();
+  for( unsigned r=0; r<2; r++ ){
+    SolvedForm sf;
+    SolvedForm ssf;
+    std::vector< Node > vars;
+    std::vector< int > btyp;
+    Node theta;
+    std::map< Node, Node > cons;
+    std::vector< Node > curr_var;
+    //try to add an instantiation
+    if( addInstantiation( sf, ssf, vars, btyp, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){
+      return true;
+    }
+  }
+  Trace("cegqi-engine") << "  WARNING : unable to find CEGQI single invocation instantiation." << std::endl;
+  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 collectTheoryIds( TypeNode tn, std::map< TypeNode, bool >& visited, std::vector< TheoryId >& tids ){
+  std::map< TypeNode, bool >::iterator itt = visited.find( tn );
+  if( itt==visited.end() ){
+    visited[tn] = true;
+    TheoryId tid = Theory::theoryOf( tn );
+    if( std::find( tids.begin(), tids.end(), tid )==tids.end() ){
+      tids.push_back( tid );
+    }
+    if( tn.isDatatype() ){
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+        for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
+          collectTheoryIds( TypeNode::fromType( ((SelectorType)dt[i][j].getType()).getRangeType() ), visited, tids );
+        }
+      }
+    }
+  }
+}
+
+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_type_eqc.clear();
+
+  eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
+  //to eliminate identified illegal terms
+  std::map< Node, Node > aux_subs;
+
+  //for each variable
+  std::vector< TheoryId > tids;
+  for( unsigned i=0; i<d_vars.size(); i++ ){
+    Node pv = d_vars[i];
+    TypeNode pvtn = pv.getType();
+    //collect relevant theories
+    std::map< TypeNode, bool > visited;
+    collectTheoryIds( pvtn, visited, tids );
+    //collect information about eqc
+    if( ee->hasTerm( pv ) ){
+      Node pvr = ee->getRepresentative( pv );
+      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;
+        }
+      }
+    }
+  }
+  //collect assertions for relevant theories
+  for( unsigned i=0; i<tids.size(); i++ ){
+    TheoryId tid = tids[i];
+    Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid );
+    if( theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid) ){
+      Trace("cbqi-proc") << "Collect assertions from theory " << 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;
+        Node atom = lit.getKind()==NOT ? lit[0] : lit;
+        if( d_is_nested_quant || std::find( d_ce_atoms.begin(), d_ce_atoms.end(), atom )!=d_ce_atoms.end() ){
+          d_curr_asserts[tid].push_back( lit );
+          Trace("cbqi-proc-debug") << "...add : " << lit << std::endl;
+        }else{
+          Trace("cbqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << 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 equivalence classes that correspond to relevant theories
+  Trace("cbqi-proc-debug") << "...collect typed equivalence classes" << std::endl;
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
+  while( !eqcs_i.isFinished() ){
+    Node r = *eqcs_i;
+    TypeNode rtn = r.getType();
+    TheoryId tid = Theory::theoryOf( rtn );
+    //if we care about the theory of this eqc
+    if( std::find( tids.begin(), tids.end(), tid )!=tids.end() ){
+      if( rtn.isInteger() || rtn.isReal() ){
+        rtn = rtn.getBaseType();
+      }
+      Trace("cbqi-proc-debug") << "...type eqc: " << r << std::endl;
+      d_curr_type_eqc[rtn].push_back( r );
+      if( d_curr_eqc.find( r )==d_curr_eqc.end() ){
+        Trace("cbqi-proc") << "Collect equivalence class " << r << std::endl;
+        Trace("cbqi-proc-debug") << "  ";
+        eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+        while( !eqc_i.isFinished() ){
+          Trace("cbqi-proc-debug") << *eqc_i << " ";
+          d_curr_eqc[r].push_back( *eqc_i );
+          ++eqc_i;
+        }
+        Trace("cbqi-proc-debug") << std::endl;
+      }
+    }
+    ++eqcs_i;
+  }
+  //construct substitution from auxiliary variable equalities (if e.g. ITE removal was applied to CE body of quantified formula)
+  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 );
+}
+
+Node CegInstantiator::getModelValue( Node n ) {
+  return d_qe->getModel()->getValue( n );
+}
+
+void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) {
+  if( n.getKind()==FORALL ){
+    d_is_nested_quant = true;
+  }else{
+    if( visited.find( n )==visited.end() ){
+      visited[n] = true;
+      if( TermDb::isBoolConnective( n.getKind() ) ){
+        for( unsigned i=0; i<n.getNumChildren(); i++ ){
+          collectCeAtoms( n[i], visited );
+        }
+      }else{
+        if( std::find( d_ce_atoms.begin(), d_ce_atoms.end(), n )==d_ce_atoms.end() ){
+          d_ce_atoms.push_back( n );
+        }
+      }
+    }
+  }
+}
+
+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;
+  }
+  //collect atoms from all lemmas: we will only do bounds coming from original body
+  d_is_nested_quant = false;
+  std::map< Node, bool > visited;
+  for( unsigned i=0; i<lems.size(); i++ ){
+    collectCeAtoms( lems[i], visited );
+  }
+}
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h
new file mode 100644
index 000000000..7dd6ef12b
--- /dev/null
+++ b/src/theory/quantifiers/ceg_instantiator.h
@@ -0,0 +1,135 @@
+/*********************                                                        */
+/*! \file ceg_instantiator.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief counterexample-guided quantifier instantiation
+ **/
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CEG_INSTANTIATOR_H
+#define __CVC4__CEG_INSTANTIATOR_H
+
+#include "theory/quantifiers_engine.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+
+namespace arith {
+  class TheoryArith;
+}
+
+namespace quantifiers {
+
+class CegqiOutput {
+public:
+  virtual ~CegqiOutput() {}
+  virtual bool addInstantiation( std::vector< Node >& subs ) = 0;
+  virtual bool isEligibleForInstantiation( Node n ) = 0;
+  virtual bool addLemma( Node lem ) = 0;
+};
+
+class CegInstantiator {
+private:
+  QuantifiersEngine * d_qe;
+  CegqiOutput * d_out;
+  //constants
+  Node d_zero;
+  Node d_one;
+  Node d_true;
+  bool d_use_vts_delta;
+  bool d_use_vts_inf;
+  //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< TypeNode, std::vector< Node > > d_curr_type_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;
+  //atoms of the CE lemma
+  bool d_is_nested_quant;
+  std::vector< Node > d_ce_atoms;
+private:
+  //collect atoms
+  void collectCeAtoms( Node n, std::map< Node, bool >& visited );
+  //for adding instantiations during check
+  void computeProgVars( Node n );
+  //solved form, involves substitution with coefficients
+  class SolvedForm {
+  public:
+    std::vector< Node > d_subs;
+    std::vector< Node > d_coeff;
+    std::vector< Node > d_has_coeff;
+    void copy( SolvedForm& sf ){
+      d_subs.insert( d_subs.end(), sf.d_subs.begin(), sf.d_subs.end() );
+      d_coeff.insert( d_coeff.end(), sf.d_coeff.begin(), sf.d_coeff.end() );
+      d_has_coeff.insert( d_has_coeff.end(), sf.d_has_coeff.begin(), sf.d_has_coeff.end() );
+    }
+    void push_back( Node pv, Node n, Node pv_coeff ){
+      d_subs.push_back( n );
+      d_coeff.push_back( pv_coeff );
+      if( !pv_coeff.isNull() ){
+        d_has_coeff.push_back( pv );
+      }
+    }
+    void pop_back( Node pv, Node n, Node pv_coeff ){
+      d_subs.pop_back();
+      d_coeff.pop_back();
+      if( !pv_coeff.isNull() ){
+        d_has_coeff.pop_back();
+      }
+    }
+  };
+  // effort=0 : do not use model value, 1: use model value, 2: one must use model value
+  bool addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
+                         std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
+                         std::map< Node, Node >& cons, std::vector< Node >& curr_var );
+  bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
+                            std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
+                            std::map< Node, Node >& cons, std::vector< Node >& curr_var );
+  bool addInstantiationCoeff( SolvedForm& sf,
+                              std::vector< Node >& vars, std::vector< int >& btyp,
+                              unsigned j, std::map< Node, Node >& cons );
+  bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons );
+  Node constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons );
+  Node applySubstitution( Node n, SolvedForm& sf, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ) {
+    return applySubstitution( n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, vars, pv_coeff, try_coeff );
+  }
+  Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff,
+                          std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true );
+  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 );
+  //get model value
+  Node getModelValue( Node n );
+public:
+  CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true );
+  //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 );
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 1f4d398be..39e7abd3b 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -20,6 +20,7 @@
 #include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/trigger.h"
 #include "util/ite_removal.h"
 
 using namespace std;
@@ -31,1377 +32,145 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::arith;
 
 #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 ) );
-  d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
-  d_true = NodeManager::currentNM()->mkConst( true );
-  d_is_nested_quant = false;
-}
-
-void CegInstantiator::computeProgVars( Node n ){
-  if( d_prog_var.find( n )==d_prog_var.end() ){
-    d_prog_var[n].clear();
-    if( std::find( d_vars.begin(), d_vars.end(), n )!=d_vars.end() ){
-      d_prog_var[n][n] = true;
-    }else if( !d_out->isEligibleForInstantiation( n ) ){
-      d_inelig[n] = true;
-      return;
-    }
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      computeProgVars( n[i] );
-      if( d_inelig.find( n[i] )!=d_inelig.end() ){
-        d_inelig[n] = true;
-        return;
-      }
-      for( std::map< Node, bool >::iterator it = d_prog_var[n[i]].begin(); it != d_prog_var[n[i]].end(); ++it ){
-        d_prog_var[n][it->first] = true;
-      }
-      //selectors applied to program variables are also variables
-      if( n.getKind()==APPLY_SELECTOR_TOTAL && d_prog_var[n].find( n[0] )!=d_prog_var[n].end() ){
-        d_prog_var[n][n] = true;
-      }
-    }
-  }
-}
-
-bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
-                                        std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
-                                        std::map< Node, Node >& cons, std::vector< Node >& curr_var ){
-  if( i==d_vars.size() ){
-    //solved for all variables, now construct instantiation
-    if( !sf.d_has_coeff.empty() ){
-      if( options::cbqiSymLia() ){
-        //use symbolic solved forms
-        SolvedForm csf;
-        csf.copy( ssf );
-        return addInstantiationCoeff( csf, vars, btyp, 0, cons );
-      }else{
-        return addInstantiationCoeff( sf, vars, btyp, 0, cons );
-      }
-    }else{
-      return addInstantiation( sf.d_subs, vars, cons );
-    }
-  }else{
-    std::map< Node, std::map< Node, bool > > subs_proc;
-    //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]];
-    bool is_cv = false;
-    Node pv;
-    if( curr_var.empty() ){
-      pv = d_vars[i];
-    }else{
-      pv = curr_var.back();
-      is_cv = true;
-    }
-    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;
-    }
-    Node pvr = pv;
-    if( d_qe->getMasterEqualityEngine()->hasTerm( pv ) ){
-      pvr = d_qe->getMasterEqualityEngine()->getRepresentative( pv );
-    }
-
-    //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
-      Trace("cbqi-inst-debug") << "[1] try based on equivalence class." << std::endl;
-      std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( pvr );
-      if( it_eqc!=d_curr_eqc.end() ){
-        Trace("cbqi-inst-debug2") << "...eqc has size " << it_eqc->second.size() << std::endl;
-        for( unsigned k=0; k<it_eqc->second.size(); k++ ){
-          Node n = it_eqc->second[k];
-          if( n!=pv ){
-            Trace("cbqi-inst-debug") << "...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
-            if( d_inelig.find( n )==d_inelig.end() ){
-              Node ns;
-              Node pv_coeff;  //coefficient of pv in the equality we solve (null is 1)
-              bool proc = false;
-              if( !d_prog_var[n].empty() ){
-                ns = applySubstitution( n, sf, vars, pv_coeff, false );
-                if( !ns.isNull() ){
-                  computeProgVars( ns );
-                  //substituted version must be new and cannot contain pv
-                  proc = subs_proc[pv_coeff].find( ns )==subs_proc[pv_coeff].end() && d_prog_var[ns].find( pv )==d_prog_var[ns].end();
-                }
-              }else{
-                ns = n;
-                proc = true;
-              }
-              if( proc ){
-                //try the substitution
-                subs_proc[ns][pv_coeff] = true;
-                if( addInstantiationInc( ns, pv, pv_coeff, 0, sf, ssf, vars,  btyp, theta, i, effort, cons, curr_var ) ){
-                  return true;
-                }
-              }
-            }
-          }
+InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) : InstStrategy( qe ){
+  
+}
+
+void InstStrategyCbqi::processResetInstantiationRound( Theory::Effort effort ) {
+  d_cbqi_set_quant_inactive = false;
+  //check if any cbqi lemma has not been added yet
+  for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+    Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+    //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
+    if( d_quantEngine->hasOwnership( q, d_quantEngine->getInstantiationEngine() ) && doCbqi( q ) ){
+      if( !hasAddedCbqiLemma( q ) ){
+        d_added_cbqi_lemma[q] = true;
+        Trace("cbqi") << "Do cbqi for " << q << std::endl;
+        //add cbqi lemma
+        //get the counterexample literal
+        Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
+        Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
+        if( !ceBody.isNull() ){
+          //add counterexample lemma
+          Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() );
+          //require any decision on cel to be phase=true
+          d_quantEngine->addRequirePhase( ceLit, true );
+          Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
+          //add counterexample lemma
+          lem = Rewriter::rewrite( lem );
+          Trace("cbqi") << "Counterexample lemma : " << lem << std::endl;
+          registerCounterexampleLemma( q, lem );
         }
-      }else{
-        Trace("cbqi-inst-debug2") << "...eqc not found." << std::endl;
-      }
-
-      //[2] : we can solve an equality for pv
-      if( pvtn.isInteger() || pvtn.isReal() ){
-        ///iterate over equivalence classes to find cases where we can solve for the variable
-        TypeNode pvtnb = pvtn.getBaseType();
-        Trace("cbqi-inst-debug") << "[2] try based on solving arithmetic equivalence classes." << std::endl;
-        for( unsigned k=0; k<d_curr_type_eqc[pvtnb].size(); k++ ){
-          Node r = d_curr_type_eqc[pvtnb][k];
-          std::map< Node, std::vector< Node > >::iterator it_reqc = d_curr_eqc.find( r );
-          std::vector< Node > lhs;
-          std::vector< bool > lhs_v;
-          std::vector< Node > lhs_coeff;
-          Assert( it_reqc!=d_curr_eqc.end() );
-          for( unsigned kk=0; kk<it_reqc->second.size(); kk++ ){
-            Node n = it_reqc->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, sf, vars, pv_coeff );
-                if( !ns.isNull() ){
-                  computeProgVars( ns );
-                }
-              }else{
-                ns = n;
-              }
-              if( !ns.isNull() ){
-                bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end();
-                Trace("cbqi-inst-debug2") << "... " << ns << " has var " << pv << " : " << hasVar << std::endl;
-                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") << "... " << 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 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];
-                        if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
-                          subs_proc[val][veq_c] = true;
-                          if( addInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
-                            return true;
-                          }
-                        }
-                      }
-                    }
-                  }
-                }
-                lhs.push_back( ns );
-                lhs_v.push_back( hasVar );
-                lhs_coeff.push_back( pv_coeff );
-              }else{
-                Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible after substitution." << std::endl;
-              }
+      //set inactive the quantified formulas whose CE literals are asserted false  
+      }else if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
+        Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl;
+        Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
+        bool value;
+        if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){
+          Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl;
+          if( !value ){
+            if( d_quantEngine->getValuation().isDecision( cel ) ){
+              Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
             }else{
-              Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible." << std::endl;
-            }
-          }
-        }
-      }else if( pvtn.isDatatype() ){
-        Trace("cbqi-inst-debug") << "[2] try based on constructors in equivalence class." << std::endl;
-        //look in equivalence class for a constructor
-        if( it_eqc!=d_curr_eqc.end() ){
-          for( unsigned k=0; k<it_eqc->second.size(); k++ ){
-            Node n = it_eqc->second[k];
-            if( n.getKind()==APPLY_CONSTRUCTOR ){
-              Trace("cbqi-inst-debug") << "... " << i << "...try based on constructor term " << n << std::endl;
-              cons[pv] = n.getOperator();
-              const Datatype& dt = ((DatatypeType)(pvtn).toType()).getDatatype();
-              unsigned cindex = Datatype::indexOf( n.getOperator().toExpr() );
-              if( is_cv ){
-                curr_var.pop_back();
-              }
-              //now must solve for selectors applied to pv
-              for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){
-                curr_var.push_back( NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ) );
-              }
-              if( addInstantiation( sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
-                return true;
-              }else{
-                //cleanup
-                cons.erase( pv );
-                Assert( curr_var.size()>=dt[cindex].getNumArgs() );
-                for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){
-                  curr_var.pop_back();
-                }
-                if( is_cv ){
-                  curr_var.push_back( pv );
-                }
-                break;
-              }
+              d_quantEngine->getModel()->setQuantifierActive( q, false );
+              d_cbqi_set_quant_inactive = true;
             }
           }
         }else{
-          Trace("cbqi-inst-debug2") << "... " << i << " does not have an eqc." << std::endl;
-        }
-      }
-
-      //[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< 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() );
-        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;
-            if( tid==THEORY_ARITH ){
-              //arithmetic inequalities and disequalities
-              if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol ) ){
-                Assert( atom[0].getType().isInteger() || atom[0].getType().isReal() );
-                Assert( atom.getKind()!=GEQ || atom[1].isConst() );
-                Node atom_lhs;
-                Node atom_rhs;
-                if( atom.getKind()==GEQ ){
-                  atom_lhs = atom[0];
-                  atom_rhs = atom[1];
-                }else{
-                  atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] );
-                  atom_lhs = Rewriter::rewrite( atom_lhs );
-                  atom_rhs = d_zero;
-                }
-
-                computeProgVars( atom_lhs );
-                //must be an eligible term
-                if( d_inelig.find( atom_lhs )==d_inelig.end() ){
-                  //apply substitution to LHS of atom
-                  if( !d_prog_var[atom_lhs].empty() ){
-                    Node atom_lhs_coeff;
-                    atom_lhs = applySubstitution( atom_lhs, sf, vars, atom_lhs_coeff );
-                    if( !atom_lhs.isNull() ){
-                      computeProgVars( atom_lhs );
-                      if( !atom_lhs_coeff.isNull() ){
-                        atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) );
-                      }
-                    }
-                  }
-                  //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( !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] );
-                          }
-                        }
-                      }
-
-                      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 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() ){
-                                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{
-                            bool is_upper = ( r==0 );
-                            if( options::cbqiModel() ){
-                              // 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 );
-                              }
-                            }
-                            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{
-                                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, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
-                                return true;
-                              }
-                            }
-                          }
-                        }
-                      }
-                    }
-                  }
-                }
-              }
-            }
-          }
-        }
-      }
-      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[3];
-          //try optimal bounds
-          for( unsigned r=0; r<2; r++ ){
-            int rr = upper_first ? (1-r) : r;
-            if( mbp_bounds[rr].empty() ){
-              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( 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(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
-                  return true;
-                }
-              }
-            }else{
-              Trace("cbqi-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << pvtn << ") : " << std::endl;
-              int best = -1;
-              Node best_bound_value[3];
-              for( unsigned j=0; j<mbp_bounds[rr].size(); j++ ){
-                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 = ";
-                }
-                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 ){
-                  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 << " : ";
-                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 = 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, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
-                      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, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
-                  return true;
-                }
-              }
-            }
-          }
-#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], 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, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
-                      return true;
-                    }
-                  }
-                }
-              }
-            }
-          }
-        }
-      }
-    }
-
-    //[4] resort to using value in model
-    // do so if we are in effort=1, or if the variable is boolean, or if we are solving for a subfield of a datatype
-    if( effort>0 || pvtn.isBoolean() || !curr_var.empty() ){
-      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.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() );
-#endif
-      if( addInstantiationInc( mv, pv, pv_coeff_m, 0, sf, ssf, vars, btyp, theta, i, new_effort, cons, curr_var ) ){
-        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, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
-                                           std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
-                                           std::map< Node, Node >& cons, std::vector< Node >& curr_var ) {
-  if( Trace.isOn("cbqi-inst") ){
-    for( unsigned j=0; j<sf.d_subs.size(); j++ ){
-      Trace("cbqi-inst") << " ";
-    }
-    Trace("cbqi-inst") << sf.d_subs.size() << ": ";
-    if( !pv_coeff.isNull() ){
-      Trace("cbqi-inst") << pv_coeff << " * ";
-    }
-    Trace("cbqi-inst") << pv << " -> " << n << std::endl;
-  }
-  //must ensure variables have been computed for n
-  computeProgVars( n );
-
-  //substitute into previous substitutions, when applicable
-  std::vector< Node > a_subs;
-  a_subs.push_back( n );
-  std::vector< Node > a_var;
-  a_var.push_back( pv );
-  std::vector< Node > a_coeff;
-  std::vector< Node > a_has_coeff;
-  if( !pv_coeff.isNull() ){
-    a_coeff.push_back( pv_coeff );
-    a_has_coeff.push_back( pv );
-  }
-  bool success = true;
-  std::map< int, Node > prev_subs;
-  std::map< int, Node > prev_coeff;
-  std::map< int, Node > prev_sym_subs;
-  std::vector< Node > new_has_coeff;
-  for( unsigned j=0; j<sf.d_subs.size(); j++ ){
-    Assert( d_prog_var.find( sf.d_subs[j] )!=d_prog_var.end() );
-    if( d_prog_var[sf.d_subs[j]].find( pv )!=d_prog_var[sf.d_subs[j]].end() ){
-      prev_subs[j] = sf.d_subs[j];
-      TNode tv = pv;
-      TNode ts = n;
-      Node a_pv_coeff;
-      Node new_subs = applySubstitution( sf.d_subs[j], a_subs, a_coeff, a_has_coeff, a_var, a_pv_coeff, true );
-      if( !new_subs.isNull() ){
-        sf.d_subs[j] = new_subs;
-        if( !a_pv_coeff.isNull() ){
-          prev_coeff[j] = sf.d_coeff[j];
-          if( sf.d_coeff[j].isNull() ){
-            Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), vars[j] )==sf.d_has_coeff.end() );
-            //now has coefficient
-            new_has_coeff.push_back( vars[j] );
-            sf.d_has_coeff.push_back( vars[j] );
-            sf.d_coeff[j] = a_pv_coeff;
-          }else{
-            sf.d_coeff[j] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[j], a_pv_coeff ) );
-          }
+          Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl;
         }
-        if( sf.d_subs[j]!=prev_subs[j] ){
-          computeProgVars( sf.d_subs[j] );
-        }
-      }else{
-        Trace("cbqi-inst-debug") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl;
-        success = false;
-        break;
-      }
-    }
-    if( options::cbqiSymLia() && pv_coeff.isNull() ){
-      //apply simple substitutions also to sym_subs
-      prev_sym_subs[j] = ssf.d_subs[j];
-      ssf.d_subs[j] = ssf.d_subs[j].substitute( a_var.begin(), a_var.end(), a_subs.begin(), a_subs.end() );
-      ssf.d_subs[j] = Rewriter::rewrite( ssf.d_subs[j] );
-    }
-  }
-  if( success ){
-    vars.push_back( pv );
-    btyp.push_back( bt );
-    sf.push_back( pv, n, pv_coeff );
-    ssf.push_back( pv, n, pv_coeff );
-    Node new_theta = theta;
-    if( !pv_coeff.isNull() ){
-      if( new_theta.isNull() ){
-        new_theta = pv_coeff;
-      }else{
-        new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, pv_coeff );
-        new_theta = Rewriter::rewrite( new_theta );
-      }
-    }
-    bool is_cv = false;
-    if( !curr_var.empty() ){
-      Assert( curr_var.back()==pv );
-      curr_var.pop_back();
-      is_cv = true;
-    }
-    success = addInstantiation( sf, ssf, vars, btyp, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var );
-    if( !success ){
-      if( is_cv ){
-        curr_var.push_back( pv );
       }
-      sf.pop_back( pv, n, pv_coeff );
-      ssf.pop_back( pv, n, pv_coeff );
-      vars.pop_back();
-      btyp.pop_back();
     }
   }
-  if( success ){
-    return true;
-  }else{
-    //revert substitution information
-    for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){
-      sf.d_subs[it->first] = it->second;
-    }
-    for( std::map< int, Node >::iterator it = prev_coeff.begin(); it != prev_coeff.end(); it++ ){
-      sf.d_coeff[it->first] = it->second;
-    }
-    for( unsigned i=0; i<new_has_coeff.size(); i++ ){
-      sf.d_has_coeff.pop_back();
-    }
-    for( std::map< int, Node >::iterator it = prev_sym_subs.begin(); it != prev_sym_subs.end(); it++ ){
-      ssf.d_subs[it->first] = it->second;
-    }
-    return false;
-  }
 }
 
-bool CegInstantiator::addInstantiationCoeff( SolvedForm& sf, std::vector< Node >& vars, std::vector< int >& btyp,
-                                             unsigned j, std::map< Node, Node >& cons ) {
-
-
-  if( j==sf.d_has_coeff.size() ){
-    return addInstantiation( sf.d_subs, vars, cons );
-  }else{
-    Assert( std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )!=vars.end() );
-    unsigned index = std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )-vars.begin();
-    Node prev = sf.d_subs[index];
-    Assert( !sf.d_coeff[index].isNull() );
-    Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_coeff[index] << " * " << vars[index] << " = " << sf.d_subs[index] << std::endl;
-    Assert( vars[index].getType().isInteger() );
-    //must ensure that divisibility constraints are met
-    //solve updated rewritten equality for vars[index], if coefficient is one, then we are successful
-    Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[index], vars[index] );
-    Node eq_rhs = sf.d_subs[index];
-    Node eq = eq_lhs.eqNode( eq_rhs );
-    eq = Rewriter::rewrite( eq );
-    Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl;
-    std::map< Node, Node > msum;
-    if( QuantArith::getMonomialSumLit( eq, msum ) ){
-      Node veq;
-      if( QuantArith::isolate( vars[index], msum, veq, EQUAL, true )!=0 ){
-        Node veq_c;
-        if( veq[0]!=vars[index] ){
-          Node veq_v;
-          if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){
-            Assert( veq_v==vars[index] );
-          }
-        }
-        sf.d_subs[index] = veq[1];
-        if( !veq_c.isNull() ){
-          sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c );
-          Trace("cbqi-inst-debug") << "...bound type is : " << btyp[index] << std::endl;
-          //intger division rounding up if from a lower bound
-          if( btyp[index]==1 && options::cbqiRoundUpLowerLia() ){
-            sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index],
-              NodeManager::currentNM()->mkNode( ITE,
-                NodeManager::currentNM()->mkNode( EQUAL,
-                  NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ),
-                  d_zero ),
-                d_zero, d_one )
-            );
-          }
-        }
-        Trace("cbqi-inst-debug") << "...normalize integers : " << vars[index] << " -> " << sf.d_subs[index] << std::endl;
-        if( options::cbqiSymLia() ){
-          //must apply substitution to previous subs
-          std::vector< Node > curr_var;
-          std::vector< Node > curr_subs;
-          curr_var.push_back( vars[index] );
-          curr_subs.push_back( sf.d_subs[index] );
-          for( unsigned k=0; k<index; k++ ){
-            Node prevs = sf.d_subs[k];
-            sf.d_subs[k] = sf.d_subs[k].substitute( curr_var.begin(), curr_var.end(), curr_subs.begin(), curr_subs.end() );
-            if( prevs!=sf.d_subs[k] ){
-              Trace("cbqi-inst-debug2") << "      rewrite " << vars[k] << " -> " << prevs << " to ";
-              sf.d_subs[k] = Rewriter::rewrite( sf.d_subs[k] );
-              Trace("cbqi-inst-debug2") << sf.d_subs[k] << std::endl;
-            }
-          }
-        }
-        if( addInstantiationCoeff( sf, vars, btyp, j+1, cons ) ){
-          return true;
-        }
-      }
-    }
-    sf.d_subs[index] = prev;
-    Trace("cbqi-inst-debug") << "...failed." << std::endl;
-    return false;
-  }
+void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){
+  Trace("cbqi-debug") << "Counterexample lemma  : " << lem << std::endl;
+  d_quantEngine->addLemma( lem, false );
 }
 
-bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ) {
-  if( vars.size()>d_vars.size() ){
-    Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl;
-    std::map< Node, Node > subs_map;
-    for( unsigned i=0; i<subs.size(); i++ ){
-      subs_map[vars[i]] = subs[i];
-    }
-    subs.clear();
-    for( unsigned i=0; i<d_vars.size(); i++ ){
-      Node n = constructInstantiation( d_vars[i], subs_map, cons );
-      Trace("cbqi-inst-debug") << "  " << d_vars[i] << " -> " << n << std::endl;
-      subs.push_back( n );
-    }
-  }
-  bool ret = d_out->addInstantiation( subs );
-#ifdef MBP_STRICT_ASSERTIONS
-  Assert( ret );
-#endif
-  return ret;
-}
-
-Node CegInstantiator::constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons ) {
-  std::map< Node, Node >::iterator it = subs_map.find( n );
-  if( it!=subs_map.end() ){
-    return it->second;
-  }else{
-    it = cons.find( n );
-    Assert( it!=cons.end() );
-    std::vector< Node > children;
-    children.push_back( it->second );
-    const Datatype& dt = Datatype::datatypeOf( it->second.toExpr() );
-    unsigned cindex = Datatype::indexOf( it->second.toExpr() );
-    for( unsigned i=0; i<dt[cindex].getNumArgs(); i++ ){
-      Node nn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][i].getSelector() ), n );
-      Node nc = constructInstantiation( nn, subs_map, cons );
-      children.push_back( nc );
-    }
-    return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
-  }
-}
-
-Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff,
-                                         std::vector< Node >& vars, 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;
-  if( !has_coeff.empty() ){
-    for( std::map< Node, bool >::iterator it = d_prog_var[n].begin(); it != d_prog_var[n].end(); ++it ){
-      if( std::find( has_coeff.begin(), has_coeff.end(), it->first )!=has_coeff.end() ){
-        req_coeff = true;
-        break;
-      }
-    }
-  }
-  if( !req_coeff ){
-    Node nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-    if( n!=nret ){
-      nret = Rewriter::rewrite( nret );
-    }
-    //result is nret
-    return nret;
-  }else{
-    if( try_coeff ){
-      //must convert to monomial representation
-      std::map< Node, Node > msum;
-      if( QuantArith::getMonomialSum( n, msum ) ){
-        std::map< Node, Node > msum_coeff;
-        std::map< Node, Node > msum_term;
-        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
-          //check if in substitution
-          std::vector< Node >::iterator its = std::find( vars.begin(), vars.end(), it->first );
-          if( its!=vars.end() ){
-            int index = its-vars.begin();
-            if( coeff[index].isNull() ){
-              //apply substitution
-              msum_term[it->first] = subs[index];
-            }else{
-              //apply substitution, multiply to ensure no divisibility conflict
-              msum_term[it->first] = subs[index];
-              //relative coefficient
-              msum_coeff[it->first] = coeff[index];
-              if( pv_coeff.isNull() ){
-                pv_coeff = coeff[index];
-              }else{
-                pv_coeff = NodeManager::currentNM()->mkNode( MULT, pv_coeff, coeff[index] );
-              }
-            }
-          }else{
-            msum_term[it->first] = it->first;
-          }
-        }
-        //make sum with normalized coefficient
-        Assert( !pv_coeff.isNull() );
-        pv_coeff = Rewriter::rewrite( pv_coeff );
-        Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_coeff << std::endl;
-        std::vector< Node > children;
-        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
-          Node c_coeff;
-          if( !msum_coeff[it->first].isNull() ){
-            c_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkConst( pv_coeff.getConst<Rational>() / msum_coeff[it->first].getConst<Rational>() ) );
-          }else{
-            c_coeff = pv_coeff;
-          }
-          if( !it->second.isNull() ){
-            c_coeff = NodeManager::currentNM()->mkNode( MULT, c_coeff, it->second );
-          }
-          Node c = NodeManager::currentNM()->mkNode( MULT, c_coeff, msum_term[it->first] );
-          children.push_back( c );
-          Trace("cegqi-si-apply-subs-debug") << "Add child : " << c << std::endl;
-        }
-        Node nret = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children );
-        nret = Rewriter::rewrite( nret );
-        //result is ( nret / pv_coeff )
-        return nret;
+bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ){
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    if( n.getKind()!=INST_CONSTANT && TermDb::hasInstConstAttr( n ) ){
+      if( !inst::Trigger::isCbqiKind( n.getKind() ) ){
+        Trace("cbqi-debug2") << "Non-cbqi kind : " << n.getKind() << " in " << n  << std::endl;
+        return true;
+      }else if( n.getKind()==MULT && ( n.getNumChildren()!=2 || !n[0].isConst() ) ){
+        Trace("cbqi-debug2") << "Non-linear arithmetic : " << n << std::endl;
+        return true;
       }else{
-        Trace("cegqi-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl;
-      }
-    }
-    // failed to apply the substitution
-    return Node::null();
-  }
-}
-
-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;
-  //add rho value
-  //get the value of c*e
-  Node ceValue = me;
-  Node new_theta = theta;
-  if( !c.isNull() ){
-    ceValue = NodeManager::currentNM()->mkNode( MULT, ceValue, c );
-    ceValue = Rewriter::rewrite( ceValue );
-    if( new_theta.isNull() ){
-      new_theta = c;
-    }else{
-      new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, c );
-      new_theta = Rewriter::rewrite( new_theta );
-    }
-    Trace("cbqi-bound2") << "...c*e = " << ceValue << std::endl;
-    Trace("cbqi-bound2") << "...theta = " << new_theta << std::endl;
-  }
-  if( !new_theta.isNull() ){
-    Node rho;
-    if( isLower ){
-      rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt );
-    }else{
-      rho = NodeManager::currentNM()->mkNode( MINUS, mt, ceValue );
-    }
-    rho = Rewriter::rewrite( rho );
-    Trace("cbqi-bound2") << "...rho = " << me << " - " << mt << " = " << rho << std::endl;
-    Trace("cbqi-bound2") << "..." << rho << " mod " << new_theta << " = ";
-    rho = NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, rho, new_theta );
-    rho = Rewriter::rewrite( rho );
-    Trace("cbqi-bound2") << rho << std::endl;
-    Kind rk = isLower ? PLUS : MINUS;
-    val = NodeManager::currentNM()->mkNode( rk, val, rho );
-    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;
-}
-
-bool CegInstantiator::check() {
-  if( d_qe->getTheoryEngine()->needCheck() ){
-    Trace("cegqi-engine") << "  CEGQI instantiator : wait until all ground theories are finished." << std::endl;
-    return false;
-  }
-  processAssertions();
-  for( unsigned r=0; r<2; r++ ){
-    SolvedForm sf;
-    SolvedForm ssf;
-    std::vector< Node > vars;
-    std::vector< int > btyp;
-    Node theta;
-    std::map< Node, Node > cons;
-    std::vector< Node > curr_var;
-    //try to add an instantiation
-    if( addInstantiation( sf, ssf, vars, btyp, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){
-      return true;
-    }
-  }
-  Trace("cegqi-engine") << "  WARNING : unable to find CEGQI single invocation instantiation." << std::endl;
-  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++ ){
+          if( hasNonCbqiOperator( n[i], visited ) ){
+            return true;
           }
         }
       }
     }
-    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();
-    }
   }
+  return false;
 }
-
-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;
+bool InstStrategyCbqi::hasNonCbqiVariable( Node q ){
   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 collectTheoryIds( TypeNode tn, std::map< TypeNode, bool >& visited, std::vector< TheoryId >& tids ){
-  std::map< TypeNode, bool >::iterator itt = visited.find( tn );
-  if( itt==visited.end() ){
-    visited[tn] = true;
-    TheoryId tid = Theory::theoryOf( tn );
-    if( std::find( tids.begin(), tids.end(), tid )==tids.end() ){
-      tids.push_back( tid );
-    }
-    if( tn.isDatatype() ){
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-        for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
-          collectTheoryIds( TypeNode::fromType( ((SelectorType)dt[i][j].getType()).getRangeType() ), visited, tids );
+    TypeNode tn = q[0][i].getType();
+    if( !tn.isInteger() && !tn.isReal() && !tn.isBoolean() ){
+      if( options::cbqiSplx() ){
+        return true;
+      }else{
+        //datatypes supported in new implementation
+        if( !tn.isDatatype() ){
+          return true;
         }
       }
     }
   }
+  return false;
 }
 
-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_type_eqc.clear();
-
-  eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
-  //to eliminate identified illegal terms
-  std::map< Node, Node > aux_subs;
-
-  //for each variable
-  std::vector< TheoryId > tids;
-  for( unsigned i=0; i<d_vars.size(); i++ ){
-    Node pv = d_vars[i];
-    TypeNode pvtn = pv.getType();
-    //collect relevant theories
-    std::map< TypeNode, bool > visited;
-    collectTheoryIds( pvtn, visited, tids );
-    //collect information about eqc
-    if( ee->hasTerm( pv ) ){
-      Node pvr = ee->getRepresentative( pv );
-      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;
-        }
-      }
-    }
-  }
-  //collect assertions for relevant theories
-  for( unsigned i=0; i<tids.size(); i++ ){
-    TheoryId tid = tids[i];
-    Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid );
-    if( theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid) ){
-      Trace("cbqi-proc") << "Collect assertions from theory " << 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;
-        Node atom = lit.getKind()==NOT ? lit[0] : lit;
-        if( d_is_nested_quant || std::find( d_ce_atoms.begin(), d_ce_atoms.end(), atom )!=d_ce_atoms.end() ){
-          d_curr_asserts[tid].push_back( lit );
-          Trace("cbqi-proc-debug") << "...add : " << lit << std::endl;
-        }else{
-          Trace("cbqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << 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 equivalence classes that correspond to relevant theories
-  Trace("cbqi-proc-debug") << "...collect typed equivalence classes" << std::endl;
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
-  while( !eqcs_i.isFinished() ){
-    Node r = *eqcs_i;
-    TypeNode rtn = r.getType();
-    TheoryId tid = Theory::theoryOf( rtn );
-    //if we care about the theory of this eqc
-    if( std::find( tids.begin(), tids.end(), tid )!=tids.end() ){
-      if( rtn.isInteger() || rtn.isReal() ){
-        rtn = rtn.getBaseType();
-      }
-      Trace("cbqi-proc-debug") << "...type eqc: " << r << std::endl;
-      d_curr_type_eqc[rtn].push_back( r );
-      if( d_curr_eqc.find( r )==d_curr_eqc.end() ){
-        Trace("cbqi-proc") << "Collect equivalence class " << r << std::endl;
-        Trace("cbqi-proc-debug") << "  ";
-        eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
-        while( !eqc_i.isFinished() ){
-          Trace("cbqi-proc-debug") << *eqc_i << " ";
-          d_curr_eqc[r].push_back( *eqc_i );
-          ++eqc_i;
-        }
-        Trace("cbqi-proc-debug") << std::endl;
-      }
-    }
-    ++eqcs_i;
-  }
-  //construct substitution from auxiliary variable equalities (if e.g. ITE removal was applied to CE body of quantified formula)
-  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 );
+bool InstStrategyCbqi::doCbqi( Node q ){
+  std::map< Node, bool >::iterator it = d_do_cbqi.find( q );
+  if( it==d_do_cbqi.end() ){
+    bool ret = false;
+    Assert( options::cbqi() );
+    if( options::cbqiAll() ){
+      ret = true;
     }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() );
+      //if quantifier has a non-arithmetic variable, then do not use cbqi
+      //if quantifier has an APPLY_UF term, then do not use cbqi
+      Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
+      std::map< Node, bool > visited;
+      ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( cb, visited );
+    }
+    d_do_cbqi[q] = ret;
+    return ret;
+  }else{
+    return it->second;
   }
+}
 
-  //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] );
+Node InstStrategyCbqi::getNextDecisionRequest(){
+  // all counterexample literals that are not asserted
+  for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+    Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+    if( hasAddedCbqiLemma( q ) ){
+      Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
+      bool value;
+      if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){
+        Trace("cbqi-debug2") << "CBQI: get next decision " << cel << std::endl;
+        return cel;
       }
     }
-    it->second.clear();
-    it->second.insert( it->second.end(), new_eqc.begin(), new_eqc.end() );
   }
+  return Node::null();
 }
 
-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::collectCeAtoms( Node n, std::map< Node, bool >& visited ) {
-  if( n.getKind()==FORALL ){
-    d_is_nested_quant = true;
-  }else{
-    if( visited.find( n )==visited.end() ){
-      visited[n] = true;
-      if( TermDb::isBoolConnective( n.getKind() ) ){
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          collectCeAtoms( n[i], visited );
-        }
-      }else{
-        if( std::find( d_ce_atoms.begin(), d_ce_atoms.end(), n )==d_ce_atoms.end() ){
-          d_ce_atoms.push_back( n );
-        }
-      }
-    }
-  }
-}
-
-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;
-  }
-  //collect atoms from lem[0]: we will only do bounds coming from original body
-  d_is_nested_quant = false;
-  std::map< Node, bool > visited;
-  collectCeAtoms( lems[0], visited );
-}
 
 //old implementation
 
-InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) :
-    InstStrategy( ie ), d_th( th ), d_counter( 0 ){
+InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) : InstStrategyCbqi( ie ), d_th( th ), d_counter( 0 ){
   d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) );
   d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
 }
@@ -1465,6 +234,7 @@ void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort
   Debug("quant-arith-debug") << std::endl;
   debugPrint( "quant-arith-debug" );
   d_counter++;
+  InstStrategyCbqi::processResetInstantiationRound( effort );
 }
 
 void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder<>& t ){
@@ -1494,89 +264,91 @@ void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder<
 }
 
 int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
-  if( e<1 ){
-    return STATUS_UNFINISHED;
-  }else if( e==1 ){
-    if( d_quantActive.find( f )!=d_quantActive.end() ){
-      //the point instantiation
-      InstMatch m_point( f );
-      bool m_point_valid = true;
-      int lem = 0;
-      //scan over all instantiation rows
-      for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
-        Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
-        Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl;
-        for( int j=0; j<(int)d_instRows[ic].size(); j++ ){
-          ArithVar x = d_instRows[ic][j];
-          if( !d_ceTableaux[ic][x].empty() ){
-            if( Debug.isOn("quant-arith-simplex") ){
-              Debug("quant-arith-simplex") << "--- Check row " << ic << " " << x << std::endl;
-              Debug("quant-arith-simplex") << "  ";
-              for( std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); it != d_ceTableaux[ic][x].end(); ++it ){
-                if( it!=d_ceTableaux[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
-                Debug("quant-arith-simplex") << it->first << " * " << it->second;
-              }
-              Debug("quant-arith-simplex") << " = ";
-              Node v = getTableauxValue( x, false );
-              Debug("quant-arith-simplex") << v << std::endl;
-              Debug("quant-arith-simplex") << "  term : " << d_tableaux_term[ic][x] << std::endl;
-              Debug("quant-arith-simplex") << "  ce-term : ";
-              for( std::map< Node, Node >::iterator it = d_tableaux_ce_term[ic][x].begin(); it != d_tableaux_ce_term[ic][x].end(); it++ ){
-                if( it!=d_tableaux_ce_term[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
-                Debug("quant-arith-simplex") << it->first << " * " << it->second;
-              }
-              Debug("quant-arith-simplex") << std::endl;
-            }
-            //instantiation row will be A*e + B*t = beta,
-            // where e is a vector of terms , and t is vector of ground terms.
-            // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
-            // We will construct the term ( beta - B*t)/coeff to use for e_i.
-            InstMatch m( f );
-            for( unsigned k=0; k<f[0].getNumChildren(); k++ ){
-              if( f[0][k].getType().isInteger() ){
-                m.setValue( k, d_zero );
+  if( doCbqi( f ) ){
+    if( e<1 ){
+      return STATUS_UNFINISHED;
+    }else if( e==1 ){
+      if( d_quantActive.find( f )!=d_quantActive.end() ){
+        //the point instantiation
+        InstMatch m_point( f );
+        bool m_point_valid = true;
+        int lem = 0;
+        //scan over all instantiation rows
+        for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
+          Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
+          Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl;
+          for( int j=0; j<(int)d_instRows[ic].size(); j++ ){
+            ArithVar x = d_instRows[ic][j];
+            if( !d_ceTableaux[ic][x].empty() ){
+              if( Debug.isOn("quant-arith-simplex") ){
+                Debug("quant-arith-simplex") << "--- Check row " << ic << " " << x << std::endl;
+                Debug("quant-arith-simplex") << "  ";
+                for( std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); it != d_ceTableaux[ic][x].end(); ++it ){
+                  if( it!=d_ceTableaux[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
+                  Debug("quant-arith-simplex") << it->first << " * " << it->second;
+                }
+                Debug("quant-arith-simplex") << " = ";
+                Node v = getTableauxValue( x, false );
+                Debug("quant-arith-simplex") << v << std::endl;
+                Debug("quant-arith-simplex") << "  term : " << d_tableaux_term[ic][x] << std::endl;
+                Debug("quant-arith-simplex") << "  ce-term : ";
+                for( std::map< Node, Node >::iterator it = d_tableaux_ce_term[ic][x].begin(); it != d_tableaux_ce_term[ic][x].end(); it++ ){
+                  if( it!=d_tableaux_ce_term[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
+                  Debug("quant-arith-simplex") << it->first << " * " << it->second;
+                }
+                Debug("quant-arith-simplex") << std::endl;
               }
-            }
-            //By default, choose the first instantiation constant to be e_i.
-            Node var = d_ceTableaux[ic][x].begin()->first;
-            //if it is integer, we need to find variable with coefficent +/- 1
-            if( var.getType().isInteger() ){
-              std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin();
-              while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){
-                ++it;
-                if( it==d_ceTableaux[ic][x].end() ){
-                  var = Node::null();
-                }else{
-                  var = it->first;
+              //instantiation row will be A*e + B*t = beta,
+              // where e is a vector of terms , and t is vector of ground terms.
+              // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
+              // We will construct the term ( beta - B*t)/coeff to use for e_i.
+              InstMatch m( f );
+              for( unsigned k=0; k<f[0].getNumChildren(); k++ ){
+                if( f[0][k].getType().isInteger() ){
+                  m.setValue( k, d_zero );
                 }
               }
-              //Otherwise, try one that divides all ground term coefficients?
-              //  Might be futile, if rewrite ensures gcd of coeffs is 1.
-            }
-            if( !var.isNull() ){
-              //add to point instantiation if applicable
-              if( d_tableaux_ce_term[ic][x].empty() && d_tableaux_term[ic][x]==d_zero ){
-                Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl;
-                Node v = getTableauxValue( x, false );
-                if( !var.getType().isInteger() || v.getType().isInteger() ){
-                  m_point.setValue( i, v );
-                }else{
-                  m_point_valid = false;
+              //By default, choose the first instantiation constant to be e_i.
+              Node var = d_ceTableaux[ic][x].begin()->first;
+              //if it is integer, we need to find variable with coefficent +/- 1
+              if( var.getType().isInteger() ){
+                std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin();
+                while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){
+                  ++it;
+                  if( it==d_ceTableaux[ic][x].end() ){
+                    var = Node::null();
+                  }else{
+                    var = it->first;
+                  }
                 }
+                //Otherwise, try one that divides all ground term coefficients?
+                //  Might be futile, if rewrite ensures gcd of coeffs is 1.
               }
-              Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
-              if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){
-                lem++;
+              if( !var.isNull() ){
+                //add to point instantiation if applicable
+                if( d_tableaux_ce_term[ic][x].empty() && d_tableaux_term[ic][x]==d_zero ){
+                  Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl;
+                  Node v = getTableauxValue( x, false );
+                  if( !var.getType().isInteger() || v.getType().isInteger() ){
+                    m_point.setValue( i, v );
+                  }else{
+                    m_point_valid = false;
+                  }
+                }
+                Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
+                if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){
+                  lem++;
+                }
+              }else{
+                Debug("quant-arith-simplex") << "Could not find var." << std::endl;
               }
-            }else{
-              Debug("quant-arith-simplex") << "Could not find var." << std::endl;
             }
           }
         }
-      }
-      if( lem==0 && m_point_valid ){
-        if( d_quantEngine->addInstantiation( f, m_point ) ){
-          Debug("quant-arith-simplex") << "...added point instantiation." << std::endl;
+        if( lem==0 && m_point_valid ){
+          if( d_quantEngine->addInstantiation( f, m_point ) ){
+            Debug("quant-arith-simplex") << "...added point instantiation." << std::endl;
+          }
         }
       }
     }
@@ -1623,7 +395,7 @@ void InstStrategySimplex::debugPrint( const char* c ){
   }
   Debug(c) << std::endl;
 
-  for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+  for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
     Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
     Debug(c) << f << std::endl;
     Debug(c) << "   Inst constants: ";
@@ -1733,44 +505,48 @@ bool CegqiOutputInstStrategy::addLemma( Node lem ) {
 }
 
 
-InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategy( qe ) {
+InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategyCbqi( qe ) {
   d_out = new CegqiOutputInstStrategy( this );
   d_small_const = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) );
 }
 
 void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) {
   d_check_vts_lemma_lc = true;
+  InstStrategyCbqi::processResetInstantiationRound( effort );
 }
 
 int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
-  if( e<1 ){
-    return STATUS_UNFINISHED;
-  }else if( e==1 ){
-    CegInstantiator * cinst = getInstantiator( f );
-    Trace("inst-alg") << "-> Run cegqi for " << f << std::endl;
-    d_curr_quant = f;
-    bool addedLemma = cinst->check();
-    d_curr_quant = Node::null();
-    return addedLemma ? STATUS_UNKNOWN : STATUS_UNFINISHED;
-  }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 );
-      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 );
+  //can only be called at last call, since it is model-based
+  if( doCbqi( f ) && effort==Theory::EFFORT_LAST_CALL ){
+    if( e<1 ){
+      return STATUS_UNFINISHED;
+    }else if( e==1 ){
+      CegInstantiator * cinst = getInstantiator( f );
+      Trace("inst-alg") << "-> Run cegqi for " << f << std::endl;
+      d_curr_quant = f;
+      bool addedLemma = cinst->check();
+      d_curr_quant = Node::null();
+      return addedLemma ? STATUS_UNKNOWN : STATUS_UNFINISHED;
+    }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 );
+        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 );
+        }
       }
     }
   }
@@ -1815,6 +591,23 @@ void InstStrategyCegqi::registerQuantifier( Node q ) {
   }
 }
 
+void InstStrategyCegqi::registerCounterexampleLemma( Node q, Node lem ) {
+  //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( q ); i++ ){
+    ce_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ) );
+  }
+  std::vector< Node > lems;
+  lems.push_back( lem );
+  CegInstantiator * cinst = getInstantiator( q );
+  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 );
+  }
+}
+
 void InstStrategyCegqi::presolve() {
   if( options::cbqiPreRegInst() ){
     for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 9fe938f16..adbb2a5e4 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -20,6 +20,7 @@
 
 #include "theory/quantifiers/instantiation_engine.h"
 #include "theory/arith/arithvar.h"
+#include "theory/quantifiers/ceg_instantiator.h"
 
 #include "util/statistics_registry.h"
 
@@ -32,106 +33,36 @@ namespace arith {
 
 namespace quantifiers {
 
-class CegqiOutput
-{
+class InstStrategyCbqi : public InstStrategy {
+protected:
+  bool d_cbqi_set_quant_inactive;
+  /** whether we have added cbqi lemma */
+  std::map< Node, bool > d_added_cbqi_lemma;
+  /** whether to do cbqi for this quantified formula */
+  std::map< Node, bool > d_do_cbqi;  
+  /** register ce lemma */
+  virtual void registerCounterexampleLemma( Node q, Node lem );
+  /** has added cbqi lemma */
+  bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); }
+  /** helper functions */
+  bool hasNonCbqiVariable( Node q );
+  bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited );
 public:
-  virtual ~CegqiOutput() {}
-  virtual bool addInstantiation( std::vector< Node >& subs ) = 0;
-  virtual bool isEligibleForInstantiation( Node n ) = 0;
-  virtual bool addLemma( Node lem ) = 0;
+  InstStrategyCbqi( QuantifiersEngine * qe );
+  ~InstStrategyCbqi() throw() {}
+  /** process functions */
+  void processResetInstantiationRound( Theory::Effort effort );
+  /** get next decision request */
+  Node getNextDecisionRequest();
+  //set quant inactive
+  bool setQuantifierInactive() { return d_cbqi_set_quant_inactive; }
+  /** whether to do CBQI for quantifier q */
+  bool doCbqi( Node q );
 };
 
-class CegInstantiator
-{
-private:
-  QuantifiersEngine * d_qe;
-  CegqiOutput * d_out;
-  //constants
-  Node d_zero;
-  Node d_one;
-  Node d_true;
-  bool d_use_vts_delta;
-  bool d_use_vts_inf;
-  //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< TypeNode, std::vector< Node > > d_curr_type_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;
-  //atoms of the CE lemma
-  bool d_is_nested_quant;
-  std::vector< Node > d_ce_atoms;
-private:
-  //collect atoms
-  void collectCeAtoms( Node n, std::map< Node, bool >& visited );
-  //for adding instantiations during check
-  void computeProgVars( Node n );
-  //solved form, involves substitution with coefficients
-  class SolvedForm {
-  public:
-    std::vector< Node > d_subs;
-    std::vector< Node > d_coeff;
-    std::vector< Node > d_has_coeff;
-    void copy( SolvedForm& sf ){
-      d_subs.insert( d_subs.end(), sf.d_subs.begin(), sf.d_subs.end() );
-      d_coeff.insert( d_coeff.end(), sf.d_coeff.begin(), sf.d_coeff.end() );
-      d_has_coeff.insert( d_has_coeff.end(), sf.d_has_coeff.begin(), sf.d_has_coeff.end() );
-    }
-    void push_back( Node pv, Node n, Node pv_coeff ){
-      d_subs.push_back( n );
-      d_coeff.push_back( pv_coeff );
-      if( !pv_coeff.isNull() ){
-        d_has_coeff.push_back( pv );
-      }
-    }
-    void pop_back( Node pv, Node n, Node pv_coeff ){
-      d_subs.pop_back();
-      d_coeff.pop_back();
-      if( !pv_coeff.isNull() ){
-        d_has_coeff.pop_back();
-      }
-    }
-  };
-  // effort=0 : do not use model value, 1: use model value, 2: one must use model value
-  bool addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
-                         std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
-                         std::map< Node, Node >& cons, std::vector< Node >& curr_var );
-  bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
-                            std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
-                            std::map< Node, Node >& cons, std::vector< Node >& curr_var );
-  bool addInstantiationCoeff( SolvedForm& sf,
-                              std::vector< Node >& vars, std::vector< int >& btyp,
-                              unsigned j, std::map< Node, Node >& cons );
-  bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons );
-  Node constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons );
-  Node applySubstitution( Node n, SolvedForm& sf, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ) {
-    return applySubstitution( n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, vars, pv_coeff, try_coeff );
-  }
-  Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff,
-                          std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true );
-  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 );
-  //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{
-private:
+class InstStrategySimplex : public InstStrategyCbqi {
+protected:
   /** reference to theory arithmetic */
   arith::TheoryArith* d_th;
   /** quantifiers we should process */
@@ -177,8 +108,7 @@ public:
 
 class InstStrategyCegqi;
 
-class CegqiOutputInstStrategy : public CegqiOutput
-{
+class CegqiOutputInstStrategy : public CegqiOutput {
 public:
   CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){}
   InstStrategyCegqi * d_out;
@@ -187,8 +117,8 @@ public:
   bool addLemma( Node lem );
 };
 
-class InstStrategyCegqi : public InstStrategy {
-private:
+class InstStrategyCegqi : public InstStrategyCbqi {
+protected:
   CegqiOutputInstStrategy * d_out;
   std::map< Node, CegInstantiator * > d_cinst;
   Node d_small_const;
@@ -197,6 +127,8 @@ private:
   /** process functions */
   void processResetInstantiationRound( Theory::Effort effort );
   int process( Node f, Theory::Effort effort, int e );
+  /** register ce lemma */
+  void registerCounterexampleLemma( Node q, Node lem );
 public:
   InstStrategyCegqi( QuantifiersEngine * qe );
   ~InstStrategyCegqi() throw() {}
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 8f1ef42d8..b32f27d8f 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -59,13 +59,17 @@ void InstantiationEngine::finishInit(){
   
   //counterexample-based quantifier instantiation
   if( options::cbqi() ){
-    if( !options::cbqi2() ){
+    if( options::cbqiSplx() ){
       d_i_splx = new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine );
       d_instStrategies.push_back( d_i_splx );
+      d_i_cbqi = d_i_splx;
     }else{
       d_i_cegqi = new InstStrategyCegqi( d_quantEngine );
       d_instStrategies.push_back( d_i_cegqi );
+      d_i_cbqi = d_i_cegqi;
     }
+  }else{
+    d_i_cbqi = NULL;
   }
 }
 
@@ -77,63 +81,6 @@ void InstantiationEngine::presolve() {
 
 bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   unsigned lastWaiting = d_quantEngine->d_lemmas_waiting.size();
-  //if counterexample-based quantifier instantiation is active
-  if( options::cbqi() ){
-    //check if any cbqi lemma has not been added yet
-    bool addedLemma = false;
-    for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-      Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
-      if( doCbqi( f ) && !hasAddedCbqiLemma( f ) ){
-        d_added_cbqi_lemma[f] = true;
-        Trace("cbqi") << "Do cbqi for " << f << std::endl;
-        //add cbqi lemma
-        //get the counterexample literal
-        Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f );
-        Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
-        if( !ceBody.isNull() ){
-          //add counterexample lemma
-          Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() );
-          //require any decision on cel to be phase=true
-          d_quantEngine->addRequirePhase( ceLit, true );
-          Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
-          //add counterexample lemma
-          lem = Rewriter::rewrite( lem );
-          Trace("cbqi") << "Counterexample lemma : " << lem << std::endl;
-
-          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;
-        }
-      }
-    }
-    if( addedLemma ){
-      return true;
-    }
-  }
-  //if not, proceed to instantiation round
-  //reset the instantiation strategies
-  for( unsigned i=0; i<d_instStrategies.size(); ++i ){
-    InstStrategy* is = d_instStrategies[i];
-    is->processResetInstantiationRound( effort );
-  }
-
   //iterate over an internal effort level e
   int e = 0;
   int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;
@@ -181,41 +128,27 @@ bool InstantiationEngine::needsCheck( Theory::Effort e ){
   return d_quantEngine->getInstWhenNeedsCheck( e );
 }
 
-unsigned InstantiationEngine::needsModel( Theory::Effort e ) {
+unsigned InstantiationEngine::needsModel( Theory::Effort e ){
   if( options::cbqiModel() && options::cbqi() ){
-    return QuantifiersEngine::QEFFORT_STANDARD;
-  }else{
-    return QuantifiersEngine::QEFFORT_NONE;
-  }
-}
-
-void InstantiationEngine::reset_round( Theory::Effort e ) {
-  d_cbqi_set_quant_inactive = false;
-  if( options::cbqi() ){
-    //set inactive the quantified formulas whose CE literals are asserted false
+    Assert( d_i_cbqi!=NULL );
+    //needs model if there is at least one cbqi quantified formula that is active
     for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
-      //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
-      if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) && hasAddedCbqiLemma( q ) ){
-        Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl;
-        Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
-        bool value;
-        if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){
-          Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl;
-          if( !value ){
-            if( d_quantEngine->getValuation().isDecision( cel ) ){
-              Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
-            }else{
-              d_quantEngine->getModel()->setQuantifierActive( q, false );
-              d_cbqi_set_quant_inactive = true;
-            }
-          }
-        }else{
-          Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl;
-        }
+      if( d_quantEngine->hasOwnership( q, this ) && d_i_cbqi->doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
+        return QuantifiersEngine::QEFFORT_STANDARD;
       }
     }
   }
+  return QuantifiersEngine::QEFFORT_NONE;
+}
+
+void InstantiationEngine::reset_round( Theory::Effort e ){
+  //if not, proceed to instantiation round
+  //reset the instantiation strategies
+  for( unsigned i=0; i<d_instStrategies.size(); ++i ){
+    InstStrategy* is = d_instStrategies[i];
+    is->processResetInstantiationRound( e );
+  }
 }
 
 void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
@@ -228,7 +161,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
     ++(d_statistics.d_instantiation_rounds);
     bool quantActive = false;
     d_quants.clear();
-    for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+    for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
       if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
         if( !options::cbqi() || !TermDb::hasInstConstAttr(q) ){
@@ -253,7 +186,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
 }
 
 bool InstantiationEngine::checkComplete() {
-  if( !options::cbqiSat() && d_cbqi_set_quant_inactive ){
+  if( !options::cbqiSat() && ( d_i_cbqi && d_i_cbqi->setQuantifierInactive() ) ){
     return false;
   }else{
     for( unsigned i=0; i<d_quants.size(); i++ ){
@@ -271,12 +204,14 @@ void InstantiationEngine::registerQuantifier( Node f ){
       d_instStrategies[i]->registerQuantifier( f );
     }
     //Notice() << "do cbqi " << f << " ? " << std::endl;
+    /*
     if( options::cbqi() ){
       Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
       if( !doCbqi( f ) ){
         d_quantEngine->addTermToDatabase( ceBody, true );
       }
     }
+    */
 
     //take into account user patterns
     if( f.getNumChildren()==3 ){
@@ -295,83 +230,20 @@ void InstantiationEngine::registerQuantifier( Node f ){
 }
 
 void InstantiationEngine::assertNode( Node f ){
-  ////if we are doing cbqi and have not added the lemma yet, do so
-  //if( doCbqi( f ) && !hasAddedCbqiLemma( f ) ){
-  //  addCbqiLemma( f );
-  //}
-}
 
-bool InstantiationEngine::hasApplyUf( Node n ){
-  if( n.getKind()==APPLY_UF ){
-    return true;
-  }else{
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( hasApplyUf( n[i] ) ){
-        return true;
-      }
-    }
-    return false;
-  }
-}
-bool InstantiationEngine::hasNonCbqiVariable( Node q ){
-  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-    TypeNode tn = q[0][i].getType();
-    if( !tn.isInteger() && !tn.isReal() && !tn.isBoolean() ){
-      if( options::cbqi2() ){
-        //datatypes supported in new implementation
-        if( !tn.isDatatype() ){
-          return true;
-        }
-      }else{
-        return true;
-      }
-    }
-  }
-  return false;
-}
-
-bool InstantiationEngine::doCbqi( Node q ){
-  if( options::cbqi.wasSetByUser() || options::cbqi2.wasSetByUser() ){
-    return options::cbqi();
-  }else if( options::cbqi() ){
-    //if quantifier has a non-arithmetic variable, then do not use cbqi
-    //if quantifier has an APPLY_UF term, then do not use cbqi
-    return !hasNonCbqiVariable( q ) && !hasApplyUf( q[1] );
-  }else{
-    return false;
-  }
 }
 
 bool InstantiationEngine::isIncomplete( Node q ) {
   return true;
-  //TODO : ensure completeness for local theory extensions
-  //if( d_i_lte ){
-  //return !d_i_lte->isLocalTheoryExt( f );
 }
 
-
-
-
-
-
-
-
-
-
-
-
 Node InstantiationEngine::getNextDecisionRequest(){
-  //propagate as decision all counterexample literals that are not asserted
   if( options::cbqi() ){
-    for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-      Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
-      if( hasAddedCbqiLemma( f ) ){
-        Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f );
-        bool value;
-        if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){
-          Debug("cbqi-prop-as-dec") << "CBQI: get next decision " << cel << std::endl;
-          return cel;
-        }
+    for( unsigned i=0; i<d_instStrategies.size(); ++i ){
+      InstStrategy* is = d_instStrategies[i];
+      Node lit = is->getNextDecisionRequest();
+      if( !lit.isNull() ){
+        return lit;
       }
     }
   }
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 3b7a5f4f8..e545ff43d 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -27,6 +27,7 @@ namespace quantifiers {
 class InstStrategyUserPatterns;
 class InstStrategyAutoGenTriggers;
 class InstStrategyFreeVariable;
+class InstStrategyCbqi;
 class InstStrategySimplex;
 class InstStrategyCegqi;
 
@@ -53,6 +54,8 @@ public:
   virtual std::string identify() const { return std::string("Unknown"); }
   /** register quantifier */
   virtual void registerQuantifier( Node q ) {}
+  /** get next decision request */
+  virtual Node getNextDecisionRequest() { return Node::null(); }
 };/* class InstStrategy */
 
 class InstantiationEngine : public QuantifiersModule
@@ -66,6 +69,7 @@ private:
   InstStrategyUserPatterns* d_isup;
   /** auto gen triggers; only kept for destructor cleanup */
   InstStrategyAutoGenTriggers* d_i_ag;
+  InstStrategyCbqi * d_i_cbqi;
   /** simplex (cbqi) */
   InstStrategySimplex * d_i_splx;
   /** generic cegqi */
@@ -74,25 +78,11 @@ private:
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
   /** current processing quantified formulas */
   std::vector< Node > d_quants;
-  /** whether we have added cbqi lemma */
-  std::map< Node, bool > d_added_cbqi_lemma;
 private:
-  /** has added cbqi lemma */
-  bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); }
-  /** helper functions */
-  bool hasNonCbqiVariable( Node q );
-  bool hasApplyUf( Node n );
-  /** whether to do CBQI for quantifier q */
-  bool doCbqi( Node q );
   /** is the engine incomplete for this quantifier */
   bool isIncomplete( Node q );
-  /** cbqi set inactive */
-  bool d_cbqi_set_quant_inactive;
-private:
   /** do instantiation round */
   bool doInstantiationRound( Theory::Effort effort );
-  /** register literals of n, f is the quantifier it belongs to */
-  //void registerLiterals( Node n, Node f );
 public:
   InstantiationEngine( QuantifiersEngine* qe );
   ~InstantiationEngine();
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 9502fd362..01d3f0c22 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -35,6 +35,8 @@ typedef enum {
   INST_WHEN_FULL_DELAY,
   /** Apply instantiation round at full effort half the time, and last call always */
   INST_WHEN_FULL_LAST_CALL,
+  /** Apply instantiation round at full effort after all other theories finish half the time, and last call always */
+  INST_WHEN_FULL_DELAY_LAST_CALL,
   /** Apply instantiation round at last call only */
   INST_WHEN_LAST_CALL,
 } InstWhenMode;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 9e8d02d30..a60f5af78 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -229,16 +229,18 @@ option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::Sygus
   template mode for sygus invariant synthesis
 
 # approach applied to general quantified formulas
+option cbqiSplx --cbqi-splx bool :read-write :default false
+ turns on old implementation of counterexample-based quantifier instantiation
 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 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 cbqiAll --cbqi-all bool :default false
+ apply counterexample-based instantiation to all quantified formulas
 option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false
  use integer infinity for vts in counterexample-based quantifier instantiation
 option cbqiUseInfReal --cbqi-use-inf-real bool :read-write :default false
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index f27b98a3d..02a1a6cf2 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -40,6 +40,10 @@ full-delay \n\
 + Run instantiation round at full effort, before theory combination, after\n\
   all other theories have finished.\n\
 \n\
+full-delay-last-call \n\
++ Alternate running instantiation rounds at full effort after all other\n\
+  theories have finished, and last call.  \n\
+\n\
 last-call\n\
 + Run instantiation at last call effort, after theory combination and\n\
   and theories report sat.\n\
@@ -235,6 +239,8 @@ inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg,
     return INST_WHEN_FULL_DELAY;
   } else if(optarg == "full-last-call") {
     return INST_WHEN_FULL_LAST_CALL;
+  } else if(optarg == "full-delay-last-call") {
+    return INST_WHEN_FULL_DELAY_LAST_CALL;
   } else if(optarg == "last-call") {
     return INST_WHEN_LAST_CALL;
   } else if(optarg == "help") {
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 0085177cc..5706c789e 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -312,12 +312,18 @@ bool Trigger::isAtomicTrigger( Node n ){
   return ( k==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) ||
          ( k!=APPLY_UF && isAtomicTriggerKind( k ) );
 }
+
 bool Trigger::isAtomicTriggerKind( Kind k ) {
   return k==APPLY_UF || k==SELECT || k==STORE ||
          k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER ||
          k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON;
 }
 
+bool Trigger::isCbqiKind( Kind k ) {
+  return quantifiers::TermDb::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT ||
+         k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER;
+}
+
 bool Trigger::isSimpleTrigger( Node n ){
   if( isAtomicTrigger( n ) ){
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index f601a02ab..bd4c19dba 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -108,6 +108,7 @@ public:
   static bool isUsableTrigger( Node n, Node f );
   static bool isAtomicTrigger( Node n );
   static bool isAtomicTriggerKind( Kind k );
+  static bool isCbqiKind( Kind k );
   static bool isSimpleTrigger( Node n );
   static bool isBooleanTermTrigger( Node n );
   static bool isPureTheoryTrigger( Node n );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 622ef5a52..28a4d4c6b 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -137,7 +137,7 @@ d_presolve_cache_wic(u){
   }else{
     d_inst_engine = NULL;
   }
-  if( options::finiteModelFind()  ){
+  if( options::finiteModelFind() ){
     if( options::fmfBoundInt() ){
       d_bint = new quantifiers::BoundedIntegers( c, this );
       d_modules.push_back( d_bint );
@@ -336,8 +336,11 @@ void QuantifiersEngine::check( Theory::Effort e ){
       if( d_modules[i]->needsCheck( e ) ){
         qm.push_back( d_modules[i] );
         needsCheck = true;
-        unsigned me = d_modules[i]->needsModel( e );
-        needsModelE = me<needsModelE ? me : needsModelE;
+        //can only request model at last call since theory combination can find inconsistencies
+        if( e>=Theory::EFFORT_LAST_CALL ){
+          unsigned me = d_modules[i]->needsModel( e );
+          needsModelE = me<needsModelE ? me : needsModelE;
+        }
       }
     }
   }
@@ -402,6 +405,11 @@ void QuantifiersEngine::check( Theory::Effort e ){
       d_modules[i]->reset_round( e );
     }
     Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
+    //reset may have added lemmas
+    flushLemmas();
+    if( d_hasAddedLemma ){
+      return;
+    }
 
     if( e==Theory::EFFORT_LAST_CALL ){
       //if effort is last call, try to minimize model first
@@ -702,7 +710,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
       }
       Assert( terms[i].getType().isSubtypeOf( f[0][i].getType() ) );
     }
-    if( options::cbqi() && !options::cbqi2() ){
+    if( options::cbqiSplx() ){
       for( int i=0; i<(int)terms.size(); i++ ){
         if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){
           Trace("inst")<< "***& Bad Instantiate " << f << " with " << std::endl;
@@ -987,7 +995,9 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY ){
     performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck();
   }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL ){
-    performCheck = ( ( e==Theory::EFFORT_FULL  && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
+    performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
+  }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL ){
+    performCheck = ( ( e==Theory::EFFORT_FULL && !getTheoryEngine()->needCheck() && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
   }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL ){
     performCheck = ( e >= Theory::EFFORT_LAST_CALL );
   }else{