Merge branch 'origin' of https://github.com/CVC4/CVC4.git

Conflicts:
	src/options/quantifiers_options

48 files changed, 2622 insertions, 1906 deletions

diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index 97116dee4..2ccc17e55 100755
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -836,7 +836,7 @@ void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) {
 //--------------------model checking---------------------------------------
 
 //do exhaustive instantiation
-bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {
+int AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {
   Trace("ambqi-check") << "Exhaustive instantiation " << q << " " << effort << std::endl;
   if (effort==0) {
     FirstOrderModelAbs * fma = fm->asFirstOrderModelAbs();
@@ -868,9 +868,10 @@ bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, in
       d_addedLemmas += lem;
       Trace("ambqi-inst-debug") << "...Total : " << d_addedLemmas << std::endl;
     }
-    return quantValid;
+    return quantValid ? 1 : 0;
+  }else{
+    return 1;
   }
-  return true;
 }
 
 bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ) {
diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h
index 3669d38b7..0adaef638 100755
--- a/src/theory/quantifiers/ambqi_builder.h
+++ b/src/theory/quantifiers/ambqi_builder.h
@@ -93,7 +93,7 @@ public:
   //process build model
   void processBuildModel(TheoryModel* m, bool fullModel);
   //do exhaustive instantiation
-  bool doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );
+  int doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );
 };
 
 }
diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp
index c8d18aced..9ccba38cd 100755
--- a/src/theory/quantifiers/anti_skolem.cpp
+++ b/src/theory/quantifiers/anti_skolem.cpp
@@ -14,18 +14,19 @@
  **/
 
 #include "theory/quantifiers/anti_skolem.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "options/quantifiers_options.h"
 
 using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
 
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
 
 struct sortTypeOrder {
   TermDb* d_tdb;
@@ -74,10 +75,13 @@ bool QuantAntiSkolem::CDSkQuantCache::add( context::Context* c, std::vector< Nod
   }
 }
 
-QuantAntiSkolem::QuantAntiSkolem( QuantifiersEngine * qe ) : QuantifiersModule( qe ){
-  d_sqc = new CDSkQuantCache( qe->getUserContext() );
+QuantAntiSkolem::QuantAntiSkolem(QuantifiersEngine* qe)
+    : QuantifiersModule(qe) {
+  d_sqc = new CDSkQuantCache(qe->getUserContext());
 }
 
+QuantAntiSkolem::~QuantAntiSkolem() { delete d_sqc; }
+
 /* Call during quantifier engine's check */
 void QuantAntiSkolem::check( Theory::Effort e, unsigned quant_e ) {
   if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
@@ -267,3 +271,6 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool
   }
 }
 
+}/* namespace CVC4::theory::quantifiers */
+}/* namespace CVC4::theory */
+}/* namespace CVC4 */
diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h
index 721371159..48205db9d 100755
--- a/src/theory/quantifiers/anti_skolem.h
+++ b/src/theory/quantifiers/anti_skolem.h
@@ -17,17 +17,39 @@
 #ifndef __CVC4__THEORY__QUANT_ANTI_SKOLEM_H
 #define __CVC4__THEORY__QUANT_ANTI_SKOLEM_H
 
-#include "theory/quantifiers_engine.h"
+#include <map>
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "context/cdhashset.h"
 #include "context/cdo.h"
 #include "theory/quantifiers/ce_guided_single_inv.h"
+#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
 class QuantAntiSkolem : public QuantifiersModule {
+public:
+  QuantAntiSkolem( QuantifiersEngine * qe );
+  virtual ~QuantAntiSkolem();
+
+  bool sendAntiSkolemizeLemma( std::vector< Node >& quants,
+                               bool pconnected = true );
+
+  /* Call during quantifier engine's check */
+  void check( Theory::Effort e, unsigned quant_e );
+  /* Called for new quantifiers */
+  void registerQuantifier( Node q ) {}
+  void assertNode( Node n ) {}
+  /** Identify this module (for debugging, dynamic configuration, etc..) */
+  std::string identify() const { return "QuantAntiSkolem"; }
+
+ private:
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-private:
+
   std::map< Node, bool > d_quant_processed;
   std::map< Node, SingleInvocationPartition > d_quant_sip;
   std::map< Node, std::vector< TypeNode > > d_ask_types;
@@ -54,22 +76,10 @@ private:
     bool add( context::Context* c, std::vector< Node >& quants, unsigned index = 0 );
   };
   CDSkQuantCache * d_sqc;
-public:
-  bool sendAntiSkolemizeLemma( std::vector< Node >& quants, bool pconnected = true );
-public:
-  QuantAntiSkolem( QuantifiersEngine * qe );
-
-  /* Call during quantifier engine's check */
-  void check( Theory::Effort e, unsigned quant_e );
-  /* Called for new quantifiers */
-  void registerQuantifier( Node q ) {}
-  void assertNode( Node n ) {}
-  /** Identify this module (for debugging, dynamic configuration, etc..) */
-  std::string identify() const { return "QuantAntiSkolem"; }
-};
+}; /* class QuantAntiSkolem */
 
-}
-}
-}
+}/* namespace CVC4::theory::quantifiers */
+}/* namespace CVC4::theory */
+}/* namespace CVC4 */
 
 #endif
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index a0d9bda0f..8e8f34cac 100755
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -264,6 +264,7 @@ CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mp
   Assert( mpat.getKind()==INST_CONSTANT );
   d_f = quantifiers::TermDb::getInstConstAttr( mpat );
   d_index = mpat.getAttribute(InstVarNumAttribute());
+  d_firstTime = false;
 }
 
 void CandidateGeneratorQEAll::resetInstantiationRound() {
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 71bf7c426..54415d974 100755
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -767,7 +767,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
       Assert( dt.isSygus() );
       //get the solution
       Node sol;
-      int status;
+      int status = -1;
       if( d_last_inst_si ){
         Assert( d_conj->getCegConjectureSingleInv() != NULL );
         sol = d_conj->getSingleInvocationSolution( i, tn, status );
@@ -786,39 +786,45 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
             for( unsigned j=0; j<svl.getNumChildren(); j++ ){
               subs.push_back( Node::fromExpr( svl[j] ) );
             }
+            bool templIsPost = false;
+            Node templ;
             if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){
-              const CegConjectureSingleInv* ceg_si =
-                  d_conj->getCegConjectureSingleInv();
+              const CegConjectureSingleInv* ceg_si = d_conj->getCegConjectureSingleInv();
               if(ceg_si->d_trans_pre.find( prog ) != ceg_si->d_trans_pre.end()){
-                std::vector<Node>& templ_vars = d_conj->getProgTempVars(prog);
-                Assert(templ_vars.size() == subs.size());
-                Node pre = ceg_si->getTransPre(prog);
-                pre = pre.substitute( templ_vars.begin(), templ_vars.end(),
-                                      subs.begin(), subs.end() );
-                TermDbSygus* sygusDb = getTermDatabase()->getTermDatabaseSygus();
-                sol = sygusDb->sygusToBuiltin( sol, sol.getType() );
-                Trace("cegqi-inv") << "Builtin version of solution is : "
-                                   << sol << ", type : " << sol.getType()
-                                   << std::endl;
-                sol = NodeManager::currentNM()->mkNode( OR, sol, pre );
+                templ = ceg_si->getTransPre(prog);
+                templIsPost = false;
               }
             }else if(options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST){
-              const CegConjectureSingleInv* ceg_si =
-                  d_conj->getCegConjectureSingleInv();
+              const CegConjectureSingleInv* ceg_si = d_conj->getCegConjectureSingleInv();
               if(ceg_si->d_trans_post.find(prog) != ceg_si->d_trans_post.end()){
-                std::vector<Node>& templ_vars = d_conj->getProgTempVars(prog);
-                Assert( templ_vars.size()==subs.size() );
-                Node post = ceg_si->getTransPost(prog);
-                post = post.substitute( templ_vars.begin(), templ_vars.end(),
-                                        subs.begin(), subs.end() );
-                TermDbSygus* sygusDb = getTermDatabase()->getTermDatabaseSygus();
-                sol = sygusDb->sygusToBuiltin( sol, sol.getType() );
-                Trace("cegqi-inv") << "Builtin version of solution is : "
-                                   << sol << ", type : " << sol.getType()
-                                   << std::endl;
-                sol = NodeManager::currentNM()->mkNode( AND, sol, post );
+                templ = ceg_si->getTransPost(prog);
+                templIsPost = true;
               }
             }
+            if( !templ.isNull() ){
+              std::vector<Node>& templ_vars = d_conj->getProgTempVars(prog);
+              
+              //take into consideration Boolean term conversion (this step can be eliminated when boolean term conversion is eliminated)
+              std::vector< Node > vars;
+              vars.insert( vars.end(), templ_vars.begin(), templ_vars.end() );
+              Node vl = Node::fromExpr( dt.getSygusVarList() );
+              Assert(vars.size() == subs.size());
+              for( unsigned j=0; j<templ_vars.size(); j++ ){
+                if( vl[j].getType().isBoolean() ){
+                  Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
+                  vars[j] = vars[j].eqNode( c );
+                }
+                Assert( vars[j].getType()==subs[j].getType() );
+              }
+              
+              templ = templ.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+              TermDbSygus* sygusDb = getTermDatabase()->getTermDatabaseSygus();
+              sol = sygusDb->sygusToBuiltin( sol, sol.getType() );
+              Trace("cegqi-inv") << "Builtin version of solution is : "
+                                 << sol << ", type : " << sol.getType()
+                                 << std::endl;
+              sol = NodeManager::currentNM()->mkNode( templIsPost ? AND : OR, sol, templ );
+            }
             if( sol==sygus_sol ){
               sol = sygus_sol;
               status = 1;
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 981abea94..e0bbbf8ac 100755
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -45,27 +45,41 @@ bool CegqiOutputSingleInv::addLemma( Node n ) {
   return d_out->addLemma( n );
 }
 
+CegConjectureSingleInv::CegConjectureSingleInv(QuantifiersEngine* qe,
+                                               CegConjecture* p)
+    : d_qe(qe),
+      d_parent(p),
+      d_sip(new SingleInvocationPartition),
+      d_sol(new CegConjectureSingleInvSol(qe)),
+      d_ei(NULL),
+      d_cosi(new CegqiOutputSingleInv(this)),
+      d_cinst(NULL),
+      d_c_inst_match_trie(NULL),
+      d_has_ites(true) {
+  //  third and fourth arguments set to (false,false) until we have solution
+  //  reconstruction for delta and infinity
+  d_cinst = new CegInstantiator(d_qe, d_cosi, false, false);
 
-CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p ) : d_qe( qe ), d_parent( p ){
-  d_has_ites = true;
-  if( options::incrementalSolving() ){
-    d_c_inst_match_trie = new inst::CDInstMatchTrie( qe->getUserContext() );
-  }else{
-    d_c_inst_match_trie = NULL;
+  if (options::incrementalSolving()) {
+    d_c_inst_match_trie = new inst::CDInstMatchTrie(qe->getUserContext());
   }
-  d_cosi = new CegqiOutputSingleInv( this );
-  //  third and fourth arguments set to (false,false) until we have solution reconstruction for delta and infinity
-  d_cinst = new CegInstantiator( d_qe, d_cosi, false, false );
 
-  d_sol = new CegConjectureSingleInvSol( qe );
-
-  d_sip = new SingleInvocationPartition;
+  if (options::cegqiSingleInvPartial()) {
+    d_ei = new CegEntailmentInfer(qe, d_sip);
+  }
+}
 
-  if( options::cegqiSingleInvPartial() ){
-    d_ei = new CegEntailmentInfer( qe, d_sip );
-  }else{
-    d_ei = NULL;
+CegConjectureSingleInv::~CegConjectureSingleInv() {
+  if (d_c_inst_match_trie) {
+    delete d_c_inst_match_trie;
+  }
+  delete d_cinst;
+  delete d_cosi;
+  if (d_ei) {
+    delete d_ei;
   }
+  delete d_sol;  // (new CegConjectureSingleInvSol(qe)),
+  delete d_sip;  // d_sip(new SingleInvocationPartition),
 }
 
 void CegConjectureSingleInv::getInitialSingleInvLemma( std::vector< Node >& lems ) {
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index feadeca39..449ab7189 100755
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -31,11 +31,10 @@ class CegConjecture;
 class CegConjectureSingleInv;
 class CegEntailmentInfer;
 
-class CegqiOutputSingleInv : public CegqiOutput
-{
+class CegqiOutputSingleInv : public CegqiOutput {
 public:
   CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){}
-  ~CegqiOutputSingleInv() {}
+  virtual ~CegqiOutputSingleInv() {}
   CegConjectureSingleInv * d_out;
   bool doAddInstantiation( std::vector< Node >& subs );
   bool isEligibleForInstantiation( Node n );
@@ -45,22 +44,13 @@ public:
 
 class SingleInvocationPartition;
 
-class CegConjectureSingleInv
-{
+class CegConjectureSingleInv {
+ private:
   friend class CegqiOutputSingleInv;
-private:
-  SingleInvocationPartition * d_sip;
-  QuantifiersEngine * d_qe;
-  CegConjecture * d_parent;
-  CegConjectureSingleInvSol * d_sol;
-  CegEntailmentInfer * d_ei;
-  //the instantiator
-  CegqiOutputSingleInv * d_cosi;
-  CegInstantiator * d_cinst;
-  //for recognizing templates for invariant synthesis
+  // for recognizing templates for invariant synthesis
   Node substituteInvariantTemplates(
-      Node n, std::map< Node, Node >& prog_templ,
-      std::map< Node, std::vector< Node > >& prog_templ_vars );
+      Node n, std::map<Node, Node>& prog_templ,
+      std::map<Node, std::vector<Node> >& prog_templ_vars);
   // partially single invocation
   Node removeDeepEmbedding( Node n, std::vector< Node >& progs,
                             std::vector< TypeNode >& types, int& type_valid,
@@ -73,42 +63,56 @@ private:
                                std::vector< Node >& terms,
                                std::map< Node, std::vector< Node > >& teq,
                                Node n, std::vector< Node >& conj );
-  //constructing solution
-  Node constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index, std::map< Node, Node >& weak_imp );
-  Node postProcessSolution( Node n );
-private:
-  //list of skolems for each argument of programs
-  std::vector< Node > d_single_inv_arg_sk;
-  //list of variables/skolems for each program
-  std::vector< Node > d_single_inv_var;
-  std::vector< Node > d_single_inv_sk;
-  std::map< Node, int > d_single_inv_sk_index;
-  //program to solution index
-  std::map< Node, unsigned > d_prog_to_sol_index;
-  //lemmas produced
+  // constructing solution
+  Node constructSolution(std::vector<unsigned>& indices, unsigned i,
+                         unsigned index, std::map<Node, Node>& weak_imp);
+  Node postProcessSolution(Node n);
+
+ private:
+  QuantifiersEngine* d_qe;
+  CegConjecture* d_parent;
+  SingleInvocationPartition* d_sip;
+  CegConjectureSingleInvSol* d_sol;
+  CegEntailmentInfer* d_ei;
+  // the instantiator
+  CegqiOutputSingleInv* d_cosi;
+  CegInstantiator* d_cinst;
+
+  // list of skolems for each argument of programs
+  std::vector<Node> d_single_inv_arg_sk;
+  // list of variables/skolems for each program
+  std::vector<Node> d_single_inv_var;
+  std::vector<Node> d_single_inv_sk;
+  std::map<Node, int> d_single_inv_sk_index;
+  // program to solution index
+  std::map<Node, unsigned> d_prog_to_sol_index;
+  // lemmas produced
   inst::InstMatchTrie d_inst_match_trie;
-  inst::CDInstMatchTrie * d_c_inst_match_trie;
-  //original conjecture
+  inst::CDInstMatchTrie* d_c_inst_match_trie;
+  // original conjecture
   Node d_orig_conjecture;
   // solution
   Node d_orig_solution;
   Node d_solution;
   Node d_sygus_solution;
   bool d_has_ites;
-public:
-  //lemmas produced
-  std::vector< Node > d_lemmas_produced;
-  std::vector< std::vector< Node > > d_inst;
-private:
-  std::vector< Node > d_curr_lemmas;
-  //add instantiation
+
+ public:
+  // lemmas produced
+  std::vector<Node> d_lemmas_produced;
+  std::vector<std::vector<Node> > d_inst;
+
+ private:
+  std::vector<Node> d_curr_lemmas;
+  // add instantiation
   bool doAddInstantiation( std::vector< Node >& subs );
   //is eligible for instantiation
   bool isEligibleForInstantiation( Node n );
   // add lemma
   bool addLemma( Node lem );
-public:
+ public:
   CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p );
+  ~CegConjectureSingleInv();
   // original conjecture
   Node d_quant;
   // single invocation portion of quantified formula
@@ -130,7 +134,7 @@ public:
   std::map< Node, Node > d_nsi_op_map;
   std::map< Node, Node > d_nsi_op_map_to_prog;
   std::map< Node, Node > d_prog_to_eval_op;
-public:
+ public:
   //get the single invocation lemma(s)
   void getInitialSingleInvLemma( std::vector< Node >& lems );
   //initialize
@@ -169,12 +173,12 @@ public:
 
 };
 
-// partitions any formulas given to it into single invocation/non-single invocation
-// only processes functions having argument types exactly matching "d_arg_types",
-//   and all invocations are in the same order across all functions
-class SingleInvocationPartition
-{
-private:
+// partitions any formulas given to it into single invocation/non-single
+// invocation only processes functions having argument types exactly matching
+// "d_arg_types",  and all invocations are in the same order across all
+// functions
+class SingleInvocationPartition {
+ private:
   //options
   Kind d_checkKind;
   bool inferArgTypes( Node n, std::vector< TypeNode >& typs, std::map< Node, bool >& visited );
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 0fe4b98c7..61a20ad42 100755
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -11,21 +11,18 @@
  **
  ** \brief Implementation of counterexample-guided quantifier instantiation
  **/
+ 
 #include "theory/quantifiers/ceg_instantiator.h"
+#include "theory/quantifiers/ceg_t_instantiator.h"
 
 #include "options/quantifiers_options.h"
 #include "smt/ite_removal.h"
-#include "theory/arith/partial_model.h"
-#include "theory/arith/theory_arith.h"
-#include "theory/arith/theory_arith_private.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/trigger.h"
 #include "theory/theory_engine.h"
 
-#include "theory/bv/theory_bv_utils.h"
-#include "util/bitvector.h"
-
-//#define MBP_STRICT_ASSERTIONS
 
 using namespace std;
 using namespace CVC4;
@@ -36,12 +33,15 @@ 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;
 }
 
+CegInstantiator::~CegInstantiator() {
+  for( std::map< Node, Instantiator * >::iterator it = d_instantiator.begin(); it != d_instantiator.end(); ++it ){
+    delete it->second;
+  }
+}
+
 void CegInstantiator::computeProgVars( Node n ){
   if( d_prog_var.find( n )==d_prog_var.end() ){
     d_prog_var[n].clear();
@@ -68,41 +68,108 @@ void CegInstantiator::computeProgVars( Node n ){
   }
 }
 
-bool CegInstantiator::doAddInstantiation( 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 CegInstantiator::isEligible( Node n ) {
+  //compute d_subs_fv, which program variables are contained in n, and determines if eligible
+  computeProgVars( n );
+  return d_inelig.find( n )==d_inelig.end();
+}
+
+bool CegInstantiator::hasVariable( Node n, Node pv ) {
+  computeProgVars( n );
+  return d_prog_var[n].find( pv )!=d_prog_var[n].end();
+}
+
+
+void CegInstantiator::registerInstantiationVariable( Node v, unsigned index ) {
+  if( d_instantiator.find( v )==d_instantiator.end() ){
+    TypeNode tn = v.getType();
+    Instantiator * vinst;
+    if( tn.isReal() ){
+      vinst = new ArithInstantiator( d_qe, tn );
+    }else if( tn.isSort() ){
+      Assert( options::quantEpr() );
+      vinst = new EprInstantiator( d_qe, tn );
+    }else if( tn.isDatatype() ){
+      vinst = new DtInstantiator( d_qe, tn );
+    }else if( tn.isBitVector() ){
+      vinst = new BvInstantiator( d_qe, tn );
+    }else if( tn.isBoolean() ){
+      vinst = new ModelValueInstantiator( d_qe, tn );
+    }else{
+      //default
+      vinst = new Instantiator( d_qe, tn );
+    }
+    d_instantiator[v] = vinst;
+  }
+  d_curr_subs_proc[v].clear();
+  d_curr_index[v] = index;
+}
+
+void CegInstantiator::unregisterInstantiationVariable( Node v ) {
+  d_curr_subs_proc.erase( v );
+  d_curr_index.erase( v );
+}
+
+bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned effort ){
   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 doAddInstantiationCoeff( csf, vars, btyp, 0, cons );
+    bool needsPostprocess = false;
+    std::map< Instantiator *, Node > pp_inst;
+    for( std::map< Node, Instantiator * >::iterator ita = d_active_instantiators.begin(); ita != d_active_instantiators.end(); ++ita ){
+      if( ita->second->needsPostProcessInstantiation( this, sf, ita->first, effort ) ){
+        needsPostprocess = true;
+        pp_inst[ ita->second ] = ita->first;
+      }
+    }
+    if( needsPostprocess ){
+      //must make copy so that backtracking reverts sf
+      SolvedForm sf_tmp;
+      sf_tmp.copy( sf );
+      bool postProcessSuccess = true;
+      for( std::map< Instantiator *, Node >::iterator itp = pp_inst.begin(); itp != pp_inst.end(); ++itp ){
+        if( !itp->first->postProcessInstantiation( this, sf_tmp, itp->second, effort ) ){
+          postProcessSuccess = false;
+          break;
+        }
+      } 
+      if( postProcessSuccess ){
+        return doAddInstantiation( sf_tmp.d_subs, sf_tmp.d_vars );
       }else{
-        return doAddInstantiationCoeff( sf, vars, btyp, 0, cons );
+        return false;
       }
     }else{
-      return doAddInstantiation( sf.d_subs, vars, cons );
+      return doAddInstantiation( sf.d_subs, sf.d_vars );
     }
   }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() ){
+    if( d_stack_vars.empty() ){
       pv = d_vars[i];
     }else{
-      pv = curr_var.back();
+      pv = d_stack_vars.back();
       is_cv = true;
+      d_stack_vars.pop_back();
+    }
+    registerInstantiationVariable( pv, i );
+
+    //get the instantiator object
+    Instantiator * vinst = NULL;
+    std::map< Node, Instantiator * >::iterator itin = d_instantiator.find( pv );
+    if( itin!=d_instantiator.end() ){
+      vinst = itin->second;
     }
+    Assert( vinst!=NULL );
+    d_active_instantiators[pv] = vinst;
+    vinst->reset( this, sf, pv, effort );
+
     TypeNode pvtn = pv.getType();
     TypeNode pvtnb = pvtn.getBaseType();
     Node pvr = pv;
     if( d_qe->getMasterEqualityEngine()->hasTerm( pv ) ){
       pvr = d_qe->getMasterEqualityEngine()->getRepresentative( pv );
     }
-    Trace("cbqi-inst-debug") << "[Find instantiation for " << pv << "], rep=" << pvr << std::endl;
+    Trace("cbqi-inst-debug") << "[Find instantiation for " << pv << "], rep=" << pvr << ", instantiator is " << vinst->identify() << std::endl;
     Node pv_value;
     if( options::cbqiModel() ){
       pv_value = getModelValue( pv );
@@ -116,72 +183,38 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
       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() ){
+        //std::vector< Node > eq_candidates;
         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() ){
+            if( isEligible( n ) ){
               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( pvtn, n, sf, vars, pv_coeff, false );
+                ns = applySubstitution( pvtn, n, sf, 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();
+                  proc = 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( doAddInstantiationInc( ns, pv, pv_coeff, 0, sf, ssf, vars,  btyp, theta, i, effort, cons, curr_var ) ){
+                if( vinst->processEqualTerm( this, sf, pv, pv_coeff, ns, effort ) ){
                   return true;
                 }
               }
             }
           }
         }
-        if( pvtn.isDatatype() ){
-          Trace("cbqi-inst-debug") << "[2] try based on constructors in equivalence class." << std::endl;
-          //[2] look in equivalence class for a constructor
-          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( doAddInstantiation( 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;
-              }
-            }
-          }
+        if( vinst->processEqualTerms( this, sf, pv, it_eqc->second, effort ) ){
+          return true;
         }
       }else{
         Trace("cbqi-inst-debug2") << "...eqc not found." << std::endl;
@@ -189,762 +222,246 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
 
       //[3] : we can solve an equality for pv
       ///iterate over equivalence classes to find cases where we can solve for the variable
-      Trace("cbqi-inst-debug") << "[3] try based on solving equalities." << 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( pvtn, n, sf, vars, pv_coeff );
-              if( !ns.isNull() ){
-                computeProgVars( ns );
+      if( vinst->hasProcessEquality( this, sf, pv, effort ) ){
+        Trace("cbqi-inst-debug") << "[3] try based on solving equalities." << 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;
+            //must be an eligible term
+            if( isEligible( n ) ){
+              Node ns;
+              Node pv_coeff;
+              if( !d_prog_var[n].empty() ){
+                ns = applySubstitution( pvtn, n, sf, pv_coeff );
+                if( !ns.isNull() ){
+                  computeProgVars( ns );
+                }
+              }else{
+                ns = n;
               }
-            }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 val;
-                  Node veq_c;
-                  bool success = false;
-                  if( pvtnb.isReal() ){
-                    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 );
-                    Node vts_coeff_inf;
-                    Node vts_coeff_delta;
-                    //isolate pv in the equality
-                    int ires = solve_arith( pv, eq, veq_c, val, vts_coeff_inf, vts_coeff_delta );
-                    if( ires!=0 ){
-                      success = true;
-                    }
-                    /*
-                    //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 << " : " << pv.getType() << "..." << 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( doAddInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
-                            return true;
-                          }
-                        }
-                      }
-                    }
-                    */
-                  }else if( pvtnb.isDatatype() ){
-                    val = solve_dt( pv, lhs[j], ns, lhs[j], ns );
-                    if( !val.isNull() ){
-                      success = true;
-                    }
-                  }
-                  if( success ){
-                    if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
-                      subs_proc[val][veq_c] = true;
-                      if( doAddInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
-                        return true;
-                      }
+              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;
+                std::vector< Node > term_coeffs;
+                std::vector< Node > terms;
+                term_coeffs.push_back( pv_coeff );
+                terms.push_back( ns );
+                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;
+                    //processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { return false; }
+                    term_coeffs.push_back( lhs_coeff[j] );
+                    terms.push_back( lhs[j] );
+                    if( vinst->processEquality( this, sf, pv, term_coeffs, terms, effort ) ){
+                      return true;
                     }
+                    term_coeffs.pop_back();
+                    terms.pop_back();
                   }
                 }
+                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;
               }
-              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;
+              Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible." << std::endl;
             }
-          }else{
-            Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible." << std::endl;
           }
         }
       }
 
       //[4] directly look at assertions
-      Trace("cbqi-inst-debug") << "[4] try based on assertions." << std::endl;
-      d_vts_sym[0] = d_qe->getTermDatabase()->getVtsInfinity( pvtn, false, false );
-      d_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];
-      //std::vector< MbpBounds > mbp_bounds[2];
-      //unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2;
-      for( unsigned r=0; r<2; r++ ){
-        TheoryId tid = r==0 ? Theory::theoryOf( pvtn ) : THEORY_UF;
-        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( pvtn.isReal() ){
-              //arithmetic inequalities and disequalities
-              if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && 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( pvtn, 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;
-                    Node vts_coeff_inf;
-                    Node vts_coeff_delta;
-                    Node val;
-                    Node veq_c;
-                    //isolate pv in the inequality
-                    int ires = solve_arith( pv, satom, veq_c, val, vts_coeff_inf, vts_coeff_delta );
-                    if( ires!=0 ){
-                      //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_inf.isNull() ){
-                              //coefficient or val won't make a difference, just compare with zero
-                              Trace("cbqi-inst-debug") << "Disequality : check infinity polarity " << vts_coeff_inf << std::endl;
-                              Assert( vts_coeff_inf.isConst() );
-                              is_upper = ( vts_coeff_inf.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_delta.isNull() ){
-                              vts_coeff_delta = delta_coeff;
-                            }else{
-                              vts_coeff_delta = NodeManager::currentNM()->mkNode( PLUS, vts_coeff_delta, delta_coeff );
-                              vts_coeff_delta = Rewriter::rewrite( vts_coeff_delta );
-                            }
-                          }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( t==0 ? vts_coeff_inf : vts_coeff_delta );
-                          }
-                          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( doAddInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
-                              return true;
-                            }
-                          }
-                        }
-                      }
-                    }
-                  }
-                }
-              }
-            }
-            /*   TODO: algebraic reasoning for bitvector instantiation
-            else if( pvtn.isBitVector() ){
-              if( atom.getKind()==BITVECTOR_ULT || atom.getKind()==BITVECTOR_ULE ){
-                for( unsigned t=0; t<2; t++ ){
-                  if( atom[t]==pv ){
-                    computeProgVars( atom[1-t] );
-                    if( d_inelig.find( atom[1-t] )==d_inelig.end() ){
-                      //only ground terms  TODO: more
-                      if( d_prog_var[atom[1-t]].empty() ){
-                        Node veq_c;
-                        Node uval;
-                        if( ( !pol && atom.getKind()==BITVECTOR_ULT ) || ( pol && atom.getKind()==BITVECTOR_ULE ) ){
-                          uval = atom[1-t];
-                        }else{
-                          uval = NodeManager::currentNM()->mkNode( (atom.getKind()==BITVECTOR_ULT)==(t==1) ? BITVECTOR_PLUS : BITVECTOR_SUB, atom[1-t], 
-                                                                   bv::utils::mkConst(pvtn.getConst<BitVectorSize>(), 1) );
-                        }
-                        if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
-                          subs_proc[uval][veq_c] = true;
-                          if( doAddInstantiationInc( uval, pv, veq_c, 0, 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() ) && !options::cbqiMidpoint();
-          bool upper_first = false;
-          if( options::cbqiMinBounds() ){
-            upper_first = mbp_bounds[1].size()<mbp_bounds[0].size();
-          }
-          int 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;
-            best_used[rr] = -1;
-            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( doAddInstantiationInc( 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] = best;
-                //if using cbqiMidpoint, only add the instance based on one bound if the bound is non-strict
-                if( !options::cbqiMidpoint() || pvtn.isInteger() || mbp_vts_coeff[rr][1][best].isNull() ){
-                  Node val = mbp_bounds[rr][best];
-                  val = getModelBasedProjectionValue( pv, val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta,
-                                                      mbp_vts_coeff[rr][0][best], mbp_vts_coeff[rr][1][best] );
-                  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( doAddInstantiationInc( 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( pv, val, true, c, pv_value, d_zero, theta, Node::null(), Node::null() );
-            if( !val.isNull() ){
-              if( subs_proc[val].find( c )==subs_proc[val].end() ){
-                subs_proc[val][c] = true;
-                if( doAddInstantiationInc( val, pv, c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
-                  return true;
-                }
-              }
-            }
-          }
-          if( options::cbqiMidpoint() && !pvtn.isInteger() ){
-            Node vals[2];
-            bool bothBounds = true;
-            Trace("cbqi-bound") << "Try midpoint of bounds..." << std::endl;
-            for( unsigned rr=0; rr<2; rr++ ){
-              int best = best_used[rr];
-              if( best==-1 ){
-                bothBounds = false;
-              }else{
-                vals[rr] = mbp_bounds[rr][best];
-                vals[rr] = getModelBasedProjectionValue( pv, vals[rr], rr==0, Node::null(), pv_value, t_values[rr][best], theta,
-                                                         mbp_vts_coeff[rr][0][best], Node::null() );
-              }
-              Trace("cbqi-bound") << "Bound : " << vals[rr] << std::endl;
-            }
-            Node val;
-            if( bothBounds ){
-              Assert( !vals[0].isNull() && !vals[1].isNull() );
-              if( vals[0]==vals[1] ){
-                val = vals[0];
-              }else{
-                val = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkNode( PLUS, vals[0], vals[1] ),
-                                                              NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ) );
-                val = Rewriter::rewrite( val );
-              }
-            }else{
-              if( !vals[0].isNull() ){
-                val = NodeManager::currentNM()->mkNode( PLUS, vals[0], d_one );
-                val = Rewriter::rewrite( val );
-              }else if( !vals[1].isNull() ){
-                val = NodeManager::currentNM()->mkNode( MINUS, vals[1], d_one );
-                val = Rewriter::rewrite( val );
-              }
-            }
-            Trace("cbqi-bound") << "Midpoint value : " << val << std::endl;
-            if( !val.isNull() ){
-              if( subs_proc[val].find( Node::null() )==subs_proc[val].end() ){
-                subs_proc[val][Node::null()] = true;
-                if( doAddInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+      if( vinst->hasProcessAssertion( this, sf, pv, effort ) ){
+        Trace("cbqi-inst-debug") << "[4] try based on assertions." << std::endl;
+        std::vector< Node > lits;
+        //unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2;
+        for( unsigned r=0; r<2; r++ ){
+          TheoryId tid = r==0 ? Theory::theoryOf( pvtn ) : THEORY_UF;
+          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];
+              if( std::find( lits.begin(), lits.end(), lit )==lits.end() ){
+                lits.push_back( lit );
+                if( vinst->processAssertion( this, sf, pv, lit, effort ) ){
                   return true;
                 }
               }
             }
           }
-#ifdef MBP_STRICT_ASSERTIONS
-          Assert( false );
-#endif
-          if( options::cbqiNopt() ){
-            //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( (int)j!=best_used[rr] && ( !options::cbqiMidpoint() || mbp_vts_coeff[rr][1][j].isNull() ) ){
-                  Node val = getModelBasedProjectionValue( pv, mbp_bounds[rr][j], rr==0, mbp_coeff[rr][j], pv_value, t_values[rr][j], theta,
-                                                           mbp_vts_coeff[rr][0][j], mbp_vts_coeff[rr][1][j] );
-                  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( doAddInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
-                        return true;
-                      }
-                    }
-                  }
-                }
-              }
-            }
-          }
+        }
+        if( vinst->processAssertions( this, sf, pv, lits, effort ) ){
+          return true;
         }
       }
     }
 
     //[5] 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() || pvtn.isBitVector() || !curr_var.empty() ) && d_qe->getTermDatabase()->isClosedEnumerableType( pvtn ) ){
+    bool use_model_value = vinst->useModelValue( this, sf, pv, effort );
+    if( ( effort>0 || use_model_value || is_cv ) && vinst->allowModelValue( this, sf, pv, effort ) ){
+#ifdef CVC4_ASSERTIONS
+      if( pvtn.isReal() && options::cbqiNestedQE() && !options::cbqiAll() ){
+        Trace("cbqi-warn") << "Had to resort to model value." << std::endl;
+        Assert( false );
+      }
+#endif
       Node mv = getModelValue( pv );
       Node pv_coeff_m;
       Trace("cbqi-inst-debug") << "[5] " << 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( doAddInstantiationInc( mv, pv, pv_coeff_m, 0, sf, ssf, vars, btyp, theta, i, new_effort, cons, curr_var ) ){
+      int new_effort = use_model_value ? effort : 1;
+      if( doAddInstantiationInc( pv, mv, pv_coeff_m, 0, sf, new_effort ) ){
         return true;
       }
     }
     Trace("cbqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl;
+    if( is_cv ){  
+      d_stack_vars.push_back( pv );
+    }
+    d_active_instantiators.erase( pv );
+    unregisterInstantiationVariable( pv );
     return false;
   }
 }
 
+void CegInstantiator::pushStackVariable( Node v ) {
+  d_stack_vars.push_back( v );
+}
 
-bool CegInstantiator::doAddInstantiationInc( 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;
-    Assert( n.getType().isSubtypeOf( pv.getType() ) );
-  }
-  //must ensure variables have been computed for n
-  computeProgVars( n );
-  Assert( d_inelig.find( n )==d_inelig.end() );
+void CegInstantiator::popStackVariable() {
+  Assert( !d_stack_vars.empty() );
+  d_stack_vars.pop_back();
+}
 
-  //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;
-  Trace("cbqi-inst-debug2") << "Applying substitutions..." << std::endl;
-  for( unsigned j=0; j<sf.d_subs.size(); j++ ){
-    Trace("cbqi-inst-debug2") << "  Apply for " << sf.d_subs[j]  << std::endl;
-    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( vars[j].getType(), 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 ) );
+bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int bt, SolvedForm& sf, unsigned effort ) {
+  if( d_curr_subs_proc[pv][n].find( pv_coeff )==d_curr_subs_proc[pv][n].end() ){
+    d_curr_subs_proc[pv][n][pv_coeff] = true;
+    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;
+      Assert( n.getType().isSubtypeOf( pv.getType() ) );
+    }
+    //must ensure variables have been computed for n
+    computeProgVars( n );
+    Assert( d_inelig.find( n )==d_inelig.end() );
+
+    //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;
+    Trace("cbqi-inst-debug2") << "Applying substitutions..." << std::endl;
+    for( unsigned j=0; j<sf.d_subs.size(); j++ ){
+      Trace("cbqi-inst-debug2") << "  Apply for " << sf.d_subs[j]  << std::endl;
+      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_vars[j].getType(), 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(), sf.d_vars[j] )==sf.d_has_coeff.end() );
+              //now has coefficient
+              new_has_coeff.push_back( sf.d_vars[j] );
+              sf.d_has_coeff.push_back( sf.d_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] );
+            Assert( d_inelig.find( sf.d_subs[j] )==d_inelig.end() );
+          }
+          Trace("cbqi-inst-debug2") << "Subs " << j << " " << sf.d_subs[j] << std::endl;
+        }else{
+          Trace("cbqi-inst-debug2") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl;
+          success = false;
+          break;
         }
-        if( sf.d_subs[j]!=prev_subs[j] ){
-          computeProgVars( sf.d_subs[j] );
-          Assert( d_inelig.find( sf.d_subs[j] )==d_inelig.end() );
-        }
-        Trace("cbqi-inst-debug2") << "Subs " << j << " " << sf.d_subs[j] << std::endl;
       }else{
-        Trace("cbqi-inst-debug2") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl;
-        success = false;
-        break;
+        Trace("cbqi-inst-debug2") << "Skip " << j << " " << sf.d_subs[j] << std::endl;
       }
-    }else{
-      Trace("cbqi-inst-debug2") << "Skip " << j << " " << sf.d_subs[j] << std::endl;
-    }
-    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 ){
-    Trace("cbqi-inst-debug2") << "Adding to vectors..." << std::endl;
-    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 );
+    if( success ){
+      Trace("cbqi-inst-debug2") << "Adding to vectors..." << std::endl;
+      sf.push_back( pv, n, pv_coeff, bt );
+      Node prev_theta = sf.d_theta;
+      Node new_theta = sf.d_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;
-    }
-    Trace("cbqi-inst-debug2") << "Recurse..." << std::endl;
-    success = doAddInstantiation( sf, ssf, vars, btyp, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var );
-    if( !success ){
-      Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl;
-      if( is_cv ){
-        curr_var.push_back( pv );
+      sf.d_theta = new_theta;
+      Trace("cbqi-inst-debug2") << "Recurse..." << std::endl;
+      unsigned i = d_curr_index[pv];
+      success = doAddInstantiation( sf, d_stack_vars.empty() ? i+1 : i, effort );
+      sf.d_theta = prev_theta;
+      if( !success ){
+        Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl;
+        sf.pop_back( pv, n, pv_coeff, bt );
       }
-      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{
-    Trace("cbqi-inst-debug2") << "Revert substitutions..." << std::endl;
-    //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::doAddInstantiationCoeff( 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 doAddInstantiation( 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_TOTAL, veq[1], veq_c );
-          Trace("cbqi-inst-debug") << "...bound type is : " << btyp[index] << std::endl;
-          //intger division rounding up if from a lower bound
-          if( btyp[index]==1 && options::cbqiRoundUpLowerLia() ){
-            sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index],
-              NodeManager::currentNM()->mkNode( ITE,
-                NodeManager::currentNM()->mkNode( EQUAL,
-                  NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, 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( doAddInstantiationCoeff( sf, vars, btyp, j+1, cons ) ){
-          return true;
-        }
+    if( success ){
+      return true;
+    }else{
+      Trace("cbqi-inst-debug2") << "Revert substitutions..." << std::endl;
+      //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();
       }
+      return false;
     }
-    sf.d_subs[index] = prev;
-    Trace("cbqi-inst-debug") << "...failed." << std::endl;
+  }else{
+    //already tried this substitution
     return false;
   }
 }
 
-bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ) {
+bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars ) {
   if( vars.size()>d_vars.size() ){
     Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl;
     std::map< Node, Node > subs_map;
@@ -953,7 +470,9 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector
     }
     subs.clear();
     for( unsigned i=0; i<d_vars.size(); i++ ){
-      Node n = constructInstantiation( d_vars[i], subs_map, cons );
+      std::map< Node, Node >::iterator it = subs_map.find( d_vars[i] );
+      Assert( it!=subs_map.end() );
+      Node n = it->second;
       Trace("cbqi-inst-debug") << "  " << d_vars[i] << " -> " << n << std::endl;
       subs.push_back( n );
     }
@@ -967,32 +486,9 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector
     }
   }
   bool ret = d_out->doAddInstantiation( 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( TypeNode tn, 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() );
@@ -1097,66 +593,6 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
   }
 }
 
-Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) {
-  Node val = t;
-  Trace("cbqi-bound2") << "Value : " << val << std::endl;
-  Assert( !e.getType().isInteger() || t.getType().isInteger() );
-  Assert( !e.getType().isInteger() || mt.getType().isInteger() );
-  //add rho value
-  //get the value of c*e
-  Node ceValue = me;
-  Node new_theta = theta;
-  if( !c.isNull() ){
-    Assert( c.getType().isInteger() );
-    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() && e.getType().isInteger() ){
-    Node rho;
-    //if( !mt.getType().isInteger() ){
-      //round up/down
-      //mt = NodeManager::currentNM()->mkNode(
-    //}
-    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( !d_vts_sym[0].isNull() );
-    val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, d_vts_sym[0] ) );
-    val = Rewriter::rewrite( val );
-  }
-  if( !delta_coeff.isNull() ){
-    //create delta here if necessary
-    if( d_vts_sym[1].isNull() ){
-      d_vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta();
-    }
-    val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, d_vts_sym[1] ) );
-    val = Rewriter::rewrite( val );
-  }
-  return val;
-}
-
 bool CegInstantiator::check() {
   if( d_qe->getTheoryEngine()->needCheck() ){
     Trace("cbqi-engine") << "  CEGQI instantiator : wait until all ground theories are finished." << std::endl;
@@ -1165,14 +601,9 @@ bool CegInstantiator::check() {
   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;
+    d_stack_vars.clear();
     //try to add an instantiation
-    if( doAddInstantiation( sf, ssf, vars, btyp, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){
+    if( doAddInstantiation( sf, 0, r==0 ? 0 : 2 ) ){
       return true;
     }
   }
@@ -1222,25 +653,27 @@ void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& ter
 }
 
 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 );
+  //only if no nested quantifiers
+  if( !QuantifiersRewriter::containsQuantifiers( q[1] ) ){
+    std::vector< Node > ps_vars;
+    std::map< Node, std::vector< Node > > teq;
+    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+      ps_vars.push_back( q[0][i] );
+      teq[q[0][i]].clear();
+    }
+    collectPresolveEqTerms( q[1], teq );
+    std::vector< Node > terms;
+    std::vector< Node > conj;
+    getPresolveEqConjuncts( ps_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 );
+    }
   }
 }
 
@@ -1362,9 +795,7 @@ void CegInstantiator::processAssertions() {
       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
     }
   }
 
@@ -1397,10 +828,8 @@ void CegInstantiator::processAssertions() {
     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() ){
+      if( isEligible( n ) ){
         //must contain at least one variable
         if( !d_prog_var[n].empty() ){
           Trace("cbqi-proc") << "...literal[" << it->first << "] : " << n << std::endl;
@@ -1453,17 +882,16 @@ Node CegInstantiator::getModelValue( Node 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 );
-        }
+  }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() ){
+        Trace("cbqi-ce-atoms") << "CE atoms : " << n << std::endl;
+        d_ce_atoms.push_back( n );
       }
     }
   }
@@ -1479,7 +907,8 @@ struct sortCegVarOrder {
 
 
 void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
-  Assert( d_vars.empty() );
+  //Assert( d_vars.empty() );
+  d_vars.clear();
   d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() );
 
   //determine variable order: must do Reals before Ints
@@ -1512,7 +941,9 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
   //remove ITEs
   IteSkolemMap iteSkolemMap;
   d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap);
-  Assert( d_aux_vars.empty() );
+  //Assert( d_aux_vars.empty() );
+  d_aux_vars.clear();
+  d_aux_eq.clear();
   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 );
@@ -1544,159 +975,14 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
   }
 }
 
-//this isolates the atom into solved form
-//     veq_c * pv <> val + vts_coeff_delta * delta + vts_coeff_inf * inf
-//  ensures val is Int if pv is Int, and val does not contain vts symbols
-int CegInstantiator::solve_arith( Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) {
-  int ires = 0;
-  Trace("cbqi-inst-debug") << "isolate for " << pv << " in " << atom << std::endl;
-  std::map< Node, Node > msum;
-  if( QuantArith::getMonomialSumLit( atom, msum ) ){
-    Trace("cbqi-inst-debug") << "got monomial sum: " << std::endl;
-    if( Trace.isOn("cbqi-inst-debug") ){
-      QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" );
-    }
-    TypeNode pvtn = pv.getType();
-    //remove vts symbols from polynomial
-    Node vts_coeff[2];
-    for( unsigned t=0; t<2; t++ ){
-      if( !d_vts_sym[t].isNull() ){
-        std::map< Node, Node >::iterator itminf = msum.find( d_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( d_vts_sym[t] );
-        }
-      }
-    }
 
-    ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() );
-    if( ires!=0 ){
-      Node realPart;
-      if( Trace.isOn("cbqi-inst-debug") ){
-        Trace("cbqi-inst-debug") << "Isolate : ";
-        if( !veq_c.isNull() ){
-          Trace("cbqi-inst-debug") << veq_c << " * ";
-        }
-        Trace("cbqi-inst-debug") << pv << " " << atom.getKind() << " " << val << std::endl;
-      }
-      if( options::cbqiAll() ){
-        // when not pure LIA/LRA, we must check whether the lhs contains pv
-        if( TermDb::containsTerm( val, pv ) ){
-          return 0;
-        }
-      }
-      if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){
-        //redo, split integer/non-integer parts
-        bool useCoeff = false;
-        Integer coeff = d_one.getConst<Rational>().getNumerator();
-        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
-          if( it->first.isNull() || it->first.getType().isInteger() ){
-            if( !it->second.isNull() ){
-              coeff = coeff.lcm( it->second.getConst<Rational>().getDenominator() );
-              useCoeff = true;
-            }
-          }
-        }
-        //multiply everything by this coefficient
-        Node rcoeff = NodeManager::currentNM()->mkConst( Rational( coeff ) );
-        std::vector< Node > real_part;
-        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
-          if( useCoeff ){
-            if( it->second.isNull() ){
-              msum[it->first] = rcoeff;
-            }else{
-              msum[it->first] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, it->second, rcoeff ) );
-            }
-          }
-          if( !it->first.isNull() && !it->first.getType().isInteger() ){
-            real_part.push_back( msum[it->first].isNull() ? it->first : NodeManager::currentNM()->mkNode( MULT, msum[it->first], it->first ) );
-          }
-        }
-        //remove delta  TODO: check this
-        vts_coeff[1] = Node::null();
-        //multiply inf
-        if( !vts_coeff[0].isNull() ){
-          vts_coeff[0] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[0] ) );
-        }
-        realPart = real_part.empty() ? d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) );
-        Assert( d_out->isEligibleForInstantiation( realPart ) );
-        //re-isolate
-        Trace("cbqi-inst-debug") << "Re-isolate..." << std::endl;
-        ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() );
-        Trace("cbqi-inst-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl;
-        Trace("cbqi-inst-debug") << "                 real part : " << realPart << std::endl;
-        if( ires!=0 ){
-          int ires_use = ( msum[pv].isNull() || msum[pv].getConst<Rational>().sgn()==1 ) ? 1 : -1;
-          val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires_use==-1 ? PLUS : MINUS,
-                                    NodeManager::currentNM()->mkNode( ires_use==-1 ? MINUS : PLUS, val, realPart ),
-                                    NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) );  //TODO: round up for upper bounds?
-          Trace("cbqi-inst-debug") << "result : " << val << std::endl;
-          Assert( val.getType().isInteger() );
-        }
-      }
-    }
-    vts_coeff_inf = vts_coeff[0];
-    vts_coeff_delta = vts_coeff[1];
-  }
-  return ires;
+Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn ){
+  d_closed_enum_type = qe->getTermDatabase()->isClosedEnumerableType( tn );
 }
 
-Node CegInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) {
-  Trace("cbqi-inst-debug2") << "Solve dt : " << v << " " << a << " " << b << " " << sa << " " << sb << std::endl;
-  Node ret;
-  if( !a.isNull() && a==v ){
-    ret = sb;
-  }else if( !b.isNull() && b==v ){
-    ret = sa;
-  }else if( !a.isNull() && a.getKind()==APPLY_CONSTRUCTOR ){
-    if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){
-      if( a.getOperator()==b.getOperator() ){
-        for( unsigned i=0; i<a.getNumChildren(); i++ ){
-          Node s = solve_dt( v, a[i], b[i], sa[i], sb[i] );
-          if( !s.isNull() ){
-            return s;
-          }
-        }
-      }
-    }else{
-      unsigned cindex = Datatype::indexOf( a.getOperator().toExpr() );
-      TypeNode tn = a.getType();
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      for( unsigned i=0; i<a.getNumChildren(); i++ ){
-        Node nn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][i].getSelector() ), sb );
-        Node s = solve_dt( v, a[i], Node::null(), sa[i], nn );
-        if( !s.isNull() ){
-          return s;
-        }
-      }
-    }
-  }else if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){
-    return solve_dt( v, b, a, sb, sa );
-  }
-  if( !ret.isNull() ){
-    //ensure does not contain
-    if( TermDb::containsTerm( ret, v ) ){
-      ret = Node::null();
-    }
-  }
-  return ret;
+
+bool Instantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ) {
+  return ci->doAddInstantiationInc( pv, n, pv_coeff, 0, sf, effort );
 }
+
+
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h
index 3d7bbcb55..94d02de9b 100755
--- a/src/theory/quantifiers/ceg_instantiator.h
+++ b/src/theory/quantifiers/ceg_instantiator.h
@@ -38,17 +38,52 @@ public:
   virtual bool addLemma( Node lem ) = 0;
 };
 
+class Instantiator;
+
+
+//solved form, involves substitution with coefficients
+class SolvedForm {
+public:
+  std::vector< Node > d_vars;
+  std::vector< Node > d_subs;
+  std::vector< Node > d_coeff;
+  std::vector< int > d_btyp;
+  std::vector< Node > d_has_coeff;
+  Node d_theta;
+  void copy( SolvedForm& sf ){
+    d_vars.insert( d_vars.end(), sf.d_vars.begin(), sf.d_vars.end() );
+    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_btyp.insert( d_btyp.end(), sf.d_btyp.begin(), sf.d_btyp.end() );
+    d_has_coeff.insert( d_has_coeff.end(), sf.d_has_coeff.begin(), sf.d_has_coeff.end() );
+    d_theta = sf.d_theta;
+  }
+  void push_back( Node pv, Node n, Node pv_coeff, int bt ){
+    d_vars.push_back( pv );
+    d_subs.push_back( n );
+    d_coeff.push_back( pv_coeff );
+    d_btyp.push_back( bt );
+    if( !pv_coeff.isNull() ){
+      d_has_coeff.push_back( pv );
+    }
+  }
+  void pop_back( Node pv, Node n, Node pv_coeff, int bt ){
+    d_vars.pop_back();
+    d_subs.pop_back();
+    d_coeff.pop_back();
+    d_btyp.pop_back();
+    if( !pv_coeff.isNull() ){
+      d_has_coeff.pop_back();
+    }
+  }
+};
+
 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;
-  Node d_vts_sym[2];
   //program variable contains cache
   std::map< Node, std::map< Node, bool > > d_prog_var;
   std::map< Node, bool > d_inelig;
@@ -67,81 +102,116 @@ private:
   //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 );
+  void collectCeAtoms( Node n, std::map< Node, bool >& visited );  
+private:
+  //map from variables to their instantiators
+  std::map< Node, Instantiator * > d_instantiator;
+  //cache of current substitutions tried between register/unregister
+  std::map< Node, std::map< Node, std::map< Node, bool > > > d_curr_subs_proc;
+  std::map< Node, unsigned > d_curr_index;
+  //stack of temporary variables we are solving (e.g. subfields of datatypes)
+  std::vector< Node > d_stack_vars;
+  //used instantiators 
+  std::map< Node, Instantiator * > d_active_instantiators;
+  //register variable
+  void registerInstantiationVariable( Node v, unsigned index );
+  void unregisterInstantiationVariable( Node v );
+private:
   //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();
-      }
-    }
-  };
-  /*
-  class MbpBound {
-  public:
-    Node d_bound;
-    Node d_coeff;
-    Node d_vts_coeff[2];
-    Node d_lit;
-  };
-  */
   // effort=0 : do not use model value, 1: use model value, 2: one must use model value
-  bool doAddInstantiation( 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 doAddInstantiationInc( 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 doAddInstantiationCoeff( SolvedForm& sf,
-                              std::vector< Node >& vars, std::vector< int >& btyp,
-                              unsigned j, std::map< Node, Node >& cons );
-  bool doAddInstantiation( 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( TypeNode tn, Node n, SolvedForm& sf, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ) {
-    return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, vars, pv_coeff, try_coeff );
-  }
-  Node applySubstitution( TypeNode tn, 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 e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff );
+  bool doAddInstantiation( SolvedForm& sf, unsigned i, unsigned effort );
+  bool doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars );
+  //process
   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 );
-private:
-  int solve_arith( Node v, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta );
-  Node solve_dt( Node v, Node a, Node b, Node sa, Node sb );
 public:
   CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true );
+  virtual ~CegInstantiator();
   //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 );
+  //output
+  CegqiOutput * getOutput() { return d_out; }
+  //get quantifiers engine
+  QuantifiersEngine* getQuantifiersEngine() { return d_qe; }
+  
+//interface for instantiators
+public:
+  void pushStackVariable( Node v );
+  void popStackVariable();
+  bool doAddInstantiationInc( Node pv, Node n, Node pv_coeff, int bt, SolvedForm& sf, unsigned effort );
+  Node getModelValue( Node n );
+  // TODO: move to solved form?
+  Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, Node& pv_coeff, bool try_coeff = true ) {
+    return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, sf.d_vars, pv_coeff, try_coeff );
+  }
+  Node applySubstitution( TypeNode tn, 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 );
+public:
+  unsigned getNumCEAtoms() { return d_ce_atoms.size(); }
+  Node getCEAtom( unsigned i ) { return d_ce_atoms[i]; }
+  // is eligible 
+  bool isEligible( Node n );
+  // has variable 
+  bool hasVariable( Node n, Node pv );
+  bool useVtsDelta() { return d_use_vts_delta; }
+  bool useVtsInfinity() { return d_use_vts_inf; }
+  bool hasNestedQuantification() { return d_is_nested_quant; }
 };
 
+
+
+// an instantiator for individual variables
+//   will make calls into CegInstantiator::doAddInstantiationInc
+class Instantiator {
+protected:
+  TypeNode d_type;
+  bool d_closed_enum_type;
+public:
+  Instantiator( QuantifiersEngine * qe, TypeNode tn );
+  virtual ~Instantiator(){}
+  virtual void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {}
+  
+  //called when pv_coeff * pv = n, and n is eligible for instantiation
+  virtual bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort );
+  //eqc is the equivalence class of pv
+  virtual bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { return false; }
+  
+  //term_coeffs.size() = terms.size() = 2, called when term_coeff[0] * terms[0] = term_coeff[1] * terms[1], terms are eligible, and at least one of these terms contains pv
+  virtual bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
+  virtual bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { return false; }
+  
+  //called when assertion lit holds.  note that lit is unsubstituted, first must substitute/solve/check eligible
+  virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
+  virtual bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { return false; }
+  virtual bool processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) { return false; }
+  
+  //do we allow instantiation for the model value of pv
+  virtual bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
+  virtual bool allowModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return d_closed_enum_type; }
+  
+  //do we need to postprocess the solved form? did we successfully postprocess
+  virtual bool needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; }
+  virtual bool postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
+  
+  /** Identify this module (for debugging) */
+  virtual std::string identify() const { return "Default"; }
+};
+
+class ModelValueInstantiator : public Instantiator {
+public:
+  ModelValueInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
+  virtual ~ModelValueInstantiator(){}
+  bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
+  std::string identify() const { return "ModelValue"; }
+};
+
+
 }
 }
 }
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
new file mode 100644
index 000000000..3282872d6
--- /dev/null
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -0,0 +1,868 @@
+/*********************                                                        */
+/*! \file ceg_t_instantiator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of theory-specific counterexample-guided quantifier instantiation
+ **/
+ 
+#include "theory/quantifiers/ceg_t_instantiator.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/trigger.h"
+
+#include "theory/arith/partial_model.h"
+#include "theory/arith/theory_arith.h"
+#include "theory/arith/theory_arith_private.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "util/bitvector.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+Node ArithInstantiator::getModelBasedProjectionValue( CegInstantiator * ci, Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) {
+  Node val = t;
+  Trace("cbqi-bound2") << "Value : " << val << std::endl;
+  Assert( !e.getType().isInteger() || t.getType().isInteger() );
+  Assert( !e.getType().isInteger() || mt.getType().isInteger() );
+  //add rho value
+  //get the value of c*e
+  Node ceValue = me;
+  Node new_theta = theta;
+  if( !c.isNull() ){
+    Assert( c.getType().isInteger() );
+    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() && e.getType().isInteger() ){
+    Node rho;
+    //if( !mt.getType().isInteger() ){
+      //round up/down
+      //mt = NodeManager::currentNM()->mkNode(
+    //}
+    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( !d_vts_sym[0].isNull() );
+    val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, d_vts_sym[0] ) );
+    val = Rewriter::rewrite( val );
+  }
+  if( !delta_coeff.isNull() ){
+    //create delta here if necessary
+    val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, ci->getQuantifiersEngine()->getTermDatabase()->getVtsDelta() ) );
+    val = Rewriter::rewrite( val );
+  }
+  return val;
+}
+
+//this isolates the atom into solved form
+//     veq_c * pv <> val + vts_coeff_delta * delta + vts_coeff_inf * inf
+//  ensures val is Int if pv is Int, and val does not contain vts symbols
+int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) {
+  int ires = 0;
+  Trace("cbqi-inst-debug") << "isolate for " << pv << " in " << atom << std::endl;
+  std::map< Node, Node > msum;
+  if( QuantArith::getMonomialSumLit( atom, msum ) ){
+    Trace("cbqi-inst-debug") << "got monomial sum: " << std::endl;
+    if( Trace.isOn("cbqi-inst-debug") ){
+      QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" );
+    }
+    TypeNode pvtn = pv.getType();
+    //remove vts symbols from polynomial
+    Node vts_coeff[2];
+    for( unsigned t=0; t<2; t++ ){
+      if( !d_vts_sym[t].isNull() ){
+        std::map< Node, Node >::iterator itminf = msum.find( d_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( d_vts_sym[t] );
+        }
+      }
+    }
+
+    ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() );
+    if( ires!=0 ){
+      Node realPart;
+      if( Trace.isOn("cbqi-inst-debug") ){
+        Trace("cbqi-inst-debug") << "Isolate : ";
+        if( !veq_c.isNull() ){
+          Trace("cbqi-inst-debug") << veq_c << " * ";
+        }
+        Trace("cbqi-inst-debug") << pv << " " << atom.getKind() << " " << val << std::endl;
+      }
+      if( options::cbqiAll() ){
+        // when not pure LIA/LRA, we must check whether the lhs contains pv
+        if( TermDb::containsTerm( val, pv ) ){
+          Trace("cbqi-inst-debug") << "fail : contains bad term" << std::endl;
+          return 0;
+        }
+      }
+      if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){
+        //redo, split integer/non-integer parts
+        bool useCoeff = false;
+        Integer coeff = ci->getQuantifiersEngine()->getTermDatabase()->d_one.getConst<Rational>().getNumerator();
+        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+          if( it->first.isNull() || it->first.getType().isInteger() ){
+            if( !it->second.isNull() ){
+              coeff = coeff.lcm( it->second.getConst<Rational>().getDenominator() );
+              useCoeff = true;
+            }
+          }
+        }
+        //multiply everything by this coefficient
+        Node rcoeff = NodeManager::currentNM()->mkConst( Rational( coeff ) );
+        std::vector< Node > real_part;
+        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+          if( useCoeff ){
+            if( it->second.isNull() ){
+              msum[it->first] = rcoeff;
+            }else{
+              msum[it->first] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, it->second, rcoeff ) );
+            }
+          }
+          if( !it->first.isNull() && !it->first.getType().isInteger() ){
+            real_part.push_back( msum[it->first].isNull() ? it->first : NodeManager::currentNM()->mkNode( MULT, msum[it->first], it->first ) );
+          }
+        }
+        //remove delta  TODO: check this
+        vts_coeff[1] = Node::null();
+        //multiply inf
+        if( !vts_coeff[0].isNull() ){
+          vts_coeff[0] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[0] ) );
+        }
+        realPart = real_part.empty() ? ci->getQuantifiersEngine()->getTermDatabase()->d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) );
+        Assert( ci->getOutput()->isEligibleForInstantiation( realPart ) );
+        //re-isolate
+        Trace("cbqi-inst-debug") << "Re-isolate..." << std::endl;
+        ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() );
+        Trace("cbqi-inst-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl;
+        Trace("cbqi-inst-debug") << "                 real part : " << realPart << std::endl;
+        if( ires!=0 ){
+          int ires_use = ( msum[pv].isNull() || msum[pv].getConst<Rational>().sgn()==1 ) ? 1 : -1;
+          val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires_use==-1 ? PLUS : MINUS,
+                                    NodeManager::currentNM()->mkNode( ires_use==-1 ? MINUS : PLUS, val, realPart ),
+                                    NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) );  //TODO: round up for upper bounds?
+          Trace("cbqi-inst-debug") << "result : " << val << std::endl;
+          Assert( val.getType().isInteger() );
+        }
+      }
+    }
+    vts_coeff_inf = vts_coeff[0];
+    vts_coeff_delta = vts_coeff[1];
+    Trace("cbqi-inst-debug") << "Return " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << ", vts = (" << vts_coeff_inf << ", " << vts_coeff_delta << ")" << std::endl;
+  }else{
+    Trace("cbqi-inst-debug") << "fail : could not get monomial sum" << std::endl;
+  }
+  return ires;
+}
+
+void ArithInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {
+  d_vts_sym[0] = ci->getQuantifiersEngine()->getTermDatabase()->getVtsInfinity( d_type, false, false );
+  d_vts_sym[1] = ci->getQuantifiersEngine()->getTermDatabase()->getVtsDelta( false, false );
+  for( unsigned i=0; i<2; i++ ){
+    d_mbp_bounds[i].clear();
+    d_mbp_coeff[i].clear();
+    for( unsigned j=0; j<2; j++ ){
+      d_mbp_vts_coeff[i][j].clear();
+    }
+    d_mbp_lit[i].clear();
+  }
+}
+
+bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) {
+  Node eq_lhs = terms[0];
+  Node eq_rhs = terms[1];
+  Node lhs_coeff = term_coeffs[0];
+  Node rhs_coeff = term_coeffs[1];
+  //make the same coefficient
+  if( rhs_coeff!=lhs_coeff ){
+    if( !rhs_coeff.isNull() ){
+      Trace("cbqi-inst-debug") << "...mult lhs by " << rhs_coeff << std::endl;
+      eq_lhs = NodeManager::currentNM()->mkNode( MULT, rhs_coeff, eq_lhs );
+      eq_lhs = Rewriter::rewrite( eq_lhs );
+    }
+    if( !lhs_coeff.isNull() ){
+      Trace("cbqi-inst-debug") << "...mult rhs by " << lhs_coeff << std::endl;
+      eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff, eq_rhs );
+      eq_rhs = Rewriter::rewrite( eq_rhs );
+    }
+  }
+  Node eq = eq_lhs.eqNode( eq_rhs );
+  eq = Rewriter::rewrite( eq );
+  Node val;
+  Node veq_c;
+  Node vts_coeff_inf;
+  Node vts_coeff_delta;
+  //isolate pv in the equality
+  int ires = solve_arith( ci, pv, eq, veq_c, val, vts_coeff_inf, vts_coeff_delta );
+  if( ires!=0 ){
+    if( ci->doAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){
+      return true;
+    }
+  }
+
+  return false;
+}
+
+bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) {
+  Trace("cbqi-inst-debug2") << "  look at " << lit << std::endl;
+  Node atom = lit.getKind()==NOT ? lit[0] : lit;
+  bool pol = lit.getKind()!=NOT;
+  //arithmetic inequalities and disequalities
+  if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && 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 = ci->getQuantifiersEngine()->getTermDatabase()->d_zero;
+    }
+    //must be an eligible term
+    if( ci->isEligible( atom_lhs ) ){
+      //apply substitution to LHS of atom
+      Node atom_lhs_coeff;
+      atom_lhs = ci->applySubstitution( d_type, atom_lhs, sf, atom_lhs_coeff );
+      if( !atom_lhs.isNull() ){
+        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() && ci->hasVariable( atom_lhs, pv ) ){
+        Node pv_value = ci->getModelValue( pv );
+        Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs );
+        //cannot contain infinity?
+        Trace("cbqi-inst-debug") << "..[3] From assertion : " << atom << ", pol = " << pol << std::endl;
+        Trace("cbqi-inst-debug") << "         substituted : " << satom << ", pol = " << pol << std::endl;
+        Node vts_coeff_inf;
+        Node vts_coeff_delta;
+        Node val;
+        Node veq_c;
+        //isolate pv in the inequality
+        int ires = solve_arith( ci, pv, satom, veq_c, val, vts_coeff_inf, vts_coeff_delta );
+        if( ires!=0 ){
+          //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( d_type.isInteger() ){
+                  uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
+                  uval = Rewriter::rewrite( uval );
+                }else{
+                  Assert( d_type.isReal() );
+                  //now is strict inequality
+                  uires = uires*2;
+                }
+              }
+            }else{
+              bool is_upper;
+              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_inf.isNull() ){
+                  //coefficient or val won't make a difference, just compare with zero
+                  Trace("cbqi-inst-debug") << "Disequality : check infinity polarity " << vts_coeff_inf << std::endl;
+                  Assert( vts_coeff_inf.isConst() );
+                  is_upper = ( vts_coeff_inf.getConst<Rational>().sgn()==1 );
+                }else{
+                  Node rhs_value = ci->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!=ci->getQuantifiersEngine()->getTermDatabase()->d_true );
+                }
+              }else{
+                is_upper = (r==0);
+              }
+              Assert( atom.getKind()==EQUAL && !pol );
+              if( d_type.isInteger() ){
+                uires = is_upper ? -1 : 1;
+                uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
+                uval = Rewriter::rewrite( uval );
+              }else{
+                Assert( d_type.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( ci->useVtsDelta() && ( uires==2 || uires==-2 ) ){
+              if( options::cbqiModel() ){
+                Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) );
+                if( vts_coeff_delta.isNull() ){
+                  vts_coeff_delta = delta_coeff;
+                }else{
+                  vts_coeff_delta = NodeManager::currentNM()->mkNode( PLUS, vts_coeff_delta, delta_coeff );
+                  vts_coeff_delta = Rewriter::rewrite( vts_coeff_delta );
+                }
+              }else{
+                Node delta = ci->getQuantifiersEngine()->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;
+              d_mbp_bounds[index].push_back( uval );
+              d_mbp_coeff[index].push_back( veq_c );
+              Trace("cbqi-inst-debug") << "Store bound " << index << " " << uval << " " << veq_c << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl;
+              for( unsigned t=0; t<2; t++ ){
+                d_mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta );
+              }
+              d_mbp_lit[index].push_back( lit );
+            }else{
+              //try this bound
+              if( ci->doAddInstantiationInc( pv, uval, veq_c, uires>0 ? 1 : -1, sf, effort ) ){
+                return true;
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+
+
+  return false;
+}
+
+bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) {
+ if( options::cbqiModel() ){
+    bool use_inf = ci->useVtsInfinity() && ( d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() );
+    bool upper_first = false;
+    if( options::cbqiMinBounds() ){
+      upper_first = d_mbp_bounds[1].size()<d_mbp_bounds[0].size();
+    }
+    int best_used[2];
+    std::vector< Node > t_values[3];
+    Node zero = ci->getQuantifiersEngine()->getTermDatabase()->d_zero;
+    Node one = ci->getQuantifiersEngine()->getTermDatabase()->d_one;
+    Node pv_value = ci->getModelValue( pv );
+    //try optimal bounds
+    for( unsigned r=0; r<2; r++ ){
+      int rr = upper_first ? (1-r) : r;
+      best_used[rr] = -1;
+      if( d_mbp_bounds[rr].empty() ){
+        if( use_inf ){
+          Trace("cbqi-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << d_type << ")" << std::endl;
+          //no bounds, we do +- infinity
+          Node val = ci->getQuantifiersEngine()->getTermDatabase()->getVtsInfinity( d_type );
+          //TODO : rho value for infinity?
+          if( rr==0 ){
+            val = NodeManager::currentNM()->mkNode( UMINUS, val );
+            val = Rewriter::rewrite( val );
+          }
+          if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){
+            return true;
+          }
+        }
+      }else{
+        Trace("cbqi-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << d_type << ") : " << std::endl;
+        int best = -1;
+        Node best_bound_value[3];
+        for( unsigned j=0; j<d_mbp_bounds[rr].size(); j++ ){
+          Node value[3];
+          if( Trace.isOn("cbqi-bound") ){
+            Assert( !d_mbp_bounds[rr][j].isNull() );
+            Trace("cbqi-bound") << "  " << j << ": " << d_mbp_bounds[rr][j];
+            if( !d_mbp_vts_coeff[rr][0][j].isNull() ){
+              Trace("cbqi-bound") << " (+ " << d_mbp_vts_coeff[rr][0][j] << " * INF)";
+            }
+            if( !d_mbp_vts_coeff[rr][1][j].isNull() ){
+              Trace("cbqi-bound") << " (+ " << d_mbp_vts_coeff[rr][1][j] << " * DELTA)";
+            }
+            if( !d_mbp_coeff[rr][j].isNull() ){
+              Trace("cbqi-bound") << " (div " << d_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] = d_mbp_vts_coeff[rr][0][j];
+              if( !value[0].isNull() ){
+                Trace("cbqi-bound") << "( " << value[0] << " * INF ) + ";
+              }else{
+                value[0] = zero;
+              }
+            }else if( t==1 ){
+              Node t_value = ci->getModelValue( d_mbp_bounds[rr][j] );
+              t_values[rr][j] = t_value;
+              value[1] = t_value;
+              Trace("cbqi-bound") << value[1];
+            }else{
+              value[2] = d_mbp_vts_coeff[rr][1][j];
+              if( !value[2].isNull() ){
+                Trace("cbqi-bound") << " + ( " << value[2] << " * DELTA )";
+              }else{
+                value[2] = zero;
+              }
+            }
+            //multiply by coefficient
+            if( value[t]!=zero && !d_mbp_coeff[rr][j].isNull() ){
+              Assert( d_mbp_coeff[rr][j].isConst() );
+              value[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / d_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!=ci->getQuantifiersEngine()->getTermDatabase()->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]!=zero ){
+            Trace("cbqi-bound") << "( " << best_bound_value[0] << " * INF ) + ";
+          }
+          Trace("cbqi-bound") << best_bound_value[1];
+          if( best_bound_value[2]!=zero ){
+            Trace("cbqi-bound") << " + ( " << best_bound_value[2] << " * DELTA )";
+          }
+          Trace("cbqi-bound") << std::endl;
+          best_used[rr] = best;
+          //if using cbqiMidpoint, only add the instance based on one bound if the bound is non-strict
+          if( !options::cbqiMidpoint() || d_type.isInteger() || d_mbp_vts_coeff[rr][1][best].isNull() ){
+            Node val = d_mbp_bounds[rr][best];
+            val = getModelBasedProjectionValue( ci, pv, val, rr==0, d_mbp_coeff[rr][best], pv_value, t_values[rr][best], sf.d_theta,
+                                                d_mbp_vts_coeff[rr][0][best], d_mbp_vts_coeff[rr][1][best] );
+            if( !val.isNull() ){
+              if( ci->doAddInstantiationInc( pv, val, d_mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, effort ) ){
+                return true;
+              }
+            }
+          }
+        }
+      }
+    }
+    //if not using infinity, use model value of zero
+    if( !use_inf && d_mbp_bounds[0].empty() && d_mbp_bounds[1].empty() ){
+      Node val = zero;
+      Node c; //null (one) coefficient
+      val = getModelBasedProjectionValue( ci, pv, val, true, c, pv_value, zero, sf.d_theta, Node::null(), Node::null() );
+      if( !val.isNull() ){
+        if( ci->doAddInstantiationInc( pv, val, c, 0, sf, effort ) ){
+          return true;
+        }
+      }
+    }
+    if( options::cbqiMidpoint() && !d_type.isInteger() ){
+      Node vals[2];
+      bool bothBounds = true;
+      Trace("cbqi-bound") << "Try midpoint of bounds..." << std::endl;
+      for( unsigned rr=0; rr<2; rr++ ){
+        int best = best_used[rr];
+        if( best==-1 ){
+          bothBounds = false;
+        }else{
+          vals[rr] = d_mbp_bounds[rr][best];
+          vals[rr] = getModelBasedProjectionValue( ci, pv, vals[rr], rr==0, Node::null(), pv_value, t_values[rr][best], sf.d_theta,
+                                                   d_mbp_vts_coeff[rr][0][best], Node::null() );
+        }
+        Trace("cbqi-bound") << "Bound : " << vals[rr] << std::endl;
+      }
+      Node val;
+      if( bothBounds ){
+        Assert( !vals[0].isNull() && !vals[1].isNull() );
+        if( vals[0]==vals[1] ){
+          val = vals[0];
+        }else{
+          val = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkNode( PLUS, vals[0], vals[1] ),
+                                                        NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ) );
+          val = Rewriter::rewrite( val );
+        }
+      }else{
+        if( !vals[0].isNull() ){
+          val = NodeManager::currentNM()->mkNode( PLUS, vals[0], one );
+          val = Rewriter::rewrite( val );
+        }else if( !vals[1].isNull() ){
+          val = NodeManager::currentNM()->mkNode( MINUS, vals[1], one );
+          val = Rewriter::rewrite( val );
+        }
+      }
+      Trace("cbqi-bound") << "Midpoint value : " << val << std::endl;
+      if( !val.isNull() ){
+        if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){
+          return true;
+        }
+      }
+    }
+    //generally should not make it to this point FIXME: write proper assertion
+    //Assert( ( ci->hasNestedQuantification() && !options::cbqiNestedQE() ) || options::cbqiAll() );
+    
+    if( options::cbqiNopt() ){
+      //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<d_mbp_bounds[rr].size(); j++ ){
+          if( (int)j!=best_used[rr] && ( !options::cbqiMidpoint() || d_mbp_vts_coeff[rr][1][j].isNull() ) ){
+            Node val = getModelBasedProjectionValue( ci, pv, d_mbp_bounds[rr][j], rr==0, d_mbp_coeff[rr][j], pv_value, t_values[rr][j], sf.d_theta,
+                                                     d_mbp_vts_coeff[rr][0][j], d_mbp_vts_coeff[rr][1][j] );
+            if( !val.isNull() ){
+              if( ci->doAddInstantiationInc( pv, val, d_mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, effort ) ){
+                return true;
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+  return false;
+}
+
+bool ArithInstantiator::needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {
+  return std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), pv )!=sf.d_has_coeff.end();
+}
+
+bool ArithInstantiator::postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {
+  Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), pv )!=sf.d_has_coeff.end() );
+  Assert( std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )!=sf.d_vars.end() );
+  unsigned index = std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )-sf.d_vars.begin();
+  Assert( !sf.d_coeff[index].isNull() );
+  Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_coeff[index] << " * " << sf.d_vars[index] << " = " << sf.d_subs[index] << std::endl;
+  Assert( sf.d_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], sf.d_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( sf.d_vars[index], msum, veq, EQUAL, true )!=0 ){
+      Node veq_c;
+      if( veq[0]!=sf.d_vars[index] ){
+        Node veq_v;
+        if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){
+          Assert( veq_v==sf.d_vars[index] );
+        }
+      }
+      sf.d_subs[index] = veq[1];
+      if( !veq_c.isNull() ){
+        sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, veq[1], veq_c );
+        Trace("cbqi-inst-debug") << "...bound type is : " << sf.d_btyp[index] << std::endl;
+        //intger division rounding up if from a lower bound
+        if( sf.d_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_TOTAL, veq[1], veq_c ),
+                ci->getQuantifiersEngine()->getTermDatabase()->d_zero ),
+              ci->getQuantifiersEngine()->getTermDatabase()->d_zero, ci->getQuantifiersEngine()->getTermDatabase()->d_one )
+          );
+        }
+      }
+      Trace("cbqi-inst-debug") << "...normalize integers : " << sf.d_vars[index] << " -> " << sf.d_subs[index] << std::endl;
+    }else{
+      Trace("cbqi-inst-debug") << "...failed to isolate." << std::endl;
+      return false;
+    }
+  }else{
+    Trace("cbqi-inst-debug") << "...failed to get monomial sum." << std::endl;
+    return false;
+  }
+  return true;
+}
+
+void DtInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {
+
+}
+
+Node DtInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) {
+  Trace("cbqi-inst-debug2") << "Solve dt : " << v << " " << a << " " << b << " " << sa << " " << sb << std::endl;
+  Node ret;
+  if( !a.isNull() && a==v ){
+    ret = sb;
+  }else if( !b.isNull() && b==v ){
+    ret = sa;
+  }else if( !a.isNull() && a.getKind()==APPLY_CONSTRUCTOR ){
+    if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){
+      if( a.getOperator()==b.getOperator() ){
+        for( unsigned i=0; i<a.getNumChildren(); i++ ){
+          Node s = solve_dt( v, a[i], b[i], sa[i], sb[i] );
+          if( !s.isNull() ){
+            return s;
+          }
+        }
+      }
+    }else{
+      unsigned cindex = Datatype::indexOf( a.getOperator().toExpr() );
+      TypeNode tn = a.getType();
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      for( unsigned i=0; i<a.getNumChildren(); i++ ){
+        Node nn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][i].getSelector() ), sb );
+        Node s = solve_dt( v, a[i], Node::null(), sa[i], nn );
+        if( !s.isNull() ){
+          return s;
+        }
+      }
+    }
+  }else if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){
+    return solve_dt( v, b, a, sb, sa );
+  }
+  if( !ret.isNull() ){
+    //ensure does not contain
+    if( TermDb::containsTerm( ret, v ) ){
+      ret = Node::null();
+    }
+  }
+  return ret;
+}
+
+bool DtInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) {
+  Trace("cbqi-inst-debug") << "[2] try based on constructors in equivalence class." << std::endl;
+  //[2] look in equivalence class for a constructor
+  for( unsigned k=0; k<eqc.size(); k++ ){
+    Node n = eqc[k];
+    if( n.getKind()==APPLY_CONSTRUCTOR ){
+      Trace("cbqi-inst-debug") << "...try based on constructor term " << n << std::endl;
+      std::vector< Node > children;
+      children.push_back( n.getOperator() );
+      const Datatype& dt = ((DatatypeType)(d_type).toType()).getDatatype();
+      unsigned cindex = Datatype::indexOf( n.getOperator().toExpr() );
+      //now must solve for selectors applied to pv
+      for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){
+        Node c = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv );
+        ci->pushStackVariable( c );
+        children.push_back( c );
+      }
+      Node val = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
+      if( ci->doAddInstantiationInc( pv, val, Node::null(), 0, sf, effort ) ){
+        return true;
+      }else{
+        //cleanup
+        for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){
+          ci->popStackVariable();
+        }
+        break;
+      }
+    }
+  }
+  return false;
+}
+
+bool DtInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) {
+  Node val = solve_dt( pv, terms[0], terms[1], terms[0], terms[1] );
+  if( !val.isNull() ){
+    Node veq_c;
+    if( ci->doAddInstantiationInc( pv, val, veq_c, 0, sf, effort ) ){
+      return true;
+    }
+  }
+  return false;
+}
+
+void EprInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {
+  d_equal_terms.clear();
+}
+
+bool EprInstantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ) {
+  if( options::quantEprMatching() ){
+    Assert( pv_coeff.isNull() );
+    d_equal_terms.push_back( n ); 
+    return false;  
+  }else{
+    return ci->doAddInstantiationInc( pv, n, pv_coeff, 0, sf, effort );
+  }
+}
+
+void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, std::vector< Node >& arg_reps, TermArgTrie * tat, unsigned index, std::map< Node, int >& match_score ) {
+  if( index==catom.getNumChildren() ){
+    Assert( tat->hasNodeData() );
+    Node gcatom = tat->getNodeData();
+    Trace("epr-inst") << "Matched : " << catom << " and " << gcatom << std::endl;
+    for( unsigned i=0; i<catom.getNumChildren(); i++ ){
+      if( catom[i]==pv ){
+        Trace("epr-inst") << "...increment " << gcatom[i] << std::endl;
+        match_score[gcatom[i]]++;
+      }else{
+        //recursive matching
+        computeMatchScore( ci, pv, catom[i], gcatom[i], match_score );
+      }
+    }
+  }else{
+    std::map< TNode, TermArgTrie >::iterator it = tat->d_data.find( arg_reps[index] );
+    if( it!=tat->d_data.end() ){
+      computeMatchScore( ci, pv, catom, arg_reps, &it->second, index+1, match_score );
+    }
+  }
+}
+
+void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, Node eqc, std::map< Node, int >& match_score ) {
+  if( inst::Trigger::isAtomicTrigger( catom ) && TermDb::containsTerm( catom, pv ) ){
+    Trace("epr-inst") << "Find matches for " << catom << "..." << std::endl;
+    std::vector< Node > arg_reps;
+    for( unsigned j=0; j<catom.getNumChildren(); j++ ){
+      arg_reps.push_back( ci->getQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( catom[j] ) );
+    }
+    if( ci->getQuantifiersEngine()->getMasterEqualityEngine()->hasTerm( eqc ) ){
+      Node rep = ci->getQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( eqc );
+      Node op = ci->getQuantifiersEngine()->getTermDatabase()->getMatchOperator( catom );
+      TermArgTrie * tat = ci->getQuantifiersEngine()->getTermDatabase()->getTermArgTrie( rep, op );
+      Trace("epr-inst") << "EPR instantiation match term : " << catom << ", check ground terms=" << (tat!=NULL) << std::endl;
+      if( tat ){
+        computeMatchScore( ci, pv, catom, arg_reps, tat, 0, match_score );
+      }
+    }
+  }
+}
+
+struct sortEqTermsMatch {
+  std::map< Node, int > d_match_score;
+  bool operator() (Node i, Node j) {
+    int match_score_i = d_match_score[i];
+    int match_score_j = d_match_score[j];
+    return match_score_i>match_score_j || ( match_score_i==match_score_j && i<j );
+  }
+};
+
+    
+bool EprInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) {
+  if( options::quantEprMatching() ){
+    //heuristic for best matching constant
+    sortEqTermsMatch setm;
+    for( unsigned i=0; i<ci->getNumCEAtoms(); i++ ){
+      Node catom = ci->getCEAtom( i );
+      computeMatchScore( ci, pv, catom, catom, setm.d_match_score );
+    }
+    //sort by match score
+    std::sort( d_equal_terms.begin(), d_equal_terms.end(), setm );
+    Node pv_coeff;
+    for( unsigned i=0; i<d_equal_terms.size(); i++ ){
+      if( ci->doAddInstantiationInc( pv, d_equal_terms[i], pv_coeff, 0, sf, effort ) ){
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+bool BvInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) {
+  /*   TODO: algebraic reasoning for bitvector instantiation
+  if( atom.getKind()==BITVECTOR_ULT || atom.getKind()==BITVECTOR_ULE ){
+    for( unsigned t=0; t<2; t++ ){
+      if( atom[t]==pv ){
+        computeProgVars( atom[1-t] );
+        if( d_inelig.find( atom[1-t] )==d_inelig.end() ){
+          //only ground terms  TODO: more
+          if( d_prog_var[atom[1-t]].empty() ){
+            Node veq_c;
+            Node uval;
+            if( ( !pol && atom.getKind()==BITVECTOR_ULT ) || ( pol && atom.getKind()==BITVECTOR_ULE ) ){
+              uval = atom[1-t];
+            }else{
+              uval = NodeManager::currentNM()->mkNode( (atom.getKind()==BITVECTOR_ULT)==(t==1) ? BITVECTOR_PLUS : BITVECTOR_SUB, atom[1-t], 
+                                                       bv::utils::mkConst(pvtn.getConst<BitVectorSize>(), 1) );
+            }
+            if( doAddInstantiationInc( pv, uval, veq_c, 0, sf, effort ) ){
+              return true;
+            }
+          }
+        }
+      }
+    }
+  }
+  */
+
+  return false;
+}
+
+
diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h
new file mode 100644
index 000000000..2df7946d5
--- /dev/null
+++ b/src/theory/quantifiers/ceg_t_instantiator.h
@@ -0,0 +1,93 @@
+/*********************                                                        */
+/*! \file ceg_t_instantiator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief theory-specific counterexample-guided quantifier instantiation
+ **/
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CEG_T_INSTANTIATOR_H
+#define __CVC4__CEG_T_INSTANTIATOR_H
+
+#include "theory/quantifiers/ceg_instantiator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class ArithInstantiator : public Instantiator {
+private:
+  Node d_vts_sym[2];
+  std::vector< Node > d_mbp_bounds[2];
+  std::vector< Node > d_mbp_coeff[2];
+  std::vector< Node > d_mbp_vts_coeff[2][2];
+  std::vector< Node > d_mbp_lit[2];
+  int solve_arith( CegInstantiator * ci, Node v, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta );
+  Node getModelBasedProjectionValue( CegInstantiator * ci, Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff );
+public:
+  ArithInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
+  virtual ~ArithInstantiator(){}
+  void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
+  bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
+  bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort );
+  bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
+  bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort );
+  bool processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort );
+  bool needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
+  bool postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
+  std::string identify() const { return "Arith"; }
+};
+
+class DtInstantiator : public Instantiator {
+private:
+  Node solve_dt( Node v, Node a, Node b, Node sa, Node sb );
+public:
+  DtInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
+  virtual ~DtInstantiator(){}
+  void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
+  bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort );
+  bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
+  bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort );
+  std::string identify() const { return "Dt"; }
+};
+
+class TermArgTrie;
+
+class EprInstantiator : public Instantiator {
+private:
+  std::vector< Node > d_equal_terms;
+  void computeMatchScore( CegInstantiator * ci, Node pv, Node catom, std::vector< Node >& arg_reps, TermArgTrie * tat, unsigned index, std::map< Node, int >& match_score );
+  void computeMatchScore( CegInstantiator * ci, Node pv, Node catom, Node eqc, std::map< Node, int >& match_score );
+public:
+  EprInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
+  virtual ~EprInstantiator(){}
+  void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
+  bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort );
+  bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort );
+  std::string identify() const { return "Epr"; }
+};
+
+class BvInstantiator : public Instantiator {
+public:
+  BvInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
+  virtual ~BvInstantiator(){}
+  bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort );
+  bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
+  std::string identify() const { return "Bv"; }
+};
+
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index f4eb67d74..11adc61fd 100755
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -84,6 +84,9 @@ d_notify( *this ),
 d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false),
 d_ee_conjectures( c ){
   d_fullEffortCount = 0;
+  d_conj_count = 0;
+  d_subs_confirmCount = 0;
+  d_subs_unkCount = 0;
   d_uequalityEngine.addFunctionKind( kind::APPLY_UF );
   d_uequalityEngine.addFunctionKind( kind::APPLY_CONSTRUCTOR );
 
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index be608aeaa..72057e734 100755
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -589,7 +589,7 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
 }
 
 
-bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
+int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
   Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;
   Assert( !d_qe->inConflict() );
   if( optUseModel() ){
@@ -723,15 +723,15 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
           if( temp.addEntry(fmfmc, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){
             if( !exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j ) ){
               //something went wrong, resort to exhaustive instantiation
-              return false;
+              return 0;
             }
           }
         }
       }
     }
-    return true;
+    return 1;
   }else{
-    return false;
+    return 0;
   }
 }
 
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 411b7a5eb..7d21b4185 100755
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -139,7 +139,7 @@ public:
   void debugPrintCond(const char * tr, Node n, bool dispStar = false);
   void debugPrint(const char * tr, Node n, bool dispStar = false);
 
-  bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
+  int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
 
   Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );
 
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 7e5424d9c..12e15d353 100755
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -258,7 +258,11 @@ void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::
         }
       }
     }else{
-      insts.push_back( qe->getInstantiation( q, terms, true ) );
+      if( hasInstLemma() ){
+        insts.push_back( getInstLemma() );
+      }else{
+        insts.push_back( qe->getInstantiation( q, terms, true ) );
+      }
     }
   }else{
     for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
@@ -428,13 +432,17 @@ void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std
     if( terms.size()==q[0].getNumChildren() ){
       if( useActive ){
         if( hasInstLemma() ){
-          Node lem;
+          Node lem = getInstLemma();
           if( std::find( active.begin(), active.end(), lem )!=active.end() ){
             insts.push_back( lem );
           }
         }
       }else{
-        insts.push_back( qe->getInstantiation( q, terms, true ) );
+        if( hasInstLemma() ){
+          insts.push_back( getInstLemma() );
+        }else{
+          insts.push_back( qe->getInstantiation( q, terms, true ) );
+        }
       }
     }else{
       for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index b3df9ca5d..2a940f1fd 100755
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -388,23 +388,6 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif
   return addedLemmas;
 }
 
-int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){
-  Assert( options::eagerInstQuant() );
-  if( !d_match_pattern.isNull() ){
-    InstMatch m( f );
-    if( getMatch( f, t, m, qe ) ){
-      if( qe->addInstantiation( f, m ) ){
-        return 1;
-      }
-    }
-  }else{
-    for( unsigned i=0; i<d_children.size(); i++ ){
-      d_children[i]->addTerm( f, t, qe );
-    }
-  }
-  return 0;
-}
-
 
 InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, Node pat, QuantifiersEngine* qe ) {
   std::vector< Node > pats;
@@ -716,22 +699,6 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe,
   }
 }
 
-int InstMatchGeneratorMulti::addTerm( Node q, Node t, QuantifiersEngine* qe ){
-  Assert( options::eagerInstQuant() );
-  int addedLemmas = 0;
-  for( int i=0; i<(int)d_children.size(); i++ ){
-    Node t_op = qe->getTermDatabase()->getMatchOperator( t );
-    if( ((InstMatchGenerator*)d_children[i])->d_match_pattern_op==t_op ){
-      InstMatch m( q );
-      //if it produces a match, then process it with the rest
-      if( ((InstMatchGenerator*)d_children[i])->getMatch( q, t, m, qe ) ){
-        processNewMatch( qe, m, i, addedLemmas );
-      }
-    }
-  }
-  return addedLemmas;
-}
-
 InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat, QuantifiersEngine* qe ) : d_f( q ), d_match_pattern( pat ) {
   if( d_match_pattern.getKind()==NOT ){
     d_match_pattern = d_match_pattern[0];
@@ -774,17 +741,19 @@ int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, Q
       Node r = qe->getEqualityQuery()->getRepresentative( d_eqc );
       //iterate over all classes except r
       tat = qe->getTermDatabase()->getTermArgTrie( Node::null(), d_op );
-      for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
-        if( it->first!=r ){
-          InstMatch m( q );
-          m.add( baseMatch );
-          addInstantiations( m, qe, addedLemmas, 0, &(it->second) );
-          if( qe->inConflict() ){
-            break;
+      if( tat ){
+        for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
+          if( it->first!=r ){
+            InstMatch m( q );
+            m.add( baseMatch );
+            addInstantiations( m, qe, addedLemmas, 0, &(it->second) );
+            if( qe->inConflict() ){
+              break;
+            }
           }
         }
+        tat = NULL;
       }
-      tat = NULL;
     }
   }
   Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl;
@@ -841,20 +810,6 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin
   }
 }
 
-int InstMatchGeneratorSimple::addTerm( Node q, Node t, QuantifiersEngine* qe ){
-  //for eager instantiation only
-  Assert( options::eagerInstQuant() );
-  InstMatch m( q );
-  for( unsigned i=0; i<t.getNumChildren(); i++ ){
-    if( d_match_pattern[i].getKind()==INST_CONSTANT ){
-      m.setValue(d_var_num[i], t[i]);
-    }else if( !qe->getEqualityQuery()->areEqual( d_match_pattern[i], t[i] ) ){
-      return 0;
-    }
-  }
-  return qe->addInstantiation( q, m ) ? 1 : 0;
-}
-
 int InstMatchGeneratorSimple::getActiveScore( QuantifiersEngine * qe ) {
   Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
   unsigned ngt = qe->getTermDatabase()->getNumGroundTerms( f );
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index 65c5a1427..c238e3c4e 100755
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -42,8 +42,6 @@ public:
   virtual bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) = 0;
   /** add instantiations directly */
   virtual int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;
-  /** add ground term t, called when t is added to term db */
-  virtual int addTerm( Node q, Node t, QuantifiersEngine* qe ) { return 0; }
   /** set active add */
   virtual void setActiveAdd( bool val ) {}
   /** get active score */
@@ -113,8 +111,6 @@ public:
   bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
   /** add instantiations */
   int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
-  /** add ground term t */
-  int addTerm( Node q, Node t, QuantifiersEngine* qe );
 
   bool d_active_add;
   void setActiveAdd( bool val );
@@ -205,8 +201,6 @@ public:
   bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return false; }
   /** add instantiations */
   int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
-  /** add ground term t */
-  int addTerm( Node q, Node t, QuantifiersEngine* qe );
 };/* class InstMatchGeneratorMulti */
 
 /** smart (single)-trigger implementation */
@@ -240,8 +234,6 @@ public:
   bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return false; }
   /** add instantiations */
   int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
-  /** add ground term t, possibly add instantiations */
-  int addTerm( Node q, Node t, QuantifiersEngine* qe );
   /** get active score */
   int getActiveScore( QuantifiersEngine * qe );
 };/* class InstMatchGeneratorSimple */
diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index 41c9c40c8..1f68fb787 100755
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -597,6 +597,8 @@ void InstPropagator::InstInfo::init( Node q, Node lem, std::vector< Node >& term
 
 InstPropagator::InstPropagator( QuantifiersEngine* qe ) :
 d_qe( qe ), d_notify(*this), d_qy( qe ){
+  d_icount = 1;
+  d_conflict = false;
 }
 
 bool InstPropagator::reset( Theory::Effort e ) {
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 523d868b5..ac6e1edbe 100755
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/trigger.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/theory_engine.h"
 
 using namespace std;
@@ -34,9 +35,13 @@ using namespace CVC4::theory::arith;
 #define ARITH_INSTANTIATOR_USE_MINUS_DELTA
 
 InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe )
-  : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() )
+  : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ), 
+d_elim_quants( qe->getSatContext() ),
+d_nested_qe_waitlist_size( qe->getUserContext() ),
+d_nested_qe_waitlist_proc( qe->getUserContext() )
 //, d_added_inst( qe->getUserContext() )
 {
+  d_qid_count = 0;
 }
 
 InstStrategyCbqi::~InstStrategyCbqi() throw(){}
@@ -55,34 +60,117 @@ unsigned InstStrategyCbqi::needsModel( Theory::Effort e ) {
   return QuantifiersEngine::QEFFORT_NONE;
 }
 
+bool InstStrategyCbqi::registerCbqiLemma( Node q ) {
+  if( !hasAddedCbqiLemma( q ) ){
+    d_added_cbqi_lemma.insert( q );
+    Trace("cbqi-debug") << "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-lemma") << "Counterexample lemma : " << lem << std::endl;
+      registerCounterexampleLemma( q, lem );
+      
+      //totality lemmas for EPR
+      QuantEPR * qepr = d_quantEngine->getQuantEPR();
+      if( qepr!=NULL ){   
+        for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+          TypeNode tn = q[0][i].getType();
+          if( tn.isSort() ){
+            if( qepr->isEPR( tn ) ){
+              //add totality lemma
+              std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn );
+              if( itc!=qepr->d_consts.end() ){
+                Assert( !itc->second.empty() );
+                Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i );
+                std::vector< Node > disj;
+                for( unsigned j=0; j<itc->second.size(); j++ ){
+                  disj.push_back( ic.eqNode( itc->second[j] ) );
+                }
+                Node tlem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj );
+                Trace("cbqi-lemma") << "EPR totality lemma : " << tlem << std::endl;
+                d_quantEngine->getOutputChannel().lemma( tlem );
+              }else{
+                Assert( false );
+              }                  
+            }else{
+              Assert( !options::cbqiAll() );
+            }
+          }
+        }
+      }      
+      
+      //compute dependencies between quantified formulas
+      if( options::cbqiLitDepend() || options::cbqiInnermost() ){
+        std::vector< Node > ics;
+        TermDb::computeVarContains( q, ics );
+        d_parent_quant[q].clear();
+        d_children_quant[q].clear();
+        std::vector< Node > dep;
+        for( unsigned i=0; i<ics.size(); i++ ){
+          Node qi = ics[i].getAttribute(InstConstantAttribute());
+          if( std::find( d_parent_quant[q].begin(), d_parent_quant[q].end(), qi )==d_parent_quant[q].end() ){
+            d_parent_quant[q].push_back( qi );
+            d_children_quant[qi].push_back( q );
+            Node qicel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( qi );
+            dep.push_back( qi );
+            dep.push_back( qicel );
+          }
+        }
+        if( !dep.empty() ){
+          Node dep_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, ceLit, NodeManager::currentNM()->mkNode( kind::AND, dep ) );
+          Trace("cbqi-lemma") << "Counterexample dependency lemma : " << dep_lemma << std::endl;
+          d_quantEngine->getOutputChannel().lemma( dep_lemma );
+        }
+      }
+      
+      //must register all sub-quantifiers of counterexample lemma, register their lemmas
+      std::vector< Node > quants;
+      TermDb::computeQuantContains( lem, quants );
+      for( unsigned i=0; i<quants.size(); i++ ){
+        if( doCbqi( quants[i] ) ){
+          registerCbqiLemma( quants[i] );
+        }
+        if( options::cbqiNestedQE() ){
+          //record these as counterexample quantifiers
+          QAttributes qa;
+          TermDb::computeQuantAttributes( quants[i], qa );
+          if( !qa.d_qid_num.isNull() ){
+            d_id_to_ce_quant[ qa.d_qid_num ] = quants[i];
+            d_ce_quant_to_id[ quants[i] ] = qa.d_qid_num;
+            Trace("cbqi-nqe") << "CE quant id = " << qa.d_qid_num << " is " << quants[i] << std::endl;
+          }
+        }
+      }
+    }
+    return true;
+  }else{
+    return false;
+  }
+}
+
 void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
   d_cbqi_set_quant_inactive = false;
   d_incomplete_check = false;
+  d_active_quant.clear();
   //check if any cbqi lemma has not been added yet
   for( unsigned 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( doCbqi( q ) ){
-      if( !hasAddedCbqiLemma( q ) ){
-        d_added_cbqi_lemma.insert( q );
-        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 );
-        }
+      if( registerCbqiLemma( q ) ){
+        Debug("cbqi-debug") << "Registered cbqi lemma." << std::endl;
       //set inactive the quantified formulas whose CE literals are asserted false
       }else if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
+        d_active_quant[q] = true;
         Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl;
         Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
         bool value;
@@ -92,8 +180,24 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
             if( d_quantEngine->getValuation().isDecision( cel ) ){
               Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
             }else{
+              Trace("cbqi") << "Inactive : " << q << std::endl;
               d_quantEngine->getModel()->setQuantifierActive( q, false );
               d_cbqi_set_quant_inactive = true;
+              d_active_quant.erase( q );
+              d_elim_quants.insert( q );
+              Trace("cbqi-nqe") << "Inactive, waitlist proc/size = " << d_nested_qe_waitlist_proc[q].get() << "/" << d_nested_qe_waitlist_size[q].get() << std::endl;
+              //process from waitlist
+              while( d_nested_qe_waitlist_proc[q]<d_nested_qe_waitlist_size[q] ){
+                int index = d_nested_qe_waitlist_proc[q];
+                Assert( index>=0 );
+                Assert( index<(int)d_nested_qe_waitlist[q].size() );
+                Node nq = d_nested_qe_waitlist[q][index];
+                Node nqeqn = doNestedQENode( d_nested_qe_info[nq].d_q, q, nq, d_nested_qe_info[nq].d_inst_terms, d_nested_qe_info[nq].d_doVts );
+                Node dqelem = nq.iffNode( nqeqn ); 
+                Trace("cbqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl;
+                d_quantEngine->getOutputChannel().lemma( dqelem );
+                d_nested_qe_waitlist_proc[q] = index + 1;
+              }
             }
           }
         }else{
@@ -102,6 +206,34 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
       }
     }
   }
+
+  //refinement: only consider innermost active quantified formulas
+  if( options::cbqiInnermost() ){
+    if( !d_children_quant.empty() && !d_active_quant.empty() ){
+      Trace("cbqi-debug") << "Find non-innermost quantifiers..." << std::endl;
+      std::vector< Node > ninner;
+      for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
+        std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( it->first );
+        if( itc!=d_children_quant.end() ){
+          for( unsigned j=0; j<itc->second.size(); j++ ){
+            if( d_active_quant.find( itc->second[j] )!=d_active_quant.end() ){
+              Trace("cbqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl;
+              ninner.push_back( it->first );
+              break;
+            }
+          }
+        }
+      } 
+      Trace("cbqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl;
+      for( unsigned i=0; i<ninner.size(); i++ ){
+        Assert( d_active_quant.find( ninner[i] )!=d_active_quant.end() );
+        d_active_quant.erase( ninner[i] );
+      }
+      Assert( !d_active_quant.empty() );
+      Trace("cbqi-debug") << "...done removing." << std::endl;
+    }
+  }
+  
   processResetInstantiationRound( effort );
 }
 
@@ -115,13 +247,20 @@ void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) {
     }
     unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
     for( int ee=0; ee<=1; ee++ ){
-      for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-        Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
-        if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
+      //for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+      //  Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+      //  if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
+      for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
+        Node q = it->first;
+        Trace("cbqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl;
+        if( d_nested_qe.find( q )==d_nested_qe.end() ){
           process( q, e, ee );
           if( d_quantEngine->inConflict() ){
             break;
           }
+        }else{
+          Trace("cbqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl;
+          Assert( false );
         }
       }
       if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
@@ -146,11 +285,88 @@ bool InstStrategyCbqi::checkComplete() {
   }
 }
 
+bool InstStrategyCbqi::checkCompleteFor( Node q ) {
+  std::map< Node, int >::iterator it = d_do_cbqi.find( q );
+  if( it!=d_do_cbqi.end() ){
+    return it->second>0;
+  }else{
+    return false;
+  }
+}
+
+Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ){
+  std::map< Node, Node >::iterator it = visited.find( n );
+  if( it==visited.end() ){
+    Node ret = n;
+    if( n.getKind()==FORALL ){
+      QAttributes qa;
+      TermDb::computeQuantAttributes( n, qa );
+      if( qa.d_qid_num.isNull() ){
+        std::vector< Node > rc;
+        rc.push_back( n[0] );
+        rc.push_back( getIdMarkedQuantNode( n[1], visited ) );
+        Node avar = NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() );
+        QuantIdNumAttribute ida;
+        avar.setAttribute(ida,d_qid_count);
+        d_qid_count++;
+        std::vector< Node > iplc;
+        iplc.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, avar ) );
+        if( n.getNumChildren()==3 ){
+          for( unsigned i=0; i<n[2].getNumChildren(); i++ ){
+            iplc.push_back( n[2][i] );
+          }
+        }
+        rc.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, iplc ) );
+        ret = NodeManager::currentNM()->mkNode( FORALL, rc );
+      }
+    }else if( n.getNumChildren()>0 ){
+      std::vector< Node > children;
+      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+        children.push_back( n.getOperator() );
+      }
+      bool childChanged = false;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        Node nc = getIdMarkedQuantNode( n[i], visited );
+        childChanged = childChanged || nc!=n[i];
+        children.push_back( nc );
+      }
+      if( childChanged ){
+        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+      }
+    }
+    visited[n] = ret;
+    return ret;
+  }else{
+    return it->second;
+  }
+}
+
 void InstStrategyCbqi::preRegisterQuantifier( Node q ) {
   if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
-    if( !options::cbqiAll() && !options::cbqiSplx() ){
+    if( d_do_cbqi[q]==2 ){
       //take full ownership of the quantified formula
       d_quantEngine->setOwner( q, this );
+      
+      //mark all nested quantifiers with id
+      if( options::cbqiNestedQE() ){
+        std::map< Node, Node > visited;
+        Node mq = getIdMarkedQuantNode( q[1], visited );
+        if( mq!=q[1] ){
+          //do not do cbqi
+          d_do_cbqi[q] = false;
+          //instead do reduction
+          std::vector< Node > qqc;
+          qqc.push_back( q[0] );
+          qqc.push_back( mq );
+          if( q.getNumChildren()==3 ){
+            qqc.push_back( q[2] );
+          }
+          Node qq = NodeManager::currentNM()->mkNode( FORALL, qqc );
+          Node mlem = NodeManager::currentNM()->mkNode( IMPLIES, q, qq );
+          Trace("cbqi-lemma") << "Mark quant id lemma : " << mlem << std::endl;
+          d_quantEngine->getOutputChannel().lemma( mlem );
+        }
+      }
     }
   }
 }
@@ -159,6 +375,98 @@ void InstStrategyCbqi::registerQuantifier( Node q ) {
 
 }
 
+Node InstStrategyCbqi::doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts ) {
+  // there is a nested quantified formula (forall y. nq[y,x]) such that 
+  //    q is (forall y. nq[y,t]) for ground terms t,
+  //    ceq is (forall y. nq[y,e]) for CE variables e.
+  // we call this function when we know (forall y. nq[y,e]) is equivalent to quantifier-free formula C[e].
+  // in this case, q is equivalent to the quantifier-free formula C[t].
+  if( d_nested_qe.find( ceq )==d_nested_qe.end() ){
+    d_nested_qe[ceq] = d_quantEngine->getInstantiatedConjunction( ceq );
+    Trace("cbqi-nqe") << "CE quantifier elimination : " << std::endl;
+    Trace("cbqi-nqe") << "  " << ceq << std::endl; 
+    Trace("cbqi-nqe") << "  " << d_nested_qe[ceq] << std::endl;
+    //should not contain quantifiers
+    Assert( !QuantifiersRewriter::containsQuantifiers( d_nested_qe[ceq] ) );
+  }
+  Assert( d_quantEngine->getTermDatabase()->d_inst_constants[q].size()==inst_terms.size() );
+  //replace inst constants with instantiation
+  Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermDatabase()->d_inst_constants[q].begin(),
+                                          d_quantEngine->getTermDatabase()->d_inst_constants[q].end(),
+                                          inst_terms.begin(), inst_terms.end() );
+  if( doVts ){
+    //do virtual term substitution
+    ret = Rewriter::rewrite( ret );
+    ret = d_quantEngine->getTermDatabase()->rewriteVtsSymbols( ret );
+  }
+  Trace("cbqi-nqe") << "Nested quantifier elimination: " << std::endl;
+  Trace("cbqi-nqe") << "  " << n << std::endl; 
+  Trace("cbqi-nqe") << "  " << ret << std::endl;
+  return ret;
+}
+
+Node InstStrategyCbqi::doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts ) {
+  if( visited.find( n )==visited.end() ){
+    Node ret = n;
+    if( n.getKind()==FORALL ){
+      QAttributes qa;
+      TermDb::computeQuantAttributes( n, qa );
+      if( !qa.d_qid_num.isNull() ){
+        //if it has an id, check whether we have done quantifier elimination for this id
+        std::map< Node, Node >::iterator it = d_id_to_ce_quant.find( qa.d_qid_num );
+        if( it!=d_id_to_ce_quant.end() ){
+          Node ceq = it->second;
+          bool doNestedQe = d_elim_quants.contains( ceq );
+          if( doNestedQe ){
+            ret = doNestedQENode( q, ceq, n, inst_terms, doVts );
+          }else{
+            Trace("cbqi-nqe") << "Add to nested qe waitlist : " << std::endl;
+            Node nr = Rewriter::rewrite( n );
+            Trace("cbqi-nqe") << "  " << ceq << std::endl;
+            Trace("cbqi-nqe") << "  " << nr << std::endl;
+            int wlsize = d_nested_qe_waitlist_size[ceq] + 1;
+            d_nested_qe_waitlist_size[ceq] = wlsize;
+            if( wlsize<(int)d_nested_qe_waitlist[ceq].size() ){
+              d_nested_qe_waitlist[ceq][wlsize] = nr;
+            }else{
+              d_nested_qe_waitlist[ceq].push_back( nr );
+            }
+            d_nested_qe_info[nr].d_q = q;
+            d_nested_qe_info[nr].d_inst_terms.clear();
+            d_nested_qe_info[nr].d_inst_terms.insert( d_nested_qe_info[nr].d_inst_terms.end(), inst_terms.begin(), inst_terms.end() );
+            d_nested_qe_info[nr].d_doVts = doVts;
+            //TODO: ensure this holds by restricting prenex when cbqiNestedQe is true.
+            Assert( !options::cbqiInnermost() );
+          }
+        } 
+      } 
+    }else if( n.getNumChildren()>0 ){
+      std::vector< Node > children;
+      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+        children.push_back( n.getOperator() );
+      }
+      bool childChanged = false;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        Node nc = doNestedQERec( q, n[i], visited, inst_terms, doVts );
+        childChanged = childChanged || nc!=n[i];
+        children.push_back( nc );
+      }
+      if( childChanged ){
+        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+      }
+    }
+    visited[n] = ret;
+    return ret;
+  }else{
+    return n;
+  }  
+}
+
+Node InstStrategyCbqi::doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts ) {
+  std::map< Node, Node > visited;
+  return doNestedQERec( q, lem, visited, inst_terms, doVts );
+}
+
 void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){
   Trace("cbqi-debug") << "Counterexample lemma  : " << lem << std::endl;
   d_quantEngine->addLemma( lem, false );
@@ -187,57 +495,91 @@ bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visit
   }
   return false;
 }
-bool InstStrategyCbqi::hasNonCbqiVariable( Node q ){
+int InstStrategyCbqi::hasNonCbqiVariable( Node q ){
+  int hmin = 1;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     TypeNode tn = q[0][i].getType();
-    if( !tn.isInteger() && !tn.isReal() && !tn.isBoolean() && !tn.isBitVector() ){
-      if( options::cbqiSplx() ){
-        return true;
-      }else{
-        //datatypes supported in new implementation
-        if( !tn.isDatatype() ){
-          return true;
-        }
+    int handled = -1;
+    if( tn.isInteger() || tn.isReal() || tn.isBoolean() || tn.isBitVector() ){
+      handled = 0;
+    }else if( tn.isDatatype() ){
+      handled = 0;
+    }else if( tn.isSort() ){
+      QuantEPR * qepr = d_quantEngine->getQuantEPR();
+      if( qepr!=NULL ){
+        handled = qepr->isEPR( tn ) ? 1 : -1;
       }
     }
+    if( handled==-1 ){
+      return -1;
+    }else if( handled<hmin ){
+      hmin = handled;
+    }
   }
-  return false;
+  return hmin;
 }
 
 bool InstStrategyCbqi::doCbqi( Node q ){
-  std::map< Node, bool >::iterator it = d_do_cbqi.find( q );
+  std::map< Node, int >::iterator it = d_do_cbqi.find( q );
   if( it==d_do_cbqi.end() ){
-    bool ret = false;
-    if( d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){
-      ret = true;
-    }else{
+    int ret = 2;
+    if( !d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){
       //if has an instantiation pattern, don't do it
       if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
-        ret = false;
-      }else{
-        if( options::cbqiAll() ){
-          ret = true;
-        }else{
-          //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 );
+        for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
+          if( q[2][i].getKind()==INST_PATTERN ){
+            ret = 0;
+          }
+        }
+      }
+      if( ret!=0 ){
+        //if quantifier has a non-handled variable, then do not use cbqi
+        //if quantifier has an APPLY_UF term, then do not use cbqi unless EPR
+        int ncbqiv = hasNonCbqiVariable( q );
+        if( ncbqiv==0 || ncbqiv==1 ){
           std::map< Node, bool > visited;
-          ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( q[1], visited );
+          if( hasNonCbqiOperator( q[1], visited ) ){
+            if( ncbqiv==1 ){
+              //all variables are fully handled, this implies this will be handlable regardless of body (e.g. for EPR)
+              //  so, try but not exclusively
+              ret = 1;
+            }else{
+              //cannot be handled
+              ret = 0;
+            }
+          }
+        }else{
+          // unhandled variable type
+          ret = 0;
+        }
+        if( ret==0 && options::cbqiAll() ){
+          //try but not exclusively
+          ret = 1;
         }
       }
     }
-    Trace("cbqi") << "doCbqi " << q << " returned " << ret << std::endl;
+    Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
     d_do_cbqi[q] = ret;
-    return ret;
+    return ret!=0;
   }else{
-    return it->second;
+    return it->second!=0;
   }
 }
 
-Node InstStrategyCbqi::getNextDecisionRequest(){
-  // all counterexample literals that are not asserted
-  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-    Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc ) {
+  if( proc.find( q )==proc.end() ){
+    proc[q] = true;
+    //first check children
+    std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( q );
+    if( itc!=d_children_quant.end() ){
+      for( unsigned j=0; j<itc->second.size(); j++ ){
+        Node d = getNextDecisionRequestProc( itc->second[j], proc );
+        if( !d.isNull() ){
+          return d;
+        }
+      }
+    }
+    //then check self
     if( hasAddedCbqiLemma( q ) ){
       Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
       bool value;
@@ -245,328 +587,21 @@ Node InstStrategyCbqi::getNextDecisionRequest(){
         Trace("cbqi-dec") << "CBQI: get next decision " << cel << std::endl;
         return cel;
       }
-    }
+    }    
   }
-  return Node::null();
+  return Node::null(); 
 }
 
-
-
-
-//old implementation
-
-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) );
-}
-
-void getInstantiationConstants( Node n, std::vector< Node >& ics ){
-  if( n.getKind()==INST_CONSTANT ){
-    if( std::find( ics.begin(), ics.end(), n )==ics.end() ){
-      ics.push_back( n );
-    }
-  }else{
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      getInstantiationConstants( n[i], ics );
-    }
-  }
-}
-
-
-void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){
-  Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;
-  d_quantActive.clear();
-  d_instRows.clear();
-  d_tableaux_term.clear();
-  d_tableaux.clear();
-  d_ceTableaux.clear();
-  //search for instantiation rows in simplex tableaux
-  ArithVariables& avnm = d_th->d_internal->d_partialModel;
-  ArithVariables::var_iterator vi, vend;
-  for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){
-    ArithVar x = *vi;
-    Node n = avnm.asNode(x);
-
-    //collect instantiation constants
-    std::vector< Node > ics;
-    getInstantiationConstants( n, ics );
-    for( unsigned i=0; i<ics.size(); i++ ){
-      NodeBuilder<> t(kind::PLUS);
-      if( n.getKind()==PLUS ){
-        for( int j=0; j<(int)n.getNumChildren(); j++ ){
-          addTermToRow( ics[i], x, n[j], t );
-        }
-      }else{
-        addTermToRow( ics[i], x, n, t );
-      }
-      d_instRows[ics[i]].push_back( x );
-      //this theory has constraints from f
-      Node f = TermDb::getInstConstAttr(ics[i]);
-      Debug("quant-arith") << "Has constraints from " << f << std::endl;
-      //set that we should process it
-      d_quantActive[ f ] = true;
-      //set tableaux term
-      if( t.getNumChildren()==0 ){
-        d_tableaux_term[ics[i]][x] = d_zero;
-      }else if( t.getNumChildren()==1 ){
-        d_tableaux_term[ics[i]][x] = t.getChild( 0 );
-      }else{
-        d_tableaux_term[ics[i]][x] = t;
-      }
-    }
-  }
-  //print debug
-  if( Debug.isOn("quant-arith-debug") ){
-    Debug("quant-arith-debug") << std::endl;
-    debugPrint( "quant-arith-debug" );
-  }
-  d_counter++;
-}
-
-void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder<>& t ){
-  if( n.getKind()==MULT ){
-    if( TermDb::hasInstConstAttr(n[1]) && n[0].getKind()==CONST_RATIONAL ){
-      if( n[1]==i ){
-        d_ceTableaux[i][x][ n[1] ] = n[0];
-      }else{
-        d_tableaux_ce_term[i][x][ n[1] ] = n[0];
-      }
-    }else{
-      d_tableaux[i][x][ n[1] ] = n[0];
-      t << n;
-    }
-  }else{
-    if( TermDb::hasInstConstAttr(n) ){
-      if( n==i ){
-        d_ceTableaux[i][x][ n ] = Node::null();
-      }else{
-        d_tableaux_ce_term[i][x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
-      }
-    }else{
-      d_tableaux[i][x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
-      t << n;
-    }
-  }
-}
-
-void InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
-  if( e==0 ){
-    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( unsigned 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( unsigned j=0; j<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 );
-              }
-            }
-            //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.
-            }
-            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;
-            }
-          }
-        }
-      }
-      if( lem==0 && m_point_valid ){
-        if( d_quantEngine->addInstantiation( f, m_point ) ){
-          Debug("quant-arith-simplex") << "...added point instantiation." << std::endl;
-        }
-      }
-    }
-  }
-}
-
-
-void InstStrategySimplex::debugPrint( const char* c ){
-  ArithVariables& avnm = d_th->d_internal->d_partialModel;
-  ArithVariables::var_iterator vi, vend;
-  for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){
-    ArithVar x = *vi;
-    Node n = avnm.asNode(x);
-    //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){
-      Debug(c) << x << " : " << n << ", bounds = ";
-      if( d_th->d_internal->d_partialModel.hasLowerBound( x ) ){
-        Debug(c) << d_th->d_internal->d_partialModel.getLowerBound( x );
-      }else{
-        Debug(c) << "-infty";
-      }
-      Debug(c) << " <= ";
-      Debug(c) << d_th->d_internal->d_partialModel.getAssignment( x );
-      Debug(c) << " <= ";
-      if( d_th->d_internal->d_partialModel.hasUpperBound( x ) ){
-        Debug(c) << d_th->d_internal->d_partialModel.getUpperBound( x );
-      }else{
-        Debug(c) << "+infty";
-      }
-      Debug(c) << std::endl;
-      //Debug(c) << "   Term = " << d_tableaux_term[x] << std::endl;
-      //Debug(c) << "   ";
-      //for( std::map< Node, Node >::iterator it2 = d_tableaux[x].begin(); it2 != d_tableaux[x].end(); ++it2 ){
-      //  Debug(c) << "( " << it2->first << ", " << it2->second << " ) ";
-      //}
-      //for( std::map< Node, Node >::iterator it2 = d_ceTableaux[x].begin(); it2 != d_ceTableaux[x].end(); ++it2 ){
-      //  Debug(c) << "(CE)( " << it2->first << ", " << it2->second << " ) ";
-      //}
-      //for( std::map< Node, Node >::iterator it2 = d_tableaux_ce_term[x].begin(); it2 != d_tableaux_ce_term[x].end(); ++it2 ){
-      //  Debug(c) << "(CE-term)( " << it2->first << ", " << it2->second << " ) ";
-      //}
-      //Debug(c) << std::endl;
-    //}
-  }
-  Debug(c) << std::endl;
-
+Node InstStrategyCbqi::getNextDecisionRequest(){
+  std::map< Node, bool > proc;
   for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-    Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
-    Debug(c) << f << std::endl;
-    Debug(c) << "   Inst constants: ";
-    for( unsigned j=0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
-      if( j>0 ){
-        Debug( c ) << ", ";
-      }
-      Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
-    }
-    Debug(c) << std::endl;
-    for( unsigned j=0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
-      Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
-      Debug(c) << "   Instantiation rows for " << ic << " : ";
-      for( unsigned k=0; k<d_instRows[ic].size(); k++ ){
-        if( k>0 ){
-          Debug(c) << ", ";
-        }
-        Debug(c) << d_instRows[ic][k];
-      }
-      Debug(c) << std::endl;
-    }
-  }
-}
-
-//say instantiation row x for quantifier f is coeff*var + A*t[e] + term = beta,
-// where var is an instantiation constant from f,
-// t[e] is a vector of terms containing instantiation constants from f,
-// and term is a ground term (c1*t1 + ... + cn*tn).
-// We construct the term ( beta - term )/coeff to use as an instantiation for var.
-bool InstStrategySimplex::doInstantiation( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var ){
-  //first try +delta
-  if( doInstantiation2( f, ic, term, x, m, var ) ){
-    ++(d_quantEngine->d_statistics.d_instantiations_cbqi_arith);
-    return true;
-  }else{
-#ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA
-    //otherwise try -delta
-    if( doInstantiation2( f, ic, term, x, m, var, true ) ){
-      ++(d_quantEngine->d_statistics.d_instantiations_cbqi_arith);
-      return true;
-    }else{
-      return false;
-    }
-#else
-    return false;
-#endif
-  }
-}
-
-bool InstStrategySimplex::doInstantiation2( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){
-  // make term ( beta - term )/coeff
-  bool vIsInteger = var.getType().isInteger();
-  Node beta = getTableauxValue( x, minus_delta );
-  if( !vIsInteger || beta.getType().isInteger() ){
-    Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term );
-    if( !d_ceTableaux[ic][x][var].isNull() ){
-      if( vIsInteger ){
-        Assert( d_ceTableaux[ic][x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) );
-        instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[ic][x][var], instVal );
-      }else{
-        Assert( d_ceTableaux[ic][x][var].getKind()==CONST_RATIONAL );
-        Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[ic][x][var].getConst<Rational>() );
-        instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal );
-      }
+    Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+    Node d = getNextDecisionRequestProc( q, proc );
+    if( !d.isNull() ){
+      return d;
     }
-    instVal = Rewriter::rewrite( instVal );
-    //use as instantiation value for var
-    int vn = var.getAttribute(InstVarNumAttribute());
-    m.setValue( vn, instVal );
-    Debug("quant-arith") << "Add instantiation " << m << std::endl;
-    return d_quantEngine->addInstantiation( f, m );
-  }else{
-    return false;
-  }
-}
-/*
-Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){
-  if( d_th->d_internal->d_partialModel.hasArithVar(n) ){
-    ArithVar v = d_th->d_internal->d_partialModel.asArithVar( n );
-    return getTableauxValue( v, minus_delta );
-  }else{
-    return NodeManager::currentNM()->mkConst( Rational(0) );
   }
-}
-*/
-Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){
-  const Rational& delta = d_th->d_internal->d_partialModel.getDelta();
-  DeltaRational drv = d_th->d_internal->d_partialModel.getAssignment( v );
-  Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );
-  return mkRationalNode(qmodel);
+  return Node::null();
 }
 
 
@@ -590,6 +625,7 @@ InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe )
   : InstStrategyCbqi( qe ) {
   d_out = new CegqiOutputInstStrategy( this );
   d_small_const = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) );
+  d_check_vts_lemma_lc = false;
 }
 
 InstStrategyCegqi::~InstStrategyCegqi() throw () {
@@ -654,9 +690,13 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
     //check if we need virtual term substitution (if used delta or infinity)
     bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false );
     if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, used_vts ) ){
+      ++(d_quantEngine->d_statistics.d_instantiations_cbqi);
       //d_added_inst.insert( d_curr_quant );
       return true;
     }else{
+      //this should never happen for monotonic selection strategies
+      Trace("cbqi-warn") << "WARNING: Existing instantiation" << std::endl;
+      Assert( !options::cbqiNestedQE() || options::cbqiAll() );
       return false;
     }
   }
@@ -671,6 +711,16 @@ bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
     if( n.getKind()==SKOLEM && d_quantEngine->getTermDatabase()->containsVtsTerm( n ) ){
       return true;
     }else{
+      TypeNode tn = n.getType();
+      if( tn.isSort() ){
+        QuantEPR * qepr = d_quantEngine->getQuantEPR();
+        if( qepr!=NULL ){
+          //legal if in the finite set of constants of type tn
+          if( qepr->isEPRConstant( tn, n ) ){
+            return true;
+          }
+        }
+      }
       //only legal if current quantified formula contains n
       return TermDb::containsTerm( d_curr_quant, n );
     }
@@ -719,7 +769,9 @@ void InstStrategyCegqi::registerCounterexampleLemma( Node q, Node lem ) {
 void InstStrategyCegqi::presolve() {
   if( options::cbqiPreRegInst() ){
     for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){
+      Trace("cbqi-presolve") << "Presolve " << it->first << std::endl;
       it->second->presolve( it->first );
     }
   }
 }
+
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 8ed59778b..c9f62243f 100755
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -34,25 +34,64 @@ namespace quantifiers {
 
 class InstStrategyCbqi : public QuantifiersModule {
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+  typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
 protected:
   bool d_cbqi_set_quant_inactive;
   bool d_incomplete_check;
   /** whether we have added cbqi lemma */
   NodeSet d_added_cbqi_lemma;
+  /** whether we have added cbqi lemma */
+  NodeSet d_elim_quants;
+  /** parent guards */
+  std::map< Node, std::vector< Node > > d_parent_quant;
+  std::map< Node, std::vector< Node > > d_children_quant;
+  std::map< Node, bool > d_active_quant;
   /** whether we have instantiated quantified formulas */
   //NodeSet d_added_inst;
-  /** whether to do cbqi for this quantified formula */
-  std::map< Node, bool > d_do_cbqi;
+  /** whether to do cbqi for this quantified formula 0 : no, 2 : yes, 1 : yes but not exclusively, -1 : heuristically */
+  std::map< Node, int > d_do_cbqi;
   /** register ce lemma */
+  bool registerCbqiLemma( Node q );
   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 );
+  int hasNonCbqiVariable( Node q );
   bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited );
+  /** get next decision request with dependency checking */
+  Node getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc );  
   /** process functions */
   virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
   virtual void process( Node q, Theory::Effort effort, int e ) = 0;
+protected:
+  //for identification
+  uint64_t d_qid_count;
+  //nested qe map
+  std::map< Node, Node > d_nested_qe;
+  //mark ids on quantifiers 
+  Node getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited );
+  // id to ce quant
+  std::map< Node, Node > d_id_to_ce_quant;
+  std::map< Node, Node > d_ce_quant_to_id;
+  //do nested quantifier elimination recursive
+  Node doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts );
+  Node doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts );
+  //elimination information (for delayed elimination)
+  class NestedQEInfo {
+  public:
+    NestedQEInfo() : d_doVts(false){}
+    ~NestedQEInfo(){}
+    Node d_q;
+    std::vector< Node > d_inst_terms;
+    bool d_doVts;
+  };
+  std::map< Node, NestedQEInfo > d_nested_qe_info;
+  NodeIntMap d_nested_qe_waitlist_size;
+  NodeIntMap d_nested_qe_waitlist_proc;
+  std::map< Node, std::vector< Node > > d_nested_qe_waitlist;
+public:
+  //do nested quantifier elimination
+  Node doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts );
 public:
   InstStrategyCbqi( QuantifiersEngine * qe );
   ~InstStrategyCbqi() throw();
@@ -64,56 +103,13 @@ public:
   void reset_round( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
   bool checkComplete();
+  bool checkCompleteFor( Node q );
   void preRegisterQuantifier( Node q );
   void registerQuantifier( Node q );
   /** get next decision request */
   Node getNextDecisionRequest();
 };
 
-
-class InstStrategySimplex : public InstStrategyCbqi {
-protected:
-  /** reference to theory arithmetic */
-  arith::TheoryArith* d_th;
-  /** quantifiers we should process */
-  std::map< Node, bool > d_quantActive;
-  /** delta */
-  std::map< TypeNode, Node > d_deltas;
-  /** for each quantifier, simplex rows */
-  std::map< Node, std::vector< arith::ArithVar > > d_instRows;
-  /** tableaux */
-  std::map< Node, std::map< arith::ArithVar, Node > > d_tableaux_term;
-  std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_tableaux_ce_term;
-  std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_tableaux;
-  /** ce tableaux */
-  std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_ceTableaux;
-  /** get value */
-  //Node getTableauxValue( Node n, bool minus_delta = false );
-  Node getTableauxValue( arith::ArithVar v, bool minus_delta = false );
-  /** do instantiation */
-  bool doInstantiation( Node f, Node ic, Node term, arith::ArithVar x, InstMatch& m, Node var );
-  bool doInstantiation2( Node f, Node ic, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false );
-  /** add term to row */
-  void addTermToRow( Node ic, arith::ArithVar x, Node n, NodeBuilder<>& t );
-  /** print debug */
-  void debugPrint( const char* c );
-private:
-  /** */
-  int d_counter;
-  /** constants */
-  Node d_zero;
-  Node d_negOne;
-  /** process functions */
-  void processResetInstantiationRound( Theory::Effort effort );
-  void process( Node f, Theory::Effort effort, int e );
-public:
-  InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie );
-  ~InstStrategySimplex() throw() {}
-  /** identify */
-  std::string identify() const { return std::string("Simplex"); }
-};
-
-
 //generalized counterexample guided quantifier instantiation
 
 class InstStrategyCegqi;
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 49e0a698f..c4bf61b28 100755
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -155,6 +155,7 @@ InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe
     d_regenerate_frequency = 3;
     d_regenerate = true;
   }else{
+    d_regenerate_frequency = 1;
     d_regenerate = false;
   }
 }
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index db597d031..afeed1e5d 100755
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -114,6 +114,7 @@ void InstantiationEngine::reset_round( Theory::Effort e ){
 }
 
 void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
+  CodeTimer codeTimer(d_quantEngine->d_statistics.d_ematching_time);
   if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
     double clSet = 0;
     if( Trace.isOn("inst-engine") ){
@@ -151,19 +152,9 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
   }
 }
 
-bool InstantiationEngine::checkComplete() {
-  if( !options::finiteModelFind() ){
-    for( unsigned i=0; i<d_quants.size(); i++ ){
-      if( isIncomplete( d_quants[i] ) ){
-        return false;
-      }
-    }
-  }
-  return true;
-}
-
-bool InstantiationEngine::isIncomplete( Node q ) {
-  return true;
+bool InstantiationEngine::checkCompleteFor( Node q ) {
+  //TODO?
+  return false;
 }
 
 void InstantiationEngine::preRegisterQuantifier( Node q ) {
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index d2b3740a1..79963cb45 100755
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -78,7 +78,7 @@ public:
   bool needsCheck( Theory::Effort e );
   void reset_round( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
-  bool checkComplete();
+  bool checkCompleteFor( Node q );
   void preRegisterQuantifier( Node q );
   void registerQuantifier( Node q );
   Node explain(TNode n){ return Node::null(); }
diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h
index 94abf3c90..04a6bc9c8 100755
--- a/src/theory/quantifiers/local_theory_ext.h
+++ b/src/theory/quantifiers/local_theory_ext.h
@@ -66,6 +66,8 @@ public:
   void check( Theory::Effort e, unsigned quant_e );
   /* Called for new quantifiers */
   void registerQuantifier( Node q ) {}
+  /* check complete */
+  bool checkComplete() { return !d_wasInvoked; }
   void assertNode( Node n ) {}
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   std::string identify() const { return "LtePartialInst"; }
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 582599680..976b81e60 100755
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -33,6 +33,10 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::kind;
 
 
+QuantifierMacros::QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){
+  d_ground_macros = false;
+}
+  
 bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){
   unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_ALL ? 2 : 1;
   for( unsigned r=0; r<rmax; r++ ){
diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h
index 39ec2f0a1..60af7ad0a 100755
--- a/src/theory/quantifiers/macros.h
+++ b/src/theory/quantifiers/macros.h
@@ -60,7 +60,7 @@ private:
   void addMacro( Node op, Node n, std::vector< Node >& opc );
   void debugMacroDefinition( Node oo, Node n );
 public:
-  QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){}
+  QuantifierMacros( QuantifiersEngine * qe );
   ~QuantifierMacros(){}
 
   bool simplify( std::vector< Node >& assertions, bool doRewrite = false );
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 7bbe06108..b30c2addb 100755
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -391,7 +391,7 @@ bool QModelBuilderIG::isTermActive( Node n ){
 
 
 //do exhaustive instantiation
-bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
+int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
   if( optUseModel() ){
     RepSetIterator riter( d_qe, &(d_qe->getModel()->d_rep_set) );
     if( riter.setQuantifier( f ) ){
@@ -470,10 +470,9 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
       }
     }
     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
-    d_incomplete_check = riter.isIncomplete();
-    return true;
+    return riter.isIncomplete() ? -1 : 1;
   }else{
-    return false;
+    return 0;
   }
 }
 
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index e4f9529a8..9b89e5ef6 100755
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -38,13 +38,14 @@ public:
   virtual ~QModelBuilder() throw() {}
   // is quantifier active?
   virtual bool isQuantifierActive( Node f );
-  //do exhaustive instantiation
-  virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; }
+  //do exhaustive instantiation  
+  // 0 :  failed, but resorting to true exhaustive instantiation may work
+  // >0 : success
+  // <0 : failed
+  virtual int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; }
   //whether to construct model
   virtual bool optUseModel();
   /** number of lemmas generated while building model */
-  //is the exhaustive instantiation incomplete?
-  bool d_incomplete_check;
   int d_addedLemmas;
   int d_triedLemmas;
   /** exist instantiation ? */
@@ -142,7 +143,7 @@ public:
   // is quantifier active?
   bool isQuantifierActive( Node f );
   //do exhaustive instantiation
-  bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
+  int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
 
   //temporary stats
   int d_numQuantSat;
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 7658f2b6b..9c09371c4 100755
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -73,7 +73,6 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
       Trace("model-engine") << "---Model Engine Round---" << std::endl;
       clSet = double(clock())/double(CLOCKS_PER_SEC);
     }
-    ++(d_statistics.d_inst_rounds);
 
     Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
     //let the strong solver verify that the model is minimal
@@ -99,7 +98,7 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
     }
 
     if( addedLemmas==0 ){
-      Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl;
+      Trace("model-engine-debug") << "No lemmas added, incomplete = " << ( d_incomplete_check || !d_incomplete_quants.empty() ) << std::endl;
       //CVC4 will answer SAT or unknown
       if( Trace.isOn("fmf-consistent") ){
         Trace("fmf-consistent") << std::endl;
@@ -113,6 +112,10 @@ bool ModelEngine::checkComplete() {
   return !d_incomplete_check;
 }
 
+bool ModelEngine::checkCompleteFor( Node q ) {
+  return std::find( d_incomplete_quants.begin(), d_incomplete_quants.end(), q )==d_incomplete_quants.end();
+}
+
 void ModelEngine::registerQuantifier( Node f ){
   if( Trace.isOn("fmf-warn") ){
     bool canHandle = true;
@@ -195,17 +198,18 @@ int ModelEngine::checkModel(){
   // FMC uses two sub-effort levels
   int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 );
   for( int e=0; e<e_max; e++) {
+    d_incomplete_quants.clear();
     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-      Node f = fm->getAssertedQuantifier( i, true );
-      Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl;
+      Node q = fm->getAssertedQuantifier( i, true );
+      Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl;
       //determine if we should check this quantifier
-      if( considerQuantifiedFormula( f ) ){
-        exhaustiveInstantiate( f, e );
+      if( considerQuantifiedFormula( q ) ){
+        exhaustiveInstantiate( q, e );
         if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){
           break;
         }
       }else{
-        Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl;
+        Trace("fmf-exh-inst") << "-> Inactive : " << q << std::endl;
       }
     }
     if( d_addedLemmas>0 ){
@@ -260,13 +264,17 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
   quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder();
   mb->d_triedLemmas = 0;
   mb->d_addedLemmas = 0;
-  mb->d_incomplete_check = false;
-  if( mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){
-    Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl;
+  int retEi = mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort );
+  if( retEi!=0 ){
+    if( retEi<0 ){
+      Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl;
+      d_incomplete_quants.push_back( f );
+    }else{
+      Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl;
+    }
     d_triedLemmas += mb->d_triedLemmas;
     d_addedLemmas += mb->d_addedLemmas;
-    d_incomplete_check = d_incomplete_check || mb->d_incomplete_check;
-    d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas;
+    d_quantEngine->d_statistics.d_instantiations_fmf_mbqi += mb->d_addedLemmas;
   }else{
     if( Trace.isOn("fmf-exh-inst-debug") ){
       Trace("fmf-exh-inst-debug") << "   Instantiation Constants: ";
@@ -303,13 +311,15 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
         }
         d_addedLemmas += addedLemmas;
         d_triedLemmas += triedLemmas;
-        d_statistics.d_exh_inst_lemmas += addedLemmas;
+        d_quantEngine->d_statistics.d_instantiations_fmf_exh += addedLemmas;
       }
     }else{
       Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
     }
     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
-    d_incomplete_check = d_incomplete_check || riter.isIncomplete();
+    if( riter.isIncomplete() ){
+      d_incomplete_quants.push_back( f );
+    }
   }
 }
 
@@ -328,18 +338,3 @@ void ModelEngine::debugPrint( const char* c ){
   //d_quantEngine->getModel()->debugPrint( c );
 }
 
-ModelEngine::Statistics::Statistics():
-  d_inst_rounds("ModelEngine::Inst_Rounds", 0),
-  d_exh_inst_lemmas("ModelEngine::Instantiations_Exhaustive", 0 ),
-  d_mbqi_inst_lemmas("ModelEngine::Instantiations_Mbqi", 0 )
-{
-  smtStatisticsRegistry()->registerStat(&d_inst_rounds);
-  smtStatisticsRegistry()->registerStat(&d_exh_inst_lemmas);
-  smtStatisticsRegistry()->registerStat(&d_mbqi_inst_lemmas);
-}
-
-ModelEngine::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_inst_rounds);
-  smtStatisticsRegistry()->unregisterStat(&d_exh_inst_lemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_mbqi_inst_lemmas);
-}
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index 12f18aa08..e89be8d2b 100755
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -42,6 +42,8 @@ private:
   //temporary statistics
   //is the exhaustive instantiation incomplete?
   bool d_incomplete_check;
+  // set of quantified formulas for which check was incomplete
+  std::vector< Node > d_incomplete_quants;
   int d_addedLemmas;
   int d_triedLemmas;
   int d_totalLemmas;
@@ -54,21 +56,11 @@ public:
   void reset_round( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
   bool checkComplete();
+  bool checkCompleteFor( Node q );
   void registerQuantifier( Node f );
   void assertNode( Node f );
   Node explain(TNode n){ return Node::null(); }
   void debugPrint( const char* c );
-public:
-  /** statistics class */
-  class Statistics {
-  public:
-    IntStat d_inst_rounds;
-    IntStat d_exh_inst_lemmas;
-    IntStat d_mbqi_inst_lemmas;
-    Statistics();
-    ~Statistics();
-  };
-  Statistics d_statistics;
   /** Identify this module */
   std::string identify() const { return "ModelEngine"; }
 };/* class ModelEngine */
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index bac2aa35c..1e484311c 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -108,7 +108,7 @@ void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) {
   }
   Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;
   
-  if( d_mg->isValid() ){
+  if( d_mg->isValid() && options::qcfEagerCheckRd() ){
     //optimization : record variable argument positions for terms that must be matched
     std::vector< TNode > vars;
     //TODO: revisit this, makes QCF faster, but misses conflicts due to caring about paths that may not be relevant (starExec jobs 14136/14137)
@@ -967,7 +967,11 @@ MatchGen::MatchGen()
     d_n(),
     d_type( typ_invalid ),
     d_type_not()
-{}
+{
+  d_qni_size = 0;
+  d_child_counter = -1;
+  d_use_children = true;
+}
 
 
 MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
@@ -980,6 +984,10 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
     d_type(),
     d_type_not()
 {
+  //initialize temporary
+  d_child_counter = -1;
+  d_use_children = true;
+  
   Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;
   std::vector< Node > qni_apps;
   d_qni_size = 0;
@@ -1853,7 +1861,7 @@ void MatchGen::setInvalid() {
 }
 
 bool MatchGen::isHandledBoolConnective( TNode n ) {
-  return TermDb::isBoolConnective( n.getKind() ) && ( n.getKind()!=ITE || n.getType().isBoolean() );
+  return TermDb::isBoolConnective( n.getKind() ) && ( n.getKind()!=ITE || n.getType().isBoolean() ) && n.getKind()!=SEP_STAR;
 }
 
 bool MatchGen::isHandledUfTerm( TNode n ) {
@@ -2024,6 +2032,7 @@ void QuantConflictFind::setIrrelevantFunction( TNode f ) {
 
 /** check */
 void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
+  CodeTimer codeTimer(d_quantEngine->d_statistics.d_qcf_time);
   if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){
     Trace("qcf-check") << "QCF : check : " << level << std::endl;
     if( d_conflict ){
@@ -2098,7 +2107,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                           ++addedLemmas;
                           if( e==effort_conflict ){
                             d_quantEngine->markRelevant( q );
-                            ++(d_statistics.d_conflict_inst);
+                            ++(d_quantEngine->d_statistics.d_instantiations_qcf);
                             if( options::qcfAllConflict() ){
                               isConflict = true;
                             }else{
@@ -2107,7 +2116,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                             break;
                           }else if( e==effort_prop_eq ){
                             d_quantEngine->markRelevant( q );
-                            ++(d_statistics.d_prop_inst);
+                            ++(d_quantEngine->d_statistics.d_instantiations_qcf);
                           }
                         }else{
                           Trace("qcf-inst") << "   ... Failed to add instantiation" << std::endl;
@@ -2234,20 +2243,14 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo
 
 QuantConflictFind::Statistics::Statistics():
   d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),
-  d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ),
-  d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ),
   d_entailment_checks("QuantConflictFind::Entailment_Checks",0)
 {
   smtStatisticsRegistry()->registerStat(&d_inst_rounds);
-  smtStatisticsRegistry()->registerStat(&d_conflict_inst);
-  smtStatisticsRegistry()->registerStat(&d_prop_inst);
   smtStatisticsRegistry()->registerStat(&d_entailment_checks);
 }
 
 QuantConflictFind::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_inst_rounds);
-  smtStatisticsRegistry()->unregisterStat(&d_conflict_inst);
-  smtStatisticsRegistry()->unregisterStat(&d_prop_inst);
   smtStatisticsRegistry()->unregisterStat(&d_entailment_checks);
 }
 
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 47a66b1b1..dc8a9acb2 100755
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -260,8 +260,6 @@ public:
   class Statistics {
   public:
     IntStat d_inst_rounds;
-    IntStat d_conflict_inst;
-    IntStat d_prop_inst;
     IntStat d_entailment_checks;
     Statistics();
     ~Statistics();
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 5aff1a848..df8533135 100755
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -48,7 +48,7 @@ void QuantDSplit::preRegisterQuantifier( Node q ) {
       }else{
         int score = -1;
         if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
-          score = dt.isInterpretedFinite() ? 1 : -1;
+          score = dt.isInterpretedFinite() ? 1 : 0;
         }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){
           score = dt.isInterpretedFinite() ? 1 : -1;
         }
@@ -73,6 +73,11 @@ bool QuantDSplit::needsCheck( Theory::Effort e ) {
   return e>=Theory::EFFORT_FULL && !d_quant_to_reduce.empty();
 }
 
+bool QuantDSplit::checkCompleteFor( Node q ) {
+  // true if we split q
+  return d_added_split.find( q )!=d_added_split.end();
+}
+
 /* Call during quantifier engine's check */
 void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) {
   //add lemmas ASAP (they are a reduction)
diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index d36824998..3e3b08814 100755
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h
@@ -43,6 +43,7 @@ public:
   /* Called for new quantifiers */
   void registerQuantifier( Node q ) {}
   void assertNode( Node n ) {}
+  bool checkCompleteFor( Node q );
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   std::string identify() const { return "QuantDSplit"; }
 };
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index b9aab0236..f4284a8ab 100755
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -419,3 +419,107 @@ void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol,
   }
 }
 
+void QuantEPR::registerNode( Node n, std::map< int, std::map< Node, bool > >& visited, bool beneathQuant, bool hasPol, bool pol ) {
+  int vindex = hasPol ? ( pol ? 1 : -1 ) : 0;
+  if( visited[vindex].find( n )==visited[vindex].end() ){
+    visited[vindex][n] = true;
+    Trace("quant-epr-debug") << "QuantEPR::registerNode " << n << std::endl;
+    if( n.getKind()==FORALL ){
+      if( beneathQuant || !hasPol || !pol ){
+        for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
+          TypeNode tn = n[0][i].getType();
+          if( d_non_epr.find( tn )==d_non_epr.end() ){
+            Trace("quant-epr") << "Sort " << tn << " is non-EPR because of nested or possible existential quantification." << std::endl;
+            d_non_epr[tn] = true;
+          }
+        }
+      }else{
+        beneathQuant = true;
+      }
+    }
+    TypeNode tn = n.getType();
+    
+    if( n.getNumChildren()>0 ){
+      if( tn.isSort() ){
+        if( d_non_epr.find( tn )==d_non_epr.end() ){
+          Trace("quant-epr") << "Sort " << tn << " is non-EPR because of " << n << std::endl;
+          d_non_epr[tn] = true;
+        }
+      }
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        bool newHasPol;
+        bool newPol;
+        QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
+        registerNode( n[i], visited, beneathQuant, newHasPol, newPol );
+      }
+    }else if( tn.isSort() ){
+      if( n.getKind()==BOUND_VARIABLE ){
+        if( d_consts.find( tn )==d_consts.end() ){
+          //mark that at least one constant must occur
+          d_consts[tn].clear();
+        }
+      }else if( std::find( d_consts[tn].begin(), d_consts[tn].end(), n )==d_consts[tn].end() ){
+        d_consts[tn].push_back( n );
+        Trace("quant-epr") << "...constant of type " << tn << " : " << n << std::endl;
+      }
+    }
+  }
+}
+
+void QuantEPR::registerAssertion( Node assertion ) {
+  std::map< int, std::map< Node, bool > > visited;
+  registerNode( assertion, visited, false, true, true );
+}
+
+void QuantEPR::finishInit() {
+  Trace("quant-epr-debug") << "QuantEPR::finishInit" << std::endl;
+  for( std::map< TypeNode, std::vector< Node > >::iterator it = d_consts.begin(); it != d_consts.end(); ++it ){
+    Assert( d_epr_axiom.find( it->first )==d_epr_axiom.end() );
+    Trace("quant-epr-debug") << "process " << it->first << std::endl;
+    if( d_non_epr.find( it->first )!=d_non_epr.end() ){
+      Trace("quant-epr-debug") << "...non-epr" << std::endl;
+      it->second.clear();
+    }else{
+      Trace("quant-epr-debug") << "...epr, #consts = " << it->second.size() << std::endl;
+      if( it->second.empty() ){
+        it->second.push_back( NodeManager::currentNM()->mkSkolem( "e", it->first, "EPR base constant" ) );
+      }
+      if( Trace.isOn("quant-epr") ){
+        Trace("quant-epr") << "Type " << it->first << " is EPR, with constants : " << std::endl;
+        for( unsigned i=0; i<it->second.size(); i++ ){
+          Trace("quant-epr") << "  " << it->second[i] << std::endl;
+        }
+      }
+    }
+  }
+}
+
+bool QuantEPR::isEPRConstant( TypeNode tn, Node k ) {
+  return std::find( d_consts[tn].begin(), d_consts[tn].end(), k )!=d_consts[tn].end();
+}
+
+void QuantEPR::addEPRConstant( TypeNode tn, Node k ) {
+  Assert( isEPR( tn ) );
+  Assert( d_epr_axiom.find( tn )==d_epr_axiom.end() );
+  if( !isEPRConstant( tn, k ) ){
+    d_consts[tn].push_back( k );
+  }
+}
+
+Node QuantEPR::mkEPRAxiom( TypeNode tn ) {
+  Assert( isEPR( tn ) );
+  std::map< TypeNode, Node >::iterator ita = d_epr_axiom.find( tn );
+  if( ita==d_epr_axiom.end() ){
+    std::vector< Node > disj;
+    Node x = NodeManager::currentNM()->mkBoundVar( tn );
+    for( unsigned i=0; i<d_consts[tn].size(); i++ ){
+      disj.push_back( NodeManager::currentNM()->mkNode( tn.isBoolean() ? IFF : EQUAL, x, d_consts[tn][i] ) );
+    }
+    Assert( !disj.empty() );
+    d_epr_axiom[tn] = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, x ), disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj ) );
+    return d_epr_axiom[tn];
+  }else{
+    return ita->second;
+  }
+}
+
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 79cdae437..3ff21aa6e 100755
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -51,8 +51,10 @@ public:
   virtual void reset_round( Theory::Effort e ){}
   /* Call during quantifier engine's check */
   virtual void check( Theory::Effort e, unsigned quant_e ) = 0;
-  /* check was complete (e.g. no lemmas implies a model) */
+  /* check was complete, return false if there is no way to answer "SAT", true if maybe can answer "SAT" */
   virtual bool checkComplete() { return true; }
+  /* check was complete for quantified formula q (e.g. no lemmas implies a model) */
+  virtual bool checkCompleteFor( Node q ) { return false; }
   /* Called for new quantified formulas */
   virtual void preRegisterQuantifier( Node q ) { }
   /* Called for new quantifiers after owners are finalized */
@@ -149,7 +151,7 @@ public:
 };
 
 
-class EqualityQuery : public QuantifiersUtil{
+class EqualityQuery : public QuantifiersUtil {
 public:
   EqualityQuery(){}
   virtual ~EqualityQuery(){};
@@ -171,6 +173,38 @@ public:
   virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0;
 };/* class EqualityQuery */
 
+class QuantEPR
+{
+private:
+  void registerNode( Node n, std::map< int, std::map< Node, bool > >& visited, bool beneathQuant, bool hasPol, bool pol );
+  /** non-epr */
+  std::map< TypeNode, bool > d_non_epr;
+  /** axioms for epr */
+  std::map< TypeNode, Node > d_epr_axiom;
+public:
+  QuantEPR(){}
+  virtual ~QuantEPR(){}
+  /** constants per type */
+  std::map< TypeNode, std::vector< Node > > d_consts;
+  /* reset */
+  //bool reset( Theory::Effort e ) {}
+  /** identify */
+  //std::string identify() const { return "QuantEPR"; }
+  /** register assertion */
+  void registerAssertion( Node assertion );
+  /** finish init */
+  void finishInit();
+  /** is EPR */
+  bool isEPR( TypeNode tn ) const { return d_non_epr.find( tn )==d_non_epr.end(); }
+  /** is EPR constant */
+  bool isEPRConstant( TypeNode tn, Node k ); 
+  /** add EPR constant */
+  void addEPRConstant( TypeNode tn, Node k ); 
+  /** get EPR axiom */
+  Node mkEPRAxiom( TypeNode tn );
+  /** has EPR axiom */
+  bool hasEPRAxiom( TypeNode tn ) const { return d_epr_axiom.find( tn )!=d_epr_axiom.end(); }
+};
 
 }
 }
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 963889a85..de8875ae3 100755
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -20,11 +20,12 @@
 #include "theory/quantifiers/trigger.h"
 
 using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
 
 bool QuantifiersRewriter::isClause( Node n ){
   if( isLiteral( n ) ){
@@ -1074,9 +1075,9 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
   return body;
 }
 
-Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, bool pol ){
+Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg ){
   if( body.getKind()==FORALL ){
-    if( pol && ( options::prenexQuant()==PRENEX_ALL || body.getNumChildren()==2 ) ){
+    if( ( pol || prenexAgg ) && ( options::prenexQuantUser() || body.getNumChildren()==2 ) ){
       std::vector< Node > terms;
       std::vector< Node > subs;
       //for doing prenexing of same-signed quantifiers
@@ -1085,14 +1086,27 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
         terms.push_back( body[0][i] );
         subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) );
       }
-      args.insert( args.end(), subs.begin(), subs.end() );
+      if( pol ){
+        args.insert( args.end(), subs.begin(), subs.end() );
+      }else{
+        nargs.insert( nargs.end(), subs.begin(), subs.end() );
+      }
       Node newBody = body[1];
       newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
       return newBody;
-    }else{
-      return body;
     }
-  }else{
+  //must remove structure
+  }else if( prenexAgg && body.getKind()==kind::ITE && body.getType().isBoolean() ){
+    Node nn = NodeManager::currentNM()->mkNode( kind::AND,
+              NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ),
+              NodeManager::currentNM()->mkNode( kind::OR, body[0], body[2] ) );
+    return computePrenex( nn, args, nargs, pol, prenexAgg );
+  }else if( prenexAgg && body.getKind()==kind::IFF ){
+    Node nn = NodeManager::currentNM()->mkNode( kind::AND,
+              NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ),
+              NodeManager::currentNM()->mkNode( kind::OR, body[0], body[1].notNode() ) );
+    return computePrenex( nn, args, nargs, pol, prenexAgg );
+  }else if( body.getType().isBoolean() ){
     Assert( body.getKind()!=EXISTS );
     bool childrenChanged = false;
     std::vector< Node > newChildren;
@@ -1101,7 +1115,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
       bool newPol;
       QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol );
       if( newHasPol ){
-        Node n = computePrenex( body[i], args, newPol );
+        Node n = computePrenex( body[i], args, nargs, newPol, prenexAgg );
         newChildren.push_back( n );
         if( n!=body[i] ){
           childrenChanged = true;
@@ -1116,10 +1130,98 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
       }else{
         return NodeManager::currentNM()->mkNode( body.getKind(), newChildren );
       }
+    }
+  }
+  return body;
+}
+
+Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel ){
+  if( containsQuantifiers( n ) ){
+    if( topLevel && options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL && ( n.getKind()==AND || ( n.getKind()==NOT && n[0].getKind()==OR ) ) ){
+      std::vector< Node > children;
+      Node nc = n.getKind()==NOT ? n[0] : n;
+      for( unsigned i=0; i<nc.getNumChildren(); i++ ){
+        Node ncc = computePrenexAgg( nc[i], true );
+        if( n.getKind()==NOT ){
+          ncc = ncc.negate();        
+        }
+        children.push_back( ncc );
+      }
+      return NodeManager::currentNM()->mkNode( AND, children );
+    }else if( n.getKind()==NOT ){
+      return computePrenexAgg( n[0], false ).negate();
+    }else if( n.getKind()==FORALL ){
+    /*
+      Node nn = computePrenexAgg( n[1], false );
+      if( nn!=n[1] ){
+        if( n.getNumChildren()==2 ){
+          return NodeManager::currentNM()->mkNode( FORALL, n[0], nn );
+        }else{
+          return NodeManager::currentNM()->mkNode( FORALL, n[0], nn, n[2] );
+        }
+      }
+      */
+      std::vector< Node > children;
+      if( n[1].getKind()==OR && options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL ){
+        for( unsigned i=0; i<n[1].getNumChildren(); i++ ){
+          children.push_back( computePrenexAgg( n[1][i], false ) );
+        }
+      }else{
+        children.push_back( computePrenexAgg( n[1], false ) );
+      }
+      std::vector< Node > args;
+      for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
+        args.push_back( n[0][i] );
+      }
+      std::vector< Node > nargs;
+      //for each child, strip top level quant
+      for( unsigned i=0; i<children.size(); i++ ){
+        if( children[i].getKind()==FORALL ){
+          for( unsigned j=0; j<children[i][0].getNumChildren(); j++ ){
+            args.push_back( children[i][0][j] );
+          }
+          children[i] = children[i][1];
+        }
+      }
+      Node nb = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children );
+      return mkForall( args, nb, true );
     }else{
-      return body;
+      std::vector< Node > args;
+      std::vector< Node > nargs;
+      Node nn = computePrenex( n, args, nargs, true, true );
+      if( n!=nn ){
+        Node nnn = computePrenexAgg( nn, false );
+        //merge prenex
+        if( nnn.getKind()==FORALL ){
+          for( unsigned i=0; i<nnn[0].getNumChildren(); i++ ){
+            args.push_back( nnn[0][i] );
+          }
+          nnn = nnn[1];
+          //pos polarity variables are inner
+          if( !args.empty() ){
+            nnn = mkForall( args, nnn, true );
+          }
+          args.clear();
+        }else if( nnn.getKind()==NOT && nnn[0].getKind()==FORALL ){
+          for( unsigned i=0; i<nnn[0][0].getNumChildren(); i++ ){
+            nargs.push_back( nnn[0][0][i] );
+          }
+          nnn = nnn[0][1].negate();
+        }
+        if( !nargs.empty() ){
+          nnn = mkForall( nargs, nnn.negate(), true ).negate();
+        }
+        if( !args.empty() ){
+          nnn = mkForall( args, nnn, true );
+        }
+        return nnn;
+      }else{
+        Assert( args.empty() );
+        Assert( nargs.empty() );
+      }
     }
   }
+  return n;
 }
 
 Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ) {
@@ -1237,6 +1339,26 @@ Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttri
     return NodeManager::currentNM()->mkNode( kind::FORALL, children );
   }
 }
+Node QuantifiersRewriter::mkForall( std::vector< Node >& args, Node body, bool marked ) {
+  if( args.empty() ){
+    return body;
+  }else{
+    std::vector< Node > children;
+    children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
+    children.push_back( body );
+    std::vector< Node > iplc;
+    if( marked ){
+      Node avar = NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() );
+      QuantIdNumAttribute ida;
+      avar.setAttribute(ida,0);
+      iplc.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, avar ) );
+    }
+    if( !iplc.empty() ){
+      children.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, iplc ) );
+    }
+    return NodeManager::currentNM()->mkNode( FORALL, children );
+  }
+}
 
 //computes miniscoping, also eliminates variables that do not occur free in body
 Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ){
@@ -1294,21 +1416,25 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo
 }
 
 Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& args, Node body ){
-  std::map< Node, std::vector< Node > > varLits;
-  std::map< Node, std::vector< Node > > litVars;
-  if( body.getKind()==OR ){
+  std::map<Node, std::vector<Node> > varLits;
+  std::map<Node, std::vector<Node> > litVars;
+  if (body.getKind() == OR) {
     Trace("ag-miniscope") << "compute aggressive miniscoping on " << body << std::endl;
-    for( size_t i=0; i<body.getNumChildren(); i++ ){
-      std::vector< Node > activeArgs;
-      computeArgVec( args, activeArgs, body[i] );
-      for (unsigned j=0; j<activeArgs.size(); j++ ){
-        varLits[activeArgs[j]].push_back( body[i] );
-      }
-      litVars[body[i]].insert( litVars[body[i]].begin(), activeArgs.begin(), activeArgs.end() );
+    for (size_t i = 0; i < body.getNumChildren(); i++) {
+      std::vector<Node> activeArgs;
+      computeArgVec(args, activeArgs, body[i]);
+      for (unsigned j = 0; j < activeArgs.size(); j++) {
+        varLits[activeArgs[j]].push_back(body[i]);
+      }
+      std::vector<Node>& lit_body_i = litVars[body[i]];
+      std::vector<Node>::iterator lit_body_i_begin = lit_body_i.begin();
+      std::vector<Node>::const_iterator active_begin = activeArgs.begin();
+      std::vector<Node>::const_iterator active_end = activeArgs.end();
+      lit_body_i.insert(lit_body_i_begin, active_begin, active_end);
     }
     //find the variable in the least number of literals
     Node bestVar;
-    for( std::map< Node, std::vector< Node > >::iterator it = varLits.begin(); it != varLits.end(); ++it ){
+    for( std::map< Node, std::vector<Node> >::iterator it = varLits.begin(); it != varLits.end(); ++it ){
       if( bestVar.isNull() || varLits[bestVar].size()>it->second.size() ){
         bestVar = it->first;
       }
@@ -1318,9 +1444,9 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg
       //we can miniscope
       Trace("ag-miniscope") << "Miniscope on " << bestVar << std::endl;
       //make the bodies
-      std::vector< Node > qlit1;
+      std::vector<Node> qlit1;
       qlit1.insert( qlit1.begin(), varLits[bestVar].begin(), varLits[bestVar].end() );
-      std::vector< Node > qlitt;
+      std::vector<Node> qlitt;
       //for all literals not containing bestVar
       for( size_t i=0; i<body.getNumChildren(); i++ ){
         if( std::find( qlit1.begin(), qlit1.end(), body[i] )==qlit1.end() ){
@@ -1328,9 +1454,9 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg
         }
       }
       //make the variable lists
-      std::vector< Node > qvl1;
-      std::vector< Node > qvl2;
-      std::vector< Node > qvsh;
+      std::vector<Node> qvl1;
+      std::vector<Node> qvl2;
+      std::vector<Node> qvsh;
       for( unsigned i=0; i<args.size(); i++ ){
         bool found1 = false;
         bool found2 = false;
@@ -1358,8 +1484,8 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg
       Assert( !qvl1.empty() );
       Assert( !qvl2.empty() || !qvsh.empty() );
       //check for literals that only contain shared variables
-      std::vector< Node > qlitsh;
-      std::vector< Node > qlit2;
+      std::vector<Node> qlitsh;
+      std::vector<Node> qlit2;
       for( size_t i=0; i<qlitt.size(); i++ ){
         bool hasVar2 = false;
         for( size_t j=0; j<litVars[qlitt[i]].size(); j++ ){
@@ -1413,7 +1539,7 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q
   }else if( computeOption==COMPUTE_COND_SPLIT ){
     return ( options::iteDtTesterSplitQuant() || options::condVarSplitQuant() ) && !is_strict_trigger;
   }else if( computeOption==COMPUTE_PRENEX ){
-    return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant() && is_std;
+    return options::prenexQuant()!=PRENEX_QUANT_NONE && !options::aggressiveMiniscopeQuant() && is_std;
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
     return ( options::varElimQuant() || options::dtVarExpandQuant() ) && is_std;
   }else{
@@ -1423,7 +1549,7 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q
 
 //general method for computing various rewrites
 Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttributes& qa ){
-  Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << std::endl;
+  Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << " " << qa.d_qid_num << std::endl;
   std::vector< Node > args;
   for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
     args.push_back( f[0][i] );
@@ -1432,6 +1558,12 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
   if( computeOption==COMPUTE_ELIM_SYMBOLS ){
     n = computeElimSymbols( n );
   }else if( computeOption==COMPUTE_MINISCOPING ){
+    if( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){
+      if( !qa.d_qid_num.isNull() ){
+        //already processed this, return self
+        return f;
+      }
+    }
     //return directly
     return computeMiniscoping( args, n, qa );
   }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
@@ -1446,7 +1578,14 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
   }else if( computeOption==COMPUTE_COND_SPLIT ){
     n = computeCondSplit( n, qa );
   }else if( computeOption==COMPUTE_PRENEX ){
-    n = computePrenex( n, args, true );
+    if( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){
+      //will rewrite at preprocess time
+      return f;
+    }else{
+      std::vector< Node > nargs;
+      n = computePrenex( n, args, nargs, true, false );
+      Assert( nargs.empty() );
+    }
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
     n = computeVarElimination( n, args, qa );
   }
@@ -1592,6 +1731,15 @@ bool QuantifiersRewriter::containsQuantifiers( Node n ){
     return cq;
   }
 }
+bool QuantifiersRewriter::isPrenexNormalForm( Node n ) {
+  if( n.getKind()==FORALL ){
+    return n[1].getKind()!=FORALL && isPrenexNormalForm( n[1] );
+  }else if( n.getKind()==NOT ){
+    return n[0].getKind()!=NOT && isPrenexNormalForm( n[0] );
+  }else{
+    return !containsQuantifiers( n );
+  }
+}
 
 Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs ){
   Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl;
@@ -1662,21 +1810,37 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
   return n;
 }
 
+
 Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
   Node prev = n;
-  if( options::preSkolemQuant() ){
-    if( !isInst || !options::preSkolemQuantNested() ){
-      Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl;
-      //apply pre-skolemization to existential quantifiers
-      std::vector< TypeNode > fvTypes;
-      std::vector< TNode > fvs;
-      n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs );
+  if( n.getKind() == kind::REWRITE_RULE ){
+    n = quantifiers::QuantifiersRewriter::rewriteRewriteRule( n );
+  }else{
+    if( options::preSkolemQuant() ){
+      if( !isInst || !options::preSkolemQuantNested() ){
+        Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl;
+        //apply pre-skolemization to existential quantifiers
+        std::vector< TypeNode > fvTypes;
+        std::vector< TNode > fvs;
+        n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs );
+      }
     }
   }
+  //pull all quantifiers globally
+  if( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){
+    Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl;
+    n = quantifiers::QuantifiersRewriter::computePrenexAgg( n, true );
+    n = Rewriter::rewrite( n );
+    Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl;
+    //Assert( isPrenexNormalForm( n ) );
+  }
   if( n!=prev ){       
-    Trace("quantifiers-preprocess") << "Preprocess " << prev<< std::endl;
+    Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl;
     Trace("quantifiers-preprocess") << "..returned " << n << std::endl;
   }
   return n;
 }
 
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 60dc8ab10..90a22f4b7 100755
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -38,7 +38,6 @@ public:
 private:
   static bool addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged );
   static void addNodeToOrBuilder( Node n, NodeBuilder<>& t );
-  static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa );
   static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited );
   static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n );
   static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl );
@@ -53,14 +52,15 @@ private:
   static bool computeVariableElimLit( Node n, bool pol, std::vector< Node >& args, std::vector< Node >& var, std::vector< Node >& subs,
                                       std::map< Node, std::map< bool, std::map< Node, bool > > >& num_bounds );
   static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa );
-private:
+public:
   static Node computeElimSymbols( Node body );
   static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa );
   static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
   //cache is dependent upon currCond, icache is not, new_conds are negated conditions
   static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa );
   static Node computeCondSplit( Node body, QAttributes& qa );
-  static Node computePrenex( Node body, std::vector< Node >& args, bool pol );
+  static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg );
+  static Node computePrenexAgg( Node n, bool topLevel );
   static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa );
   static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa );
 private:
@@ -89,8 +89,11 @@ private:
   static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
 public:
   static Node rewriteRewriteRule( Node r );
-  static bool containsQuantifiers(Node n);
+  static bool containsQuantifiers( Node n );
+  static bool isPrenexNormalForm( Node n );
   static Node preprocess( Node n, bool isInst = false );
+  static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa );
+  static Node mkForall( std::vector< Node >& args, Node body, bool marked = false );
 };/* class QuantifiersRewriter */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index 2b90520fd..aae8f6c5b 100755
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -51,7 +51,10 @@ private:
   //what each literal does
   class RDomainLit {
   public:
-    RDomainLit() : d_merge(false){}
+    RDomainLit() : d_merge(false){
+      d_rd[0] = NULL;
+      d_rd[1] = NULL;
+    }
     ~RDomainLit(){}
     bool d_merge;
     RDomain * d_rd[2];
@@ -72,6 +75,7 @@ public:
   RDomain * getRDomain( Node n, int i, bool getParent = true );
 };/* class RelevantDomain */
 
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 2c58b8f77..ec1b41a98 100755
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -20,6 +20,7 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/inst_match_generator.h"
 #include "theory/quantifiers/model_engine.h"
+#include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/theory_engine.h"
@@ -204,6 +205,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) {
       Trace("rewrite-engine-inst-debug") << "...No qinfo." << std::endl;
     }
   }
+  d_quantEngine->d_statistics.d_instantiations_rr += addedLemmas;
   Trace("rewrite-engine-inst") << "-> Generated " << addedLemmas << " lemmas." << std::endl;
   return addedLemmas;
 }
@@ -294,6 +296,11 @@ void RewriteEngine::assertNode( Node n ) {
 
 }
 
+bool RewriteEngine::checkCompleteFor( Node q ) { 
+  // by semantics of rewrite rules, saturation -> SAT 
+  return std::find( d_rr_quant.begin(), d_rr_quant.end(), q )!=d_rr_quant.end();
+}
+
 Node RewriteEngine::getInstConstNode( Node n, Node q ) {
   std::map< Node, Node >::iterator it = d_inst_const_node[q].find( n );
   if( it==d_inst_const_node[q].end() ){
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index 424530696..ef3337e53 100755
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -18,19 +18,17 @@
 #ifndef __CVC4__REWRITE_ENGINE_H
 #define __CVC4__REWRITE_ENGINE_H
 
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/trigger.h"
-
+#include "context/cdchunk_list.h"
 #include "context/context.h"
 #include "context/context_mm.h"
-#include "context/cdchunk_list.h"
+#include "theory/quantifiers/trigger.h"
+#include "theory/quantifiers/quant_conflict_find.h"
+#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-class QuantInfo;
-
 class RewriteEngine : public QuantifiersModule
 {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
@@ -57,7 +55,8 @@ public:
   bool needsCheck( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
   void registerQuantifier( Node f );
-  void assertNode( Node n );  
+  void assertNode( Node n );
+  bool checkCompleteFor( Node q );
   /** Identify this module */
   std::string identify() const { return "RewriteEngine"; }
 };
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index d3a5e178f..2c6bfb7d3 100755
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -33,14 +33,14 @@
 #include "util/bitvector.h"
 
 using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-
 using namespace CVC4::theory::inst;
 
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
 TNode TermArgTrie::existsTerm( std::vector< TNode >& reps, int argIndex ) {
   if( argIndex==(int)reps.size() ){
     if( d_data.empty() ){
@@ -84,15 +84,25 @@ void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) {
   }
 }
 
-TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_inactive_map( c ), d_op_id_count( 0 ), d_typ_id_count( 0 ) {
-  d_true = NodeManager::currentNM()->mkConst( true );
-  d_false = NodeManager::currentNM()->mkConst( false );
-  d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
-  d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
-  if( options::ceGuidedInst() ){
-    d_sygus_tdb = new TermDbSygus( c, qe );
-  }else{
-    d_sygus_tdb = NULL;
+TermDb::TermDb(context::Context* c, context::UserContext* u,
+               QuantifiersEngine* qe)
+    : d_quantEngine(qe),
+      d_inactive_map(c),
+      d_op_id_count(0),
+      d_typ_id_count(0),
+      d_sygus_tdb(NULL) {
+  d_consistent_ee = true;
+  d_true = NodeManager::currentNM()->mkConst(true);
+  d_false = NodeManager::currentNM()->mkConst(false);
+  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
+  d_one = NodeManager::currentNM()->mkConst(Rational(1));
+  if (options::ceGuidedInst()) {
+    d_sygus_tdb = new TermDbSygus(c, qe);
+  }
+}
+TermDb::~TermDb(){
+  if(d_sygus_tdb) {
+    delete d_sygus_tdb;
   }
 }
 
@@ -129,7 +139,7 @@ Node TermDb::getMatchOperator( Node n ) {
   Kind k = n.getKind();
   //datatype operators may be parametric, always assume they are
   if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || 
-      k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER ){
+      k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==SEP_PTO ){
     //since it is parametric, use a particular one as op
     TypeNode tn = n[0].getType();
     Node op = n.getOperator();
@@ -175,17 +185,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
           if( d_sygus_tdb ){
             d_sygus_tdb->registerEvalTerm( n );
           }
-
-          if( options::eagerInstQuant() ){
-            for( unsigned i=0; i<n.getNumChildren(); i++ ){
-              if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
-                int addedLemmas = 0;
-                for( unsigned i=0; i<d_op_triggers[op].size(); i++ ){
-                  addedLemmas += d_op_triggers[op][i]->addTerm( n );
-                }
-              }
-            }
-          }
         }
       }else{
         setTermInactive( n );
@@ -1319,19 +1318,25 @@ bool TermDb::mayComplete( TypeNode tn ) {
 
 void TermDb::computeVarContains( Node n, std::vector< Node >& varContains ) {
   std::map< Node, bool > visited;
-  computeVarContains2( n, varContains, visited );
+  computeVarContains2( n, INST_CONSTANT, varContains, visited );
+}
+
+void TermDb::computeQuantContains( Node n, std::vector< Node >& quantContains ) {
+  std::map< Node, bool > visited;
+  computeVarContains2( n, FORALL, quantContains, visited );
 }
 
-void TermDb::computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited ){
+
+void TermDb::computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited ){
   if( visited.find( n )==visited.end() ){
     visited[n] = true;
-    if( n.getKind()==INST_CONSTANT ){
+    if( n.getKind()==k ){
       if( std::find( varContains.begin(), varContains.end(), n )==varContains.end() ){
         varContains.push_back( n );
       }
     }else{
       for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        computeVarContains2( n[i], varContains, visited );
+        computeVarContains2( n[i], k, varContains, visited );
       }
     }
   }
@@ -1963,7 +1968,7 @@ bool TermDb::isComm( Kind k ) {
 }
 
 bool TermDb::isBoolConnective( Kind k ) {
-  return k==OR || k==AND || k==IFF || k==ITE || k==FORALL || k==NOT;
+  return k==OR || k==AND || k==IFF || k==ITE || k==FORALL || k==NOT || k==SEP_STAR;
 }
 
 void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
@@ -2163,6 +2168,10 @@ void TermDb::computeQuantAttributes( Node q, QAttributes& qa ){
           qa.d_quant_elim_partial = true;
           //don't set owner, should happen naturally
         }
+        if( avar.hasAttribute(QuantIdNumAttribute()) ){
+          qa.d_qid_num = avar;
+          Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl;
+        }
         if( avar.getKind()==REWRITE_RULE ){
           Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl;
           Assert( i==0 );
@@ -2254,6 +2263,25 @@ bool TermDb::isQAttrQuantElimPartial( Node q ) {
   }
 }
 
+int TermDb::getQAttrQuantIdNum( Node q ) {
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it!=d_qattr.end() ){
+    if( !it->second.d_qid_num.isNull() ){
+      return it->second.d_qid_num.getAttribute(QuantIdNumAttribute());
+    }
+  }
+  return -1;
+}
+
+Node TermDb::getQAttrQuantIdNumNode( Node q ) {
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it==d_qattr.end() ){
+    return Node::null();
+  }else{
+    return it->second.d_qid_num;
+  }
+}
+
 TermDbSygus::TermDbSygus( context::Context* c, QuantifiersEngine* qe ) : d_quantEngine( qe ){
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
@@ -3125,7 +3153,6 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
           std::string name = std::string( str.begin() + found +1, str.end() );
           out << name;
         }else{
-          Trace("ajr-temp") << "[[print operator " << op << "]]" << std::endl;
           out << op;
         }
         if( n.getNumChildren()>0 ){
@@ -3281,3 +3308,6 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems
   }
 }
 
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 7ab3668eb..d4fdaa5e5 100755
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -105,6 +105,11 @@ typedef expr::Attribute< QuantElimAttributeId, bool > QuantElimAttribute;
 struct QuantElimPartialAttributeId {};
 typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAttribute;
 
+/** Attribute for id number */
+struct QuantIdNumAttributeId {};
+typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute;
+
+
 class QuantifiersEngine;
 
 namespace inst{
@@ -145,6 +150,7 @@ public:
   bool d_quant_elim;
   bool d_quant_elim_partial;
   Node d_ipl;
+  Node d_qid_num;
   bool isRewriteRule() { return !d_rr.isNull(); }
   bool isFunDef() { return !d_fundef_f.isNull(); }
 };
@@ -182,23 +188,25 @@ private:
   std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
   /** whether master equality engine is UF-inconsistent */
   bool d_consistent_ee;
-public:
-  TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe );
-  ~TermDb(){}
+
+ public:
+  TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe);
+  ~TermDb();
   /** boolean terms */
   Node d_true;
   Node d_false;
   /** constants */
   Node d_zero;
   Node d_one;
-public:
+
+ public:
   /** presolve (called once per user check-sat) */
   void presolve();
   /** reset (calculate which terms are active) */
   bool reset( Theory::Effort effort );
   /** identify */
   std::string identify() const { return "TermDb"; }  
-private:
+ private:
   /** map from operators to ground terms for that operator */
   std::map< Node, std::vector< Node > > d_op_map;
   /** map from type nodes to terms of that type */
@@ -301,8 +309,6 @@ private:
   /** map from universal quantifiers to the list of variables */
   std::map< Node, std::vector< Node > > d_vars;
   std::map< Node, std::map< Node, unsigned > > d_var_num;
-  /** map from universal quantifiers to the list of instantiation constants */
-  std::map< Node, std::vector< Node > > d_inst_constants;
   /** map from universal quantifiers to their inst constant body */
   std::map< Node, Node > d_inst_const_body;
   /** map from universal quantifiers to their counterexample literals */
@@ -312,6 +318,8 @@ private:
   /** make instantiation constants for */
   void makeInstantiationConstantsFor( Node q );
 public:
+  /** map from universal quantifiers to the list of instantiation constants */
+  std::map< Node, std::vector< Node > > d_inst_constants;
   /** get variable number */
   unsigned getVariableNum( Node q, Node v ) { return d_var_num[q][v]; }
   /** get the i^th instantiation constant of q */
@@ -388,7 +396,7 @@ public:
 //for triggers
 private:
   /** helper function for compute var contains */
-  static void computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited );
+  static void computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited );
   /** triggers for each operator */
   std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
   /** helper for is instance of */
@@ -402,6 +410,8 @@ public:
   static void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains );
   /** get var contains for node n */
   static void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains );
+  /** compute quant contains */
+  static void computeQuantContains( Node n, std::vector< Node >& quantContains );
   /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */
   static int isInstanceOf( Node n1, Node n2 );
   /** filter all nodes that have instances */
@@ -541,6 +551,10 @@ public:
   bool isQAttrQuantElim( Node q );
   /** is quant elim partial */
   bool isQAttrQuantElimPartial( Node q );
+  /** get quant id num */
+  int getQAttrQuantIdNum( Node q );
+  /** get quant id num */
+  Node getQAttrQuantIdNumNode( Node q );
   /** compute quantifier attributes */
   static void computeQuantAttributes( Node q, QAttributes& qa );
 };/* class TermDb */
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 7ad13b3a8..e97a76ce6 100755
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -88,6 +88,13 @@ void TheoryQuantifiers::presolve() {
   }
 }
 
+void TheoryQuantifiers::ppNotifyAssertions( std::vector< Node >& assertions ) {
+  Trace("quantifiers-presolve") << "TheoryQuantifiers::ppNotifyAssertions" << std::endl;
+  if( getQuantifiersEngine() ){
+    getQuantifiersEngine()->ppNotifyAssertions( assertions );
+  }
+}
+
 Node TheoryQuantifiers::getValue(TNode n) {
   //NodeManager* nodeManager = NodeManager::currentNM();
   switch(n.getKind()) {
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 6775e0536..ba5a75d86 100755
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -61,6 +61,7 @@ public:
   void notifyEq(TNode lhs, TNode rhs);
   void preRegisterTerm(TNode n);
   void presolve();
+  void ppNotifyAssertions( std::vector< Node >& assertions );
   void check(Effort e);
   Node getNextDecisionRequest();
   Node getValue(TNode n);
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 2faed3af0..3017238ca 100755
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -76,12 +76,6 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes )
     ++(qe->d_statistics.d_multi_triggers);
   }
   //Notice() << "Trigger : " << (*this) << "  for " << f << std::endl;
-  if( options::eagerInstQuant() ){
-    for( int i=0; i<(int)d_nodes.size(); i++ ){
-      Node op = qe->getTermDatabase()->getMatchOperator( d_nodes[i] );
-      qe->getTermDatabase()->registerTrigger( this, op );
-    }
-  }
   Trace("trigger-debug") << "Finished making trigger." << std::endl;
 }
 
@@ -107,10 +101,6 @@ bool Trigger::getMatch( Node f, Node t, InstMatch& m ){
   return ((InstMatchGenerator*)d_mg)->getMatch( f, t, m, d_quantEngine );
 }
 
-int Trigger::addTerm( Node t ){
-  return d_mg->addTerm( d_f, t, d_quantEngine );
-}
-
 Node Trigger::getInstPattern(){
   return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes );
 }
@@ -363,7 +353,8 @@ bool Trigger::isAtomicTrigger( Node n ){
 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;
+         k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON ||
+         k==SEP_PTO;
 }
 
 bool Trigger::isRelationalTrigger( Node n ) {
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 6d7bf1f4d..631627331 100755
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -72,8 +72,6 @@ class Trigger {
       Currently the trigger should not be a multi-trigger.
   */
   bool getMatch( Node f, Node t, InstMatch& m);
-  /** add ground term t, called when t is added to the TermDb */
-  int addTerm( Node t );
   /** return whether this is a multi-trigger */
   bool isMultiTrigger() { return d_nodes.size()>1; }
   /** get inst pattern list */