SyGuS streaming solution mode (#1131)

* Refactor conjecture class in ce guided instantiation, move to own file.  In preparation for sygus streaming mode.

* Infrastructure for streaming guards, more cleanup.

* Do explicit exclusion to move to next solution for sygus streaming option, now functional. More cleanup.

* More cleanup, add comments.

* Update comments

* Optimizations for invariant synthesis. Fix corner case for single invocation inference, more encapsulation in single inv utility. Minor fix for variable elimination in quantifiers rewriter.

* Fix makefile.

* Cleanup.

* Remove unused includes.

* Minor

11 files changed, 1135 insertions, 930 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 3a41b30ab..7b9a607a1 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -350,6 +350,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/bv_inverter.h \
 	theory/quantifiers/candidate_generator.cpp \
 	theory/quantifiers/candidate_generator.h \
+	theory/quantifiers/ce_guided_conjecture.cpp \
+	theory/quantifiers/ce_guided_conjecture.h \
 	theory/quantifiers/ce_guided_instantiation.cpp \
 	theory/quantifiers/ce_guided_instantiation.h \
 	theory/quantifiers/ce_guided_single_inv.cpp \
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index d5619ed77..44fbc4ee7 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -270,6 +270,8 @@ option sygusMinGrammarAgg --sygus-min-grammar-agg bool :default false
   aggressively minimize sygus grammars
 option sygusAddConstGrammar --sygus-add-const-grammar bool :default true
   statically add constants appearing in conjecture to grammars
+option sygusTemplEmbedGrammar --sygus-templ-embed-grammar bool :default false
+  embed sygus templates into grammars
   
 option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToSygusInvTemplMode
   template mode for sygus invariant synthesis
@@ -287,6 +289,9 @@ option sygusCRefEval --sygus-cref-eval bool :default true
 option sygusCRefEvalMinExp --sygus-cref-eval-min-exp bool :default true
   use min explain for direct evaluation of refinement lemmas for conflict analysis
   
+option sygusStream --sygus-stream bool :default false
+  enumerate a stream of solutions instead of terminating after the first one
+  
 # CEGQI applied to general quantified formulas
 option cbqi --cbqi bool :read-write :default false
  turns on counterexample-based quantifier instantiation
diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp
new file mode 100644
index 000000000..fbf08e909
--- /dev/null
+++ b/src/theory/quantifiers/ce_guided_conjecture.cpp
@@ -0,0 +1,785 @@
+/*********************                                                        */
+/*! \file ce_guided_conjecture.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 class that encapsulates counterexample-guided instantiation
+ **        techniques for a single SyGuS synthesis conjecture
+ **/
+#include "theory/quantifiers/ce_guided_conjecture.h"
+
+#include "expr/datatype.h"
+#include "options/quantifiers_options.h"
+#include "prop/prop_engine.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/term_database_sygus.h"
+#include "theory/theory_engine.h"
+
+using namespace CVC4::kind;
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+// recursion is not an issue since OR nodes are flattened by the (quantifiers) rewriter
+// this function is for sanity since solution correctness in SyGuS depends on fully miniscoping based on this function
+void collectDisjuncts( Node n, std::vector< Node >& d ) {
+  if( n.getKind()==OR ){
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      collectDisjuncts( n[i], d );
+    }
+  }else{
+    d.push_back( n );
+  }
+}
+
+CegConjecture::CegConjecture( QuantifiersEngine * qe )
+    : d_qe( qe ) {
+  d_refine_count = 0;
+  d_ceg_si = new CegConjectureSingleInv( qe, this );
+  d_ceg_pbe = new CegConjecturePbe( qe, this );
+}
+
+CegConjecture::~CegConjecture() {
+  delete d_ceg_si;
+  delete d_ceg_pbe;
+}
+
+Node CegConjecture::convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars, std::map< Node, Node >& visited ){
+  std::map< Node, Node >::iterator it = visited.find( n );
+  if( it==visited.end() ){
+    Node ret = n;
+    
+    std::vector< Node > children;
+    bool childChanged = false;
+    bool madeOp = false;
+    Kind ret_k = n.getKind();
+    Node op;
+    if( n.getNumChildren()>0 ){
+      if( n.getKind()==kind::APPLY_UF ){
+        op = n.getOperator();
+      }
+    }else{
+      op = n;
+    }
+    // is it a synth function?
+    std::map< Node, Node >::iterator its = synth_fun_vars.find( op );
+    if( its!=synth_fun_vars.end() ){
+      Assert( its->second.getType().isDatatype() );
+      // make into evaluation function
+      const Datatype& dt = ((DatatypeType)its->second.getType().toType()).getDatatype();
+      Assert( dt.isSygus() );
+      children.push_back( Node::fromExpr( dt.getSygusEvaluationFunc() ) );
+      children.push_back( its->second );
+      madeOp = true;
+      childChanged = true;
+      ret_k = kind::APPLY_UF;
+    }
+    if( n.getNumChildren()>0 || childChanged ){
+      if( !madeOp ){
+        if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+          children.push_back( n.getOperator() );
+        }
+      }
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        Node nc = convertToEmbedding( n[i], synth_fun_vars, visited ); 
+        childChanged = childChanged || nc!=n[i];
+        children.push_back( nc );
+      }
+      if( childChanged ){
+        ret = NodeManager::currentNM()->mkNode( ret_k, children );
+      }
+    }
+    visited[n] = ret;
+    return ret;
+  }else{
+    return it->second;
+  }
+}
+
+void CegConjecture::collectConstants( Node n, std::map< TypeNode, std::vector< Node > >& consts, std::map< Node, bool >& visited ) {
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    if( n.isConst() ){
+      TypeNode tn = n.getType();
+      Node nc = n;
+      if( tn.isReal() ){
+        nc = NodeManager::currentNM()->mkConst( n.getConst<Rational>().abs() );
+      }
+      if( std::find( consts[tn].begin(), consts[tn].end(), nc )==consts[tn].end() ){
+        Trace("cegqi-debug") << "...consider const : " << nc << std::endl;
+        consts[tn].push_back( nc );
+      }
+    }
+    
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      collectConstants( n[i], consts, visited );
+    }
+  }
+}
+
+
+void CegConjecture::assign( Node q ) {
+  Assert( d_embed_quant.isNull() );
+  Assert( q.getKind()==FORALL );
+  Trace("cegqi") << "CegConjecture : assign : " << q << std::endl;
+  d_quant = q;
+
+  Node simp_quant = q;
+  //register with single invocation if applicable
+  if( d_qe->getTermDatabase()->isQAttrSygus( d_quant ) ){
+    d_ceg_si->initialize( d_quant );
+    simp_quant = d_ceg_si->getSimplifiedConjecture();
+  }
+
+  // convert to deep embedding and finalize single invocation here
+  // now, construct the grammar
+  Trace("cegqi") << "CegConjecture : convert to deep embedding..." << std::endl;
+  std::map< TypeNode, std::vector< Node > > extra_cons;
+  Trace("cegqi") << "CegConjecture : collect constants..." << std::endl;
+  if( options::sygusAddConstGrammar() ){
+    std::map< Node, bool > visited;
+    collectConstants( q[1], extra_cons, visited );
+  }
+  bool has_ites = true;
+  bool is_syntax_restricted = false;
+  std::vector< Node > qchildren;
+  std::map< Node, Node > visited;
+  std::map< Node, Node > synth_fun_vars;
+  std::vector< Node > ebvl;
+  Node qbody_subs = simp_quant[1];
+  for( unsigned i=0; i<simp_quant[0].getNumChildren(); i++ ){
+    Node v = simp_quant[0][i];
+    Node sf = v.getAttribute(SygusSynthFunAttribute());
+    Assert( !sf.isNull() );
+    Node sfvl = sf.getAttribute(SygusSynthFunVarListAttribute());
+    // sfvl may be null for constant synthesis functions
+    Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " << sfvl << std::endl;
+    TypeNode tn;
+    std::stringstream ss;
+    ss << sf;
+    if( v.getType().isDatatype() && ((DatatypeType)v.getType().toType()).getDatatype().isSygus() ){
+      tn = v.getType();
+    }else{
+      // make the default grammar
+      tn = d_qe->getTermDatabaseSygus()->mkSygusDefaultType( v.getType(), sfvl, ss.str(), extra_cons );
+    }
+    Node templ = d_ceg_si->getTemplate( sf );
+    if( !templ.isNull() ){
+      TNode templ_arg = d_ceg_si->getTemplateArg( sf );
+      Assert( !templ_arg.isNull() );
+        Trace("cegqi-debug") << "Template for " << sf << " is : " << templ << " with arg " << templ_arg << std::endl;
+      // if there is a template for this argument, make a sygus type on top of it
+      if( options::sygusTemplEmbedGrammar() ){
+        Trace("cegqi-debug") << "  embed this template as a grammar..." << std::endl;
+        tn = d_qe->getTermDatabaseSygus()->mkSygusTemplateType( templ, templ_arg, tn, sfvl, ss.str() );
+      }else{
+        // otherwise, apply it as a preprocessing pass 
+        Trace("cegqi-debug") << "  apply this template as a substituion during preprocess..." << std::endl;
+        std::vector< Node > schildren;
+        std::vector< Node > largs;
+        for( unsigned j=0; j<sfvl.getNumChildren(); j++ ){
+          schildren.push_back( sfvl[j] );
+          largs.push_back( NodeManager::currentNM()->mkBoundVar( sfvl[j].getType() ) );
+        }
+        std::vector< Node > subsfn_children;
+        subsfn_children.push_back( sf );
+        subsfn_children.insert( subsfn_children.end(), schildren.begin(), schildren.end() );
+        Node subsfn = NodeManager::currentNM()->mkNode( kind::APPLY_UF, subsfn_children );
+        TNode subsf = subsfn;
+        Trace("cegqi-debug") << "  substitute arg : " << templ_arg << " -> " << subsf << std::endl;
+        templ = templ.substitute( templ_arg, subsf );
+        // substitute lambda arguments
+        templ = templ.substitute( schildren.begin(), schildren.end(), largs.begin(), largs.end() );
+        Node subsn = NodeManager::currentNM()->mkNode( kind::LAMBDA, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, largs ), templ );
+        TNode var = sf;
+        TNode subs = subsn;
+        Trace("cegqi-debug") << "  substitute : " << var << " -> " << subs << std::endl;
+        qbody_subs = qbody_subs.substitute( var, subs );
+        Trace("cegqi-debug") << "  body is now : " << qbody_subs << std::endl;
+      }
+    }
+    d_qe->getTermDatabaseSygus()->registerSygusType( tn );
+    // check grammar restrictions
+    if( !d_qe->getTermDatabaseSygus()->sygusToBuiltinType( tn ).isBoolean() ){
+      if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){
+        has_ites = false;
+      }
+    }
+    Assert( tn.isDatatype() );
+    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+    Assert( dt.isSygus() );
+    if( !dt.getSygusAllowAll() ){
+      is_syntax_restricted = true;
+    }
+
+    // ev is the first-order variable corresponding to this synth fun
+    std::stringstream ssf;
+    ssf << "f" << sf;
+    Node ev = NodeManager::currentNM()->mkBoundVar( ssf.str(), tn );
+    ebvl.push_back( ev );
+    synth_fun_vars[sf] = ev;
+    Trace("cegqi") << "...embedding synth fun : " << sf << " -> " << ev << std::endl;
+  }
+  qchildren.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, ebvl ) );
+  if( qbody_subs!=simp_quant[1] ){
+    Trace("cegqi") << "...rewriting : " << qbody_subs << std::endl;
+    qbody_subs = Rewriter::rewrite( qbody_subs );
+    Trace("cegqi") << "...got : " << qbody_subs << std::endl;
+  }
+  qchildren.push_back( convertToEmbedding( qbody_subs, synth_fun_vars, visited ) );
+  if( q.getNumChildren()==3 ){
+    qchildren.push_back( q[2] );
+  }
+  q = NodeManager::currentNM()->mkNode( kind::FORALL, qchildren );
+  Trace("cegqi") << "CegConjecture : converted to embedding : " << q << std::endl;
+  d_embed_quant = q;
+
+  // we now finalize the single invocation module, based on the syntax restrictions
+  if( d_qe->getTermDatabase()->isQAttrSygus( d_quant ) ){
+    d_ceg_si->finishInit( is_syntax_restricted, has_ites );
+  }
+
+  Assert( d_candidates.empty() );
+  std::vector< Node > vars;
+  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+    vars.push_back( q[0][i] );
+    Node e = NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() );
+    d_candidates.push_back( e );
+  }
+  Trace("cegqi") << "Base quantified formula is : " << q << std::endl;
+  //construct base instantiation
+  d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, vars, d_candidates ) );
+  
+  // register this term with sygus database
+  std::vector< Node > guarded_lemmas;
+  if( !isSingleInvocation() ){
+    if( options::sygusPbe() ){
+      d_ceg_pbe->initialize( d_base_inst, d_candidates, guarded_lemmas );
+    }
+    for( unsigned i=0; i<d_candidates.size(); i++ ){
+      Node e = d_candidates[i];
+      if( options::sygusPbe() ){
+        std::vector< std::vector< Node > > exs;
+        std::vector< Node > exos;
+        std::vector< Node > exts;
+        // use the PBE examples, regardless of the search algorith, since these help search space pruning
+        if( d_ceg_pbe->getPbeExamples( e, exs, exos, exts ) ){
+          d_qe->getTermDatabaseSygus()->registerPbeExamples( e, exs, exos, exts );
+        }
+      }else{
+        d_qe->getTermDatabaseSygus()->registerMeasuredTerm( e, e );
+      }
+    }
+  }
+  
+  Trace("cegqi") << "Base instantiation is :      " << d_base_inst << std::endl;
+  if( d_qe->getTermDatabase()->isQAttrSygus( d_quant ) ){
+    collectDisjuncts( d_base_inst, d_base_disj );
+    Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl;
+    //store the inner variables for each disjunct
+    for( unsigned j=0; j<d_base_disj.size(); j++ ){
+      Trace("cegqi") << "  " << j << " : " << d_base_disj[j] << std::endl;
+      d_inner_vars_disj.push_back( std::vector< Node >() );
+      //if the disjunct is an existential, store it
+      if( d_base_disj[j].getKind()==NOT && d_base_disj[j][0].getKind()==FORALL ){
+        for( unsigned k=0; k<d_base_disj[j][0][0].getNumChildren(); k++ ){
+          d_inner_vars.push_back( d_base_disj[j][0][0][k] );
+          d_inner_vars_disj[j].push_back( d_base_disj[j][0][0][k] );
+        }
+      }
+    }
+    d_syntax_guided = true;
+  }else if( d_qe->getTermDatabase()->isQAttrSynthesis( d_quant ) ){
+    d_syntax_guided = false;
+  }else{
+    Assert( false );
+  }
+  
+  // initialize the guard
+  if( !d_syntax_guided ){
+    if( d_nsg_guard.isNull() ){
+      d_nsg_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
+      d_nsg_guard = d_qe->getValuation().ensureLiteral( d_nsg_guard );
+      AlwaysAssert( !d_nsg_guard.isNull() );
+      d_qe->getOutputChannel().requirePhase( d_nsg_guard, true );
+      // negated base as a guarded lemma
+      guarded_lemmas.push_back( d_base_inst.negate() );
+    }
+  }else if( d_ceg_si->getGuard().isNull() ){
+    std::vector< Node > lems;
+    d_ceg_si->getInitialSingleInvLemma( lems );
+    for( unsigned i=0; i<lems.size(); i++ ){
+      Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation " << i << " : " << lems[i] << std::endl;
+      d_qe->getOutputChannel().lemma( lems[i] );
+      if( Trace.isOn("cegqi-debug") ){
+        Node rlem = Rewriter::rewrite( lems[i] );
+        Trace("cegqi-debug") << "...rewritten : " << rlem << std::endl;
+      }
+    }
+  }
+  Assert( !getGuard().isNull() );
+  Node gneg = getGuard().negate();
+  for( unsigned i=0; i<guarded_lemmas.size(); i++ ){
+    Node lem = NodeManager::currentNM()->mkNode( OR, gneg, guarded_lemmas[i] );
+    Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem << std::endl;
+    d_qe->getOutputChannel().lemma( lem );
+  }
+  
+  Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() << std::endl;
+}
+
+Node CegConjecture::getGuard() {
+  return !d_syntax_guided ? d_nsg_guard : d_ceg_si->getGuard();
+}
+
+bool CegConjecture::isSingleInvocation() const {
+  return d_ceg_si->isSingleInvocation();
+}
+
+bool CegConjecture::needsCheck( std::vector< Node >& lem ) {
+  if( isSingleInvocation() && !d_ceg_si->needsCheck() ){
+    return false;
+  }else{
+    bool value;
+    Assert( !getGuard().isNull() );
+    // non or fully single invocation : look at guard only
+    if( d_qe->getValuation().hasSatValue( getGuard(), value ) ) {
+      if( !value ){
+        Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl;
+        return false;
+      }
+    }else{
+      Assert( false );
+    }
+    return true;
+  }
+}
+
+
+void CegConjecture::doSingleInvCheck(std::vector< Node >& lems) {
+  if( d_ceg_si!=NULL ){
+    d_ceg_si->check(lems);
+  }
+}
+
+void CegConjecture::doBasicCheck(std::vector< Node >& lems) {
+  std::vector< Node > model_terms;
+  std::vector< Node > clist;
+  getCandidateList( clist, true );
+  Assert( clist.size()==d_quant[0].getNumChildren() );
+  getModelValues( clist, model_terms );
+  if( d_qe->addInstantiation( d_quant, model_terms ) ){
+    //record the instantiation
+    recordInstantiation( model_terms );
+  }else{
+    Assert( false );
+  }
+}
+
+bool CegConjecture::needsRefinement() { 
+  return !d_ce_sk.empty();
+}
+
+void CegConjecture::getCandidateList( std::vector< Node >& clist, bool forceOrig ) {
+  if( d_ceg_pbe->isPbe() && !forceOrig ){
+    d_ceg_pbe->getCandidateList( d_candidates, clist );
+  }else{
+    clist.insert( clist.end(), d_candidates.begin(), d_candidates.end() );
+  }
+}
+
+bool CegConjecture::constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, std::vector< Node >& candidate_values, 
+                                         std::vector< Node >& lems ) {
+  Assert( clist.size()==model_values.size() );
+  if( d_ceg_pbe->isPbe() ){
+    return d_ceg_pbe->constructCandidates( clist, model_values, d_candidates, candidate_values, lems );
+  }else{
+    Assert( model_values.size()==d_candidates.size() );
+    candidate_values.insert( candidate_values.end(), model_values.begin(), model_values.end() );
+  }
+  return true;
+}
+
+void CegConjecture::doCheck(std::vector< Node >& lems, std::vector< Node >& model_values) {
+  std::vector< Node > clist;
+  getCandidateList( clist );
+  std::vector< Node > c_model_values;
+  Trace("cegqi-check") << "CegConjuncture : check, build candidates..." << std::endl;
+  bool constructed_cand = constructCandidates( clist, model_values, c_model_values, lems );
+
+  //must get a counterexample to the value of the current candidate
+  Node inst;
+  if( constructed_cand ){
+    if( Trace.isOn("cegqi-check")  ){
+      Trace("cegqi-check") << "CegConjuncture : check candidate : " << std::endl;
+      for( unsigned i=0; i<c_model_values.size(); i++ ){
+        Trace("cegqi-check") << "  " << i << " : " << d_candidates[i] << " -> " << c_model_values[i] << std::endl;
+      }
+    }
+    Assert( c_model_values.size()==d_candidates.size() );
+    inst = d_base_inst.substitute( d_candidates.begin(), d_candidates.end(), c_model_values.begin(), c_model_values.end() );
+  }else{
+    inst = d_base_inst;
+  }
+  
+  //check whether we will run CEGIS on inner skolem variables
+  bool sk_refine = ( !isGround() || d_refine_count==0 ) && ( !d_ceg_pbe->isPbe() || constructed_cand );
+  if( sk_refine ){
+    Assert( d_ce_sk.empty() );
+    d_ce_sk.push_back( std::vector< Node >() );
+  }else{
+    if( !constructed_cand ){
+      return;
+    }
+  }
+  
+  std::vector< Node > ic;
+  ic.push_back( d_quant.negate() );
+  std::vector< Node > d;
+  collectDisjuncts( inst, d );
+  Assert( d.size()==d_base_disj.size() );
+  //immediately skolemize inner existentials
+  for( unsigned i=0; i<d.size(); i++ ){
+    Node dr = Rewriter::rewrite( d[i] );
+    if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){
+      if( constructed_cand ){
+        ic.push_back( d_qe->getTermDatabase()->getSkolemizedBody( dr[0] ).negate() );
+      }
+      if( sk_refine ){
+        Assert( !isGround() );
+        d_ce_sk.back().push_back( dr[0] );
+      }
+    }else{
+      if( constructed_cand ){
+        ic.push_back( dr );
+        if( !d_inner_vars_disj[i].empty() ){
+          Trace("cegqi-debug") << "*** quantified disjunct : " << d[i] << " simplifies to " << dr << std::endl;
+        }
+      }
+      if( sk_refine ){
+        d_ce_sk.back().push_back( Node::null() );
+      }
+    }
+  }
+  if( constructed_cand ){
+    Node lem = NodeManager::currentNM()->mkNode( OR, ic );
+    lem = Rewriter::rewrite( lem );
+    //eagerly unfold applications of evaluation function
+    if( options::sygusDirectEval() ){
+      Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl;
+      std::map< Node, Node > visited_n;
+      lem = d_qe->getTermDatabaseSygus()->getEagerUnfold( lem, visited_n );
+    }
+    if( options::sygusStream() ){
+      // if we are in streaming mode, we guard with the current stream guard
+      Node curr_stream_guard = getCurrentStreamGuard();
+      Assert( !curr_stream_guard.isNull() );
+      lem = NodeManager::currentNM()->mkNode( kind::OR, curr_stream_guard.negate(), lem );
+    }
+    lems.push_back( lem );
+    recordInstantiation( c_model_values );
+  }
+}
+        
+void CegConjecture::doRefine( std::vector< Node >& lems ){
+  Assert( lems.empty() );
+  Assert( d_ce_sk.size()==1 );
+
+  //first, make skolem substitution
+  Trace("cegqi-refine") << "doRefine : construct skolem substitution..." << std::endl;
+  std::vector< Node > sk_vars;
+  std::vector< Node > sk_subs;
+  //collect the substitution over all disjuncts
+  for( unsigned k=0; k<d_ce_sk[0].size(); k++ ){
+    Node ce_q = d_ce_sk[0][k];
+    if( !ce_q.isNull() ){
+      Assert( !d_inner_vars_disj[k].empty() );
+      Assert( d_inner_vars_disj[k].size()==d_qe->getTermDatabase()->d_skolem_constants[ce_q].size() );
+      std::vector< Node > model_values;
+      getModelValues( d_qe->getTermDatabase()->d_skolem_constants[ce_q], model_values );
+      sk_vars.insert( sk_vars.end(), d_inner_vars_disj[k].begin(), d_inner_vars_disj[k].end() );
+      sk_subs.insert( sk_subs.end(), model_values.begin(), model_values.end() );
+    }else{
+      if( !d_inner_vars_disj[k].empty() ){
+        //denegrate case : quantified disjunct was trivially true and does not need to be refined
+        //add trivial substitution (in case we need substitution for previous cex's)
+        for( unsigned i=0; i<d_inner_vars_disj[k].size(); i++ ){
+          sk_vars.push_back( d_inner_vars_disj[k][i] );
+          sk_subs.push_back( getModelValue( d_inner_vars_disj[k][i] ) ); // will return dummy value
+        }
+      }
+    }
+  } 
+  
+  //for conditional evaluation
+  std::vector< Node > lem_c;
+  Assert( d_ce_sk[0].size()==d_base_disj.size() );
+  std::vector< Node > inst_cond_c;
+  Trace("cegqi-refine") << "doRefine : Construct refinement lemma..." << std::endl;
+  for( unsigned k=0; k<d_ce_sk[0].size(); k++ ){
+    Node ce_q = d_ce_sk[0][k];
+    Trace("cegqi-refine-debug") << "  For counterexample point, disjunct " << k << " : " << ce_q << " " << d_base_disj[k] << std::endl;
+    Node c_disj;
+    if( !ce_q.isNull() ){
+      Assert( d_base_disj[k].getKind()==kind::NOT && d_base_disj[k][0].getKind()==kind::FORALL );
+      c_disj = d_base_disj[k][0][1];
+    }else{
+      if( d_inner_vars_disj[k].empty() ){
+        c_disj = d_base_disj[k].negate();
+      }else{
+        //denegrate case : quantified disjunct was trivially true and does not need to be refined
+        Trace("cegqi-refine-debug") << "*** skip " << d_base_disj[k] << std::endl;
+      }
+    }
+    if( !c_disj.isNull() ){
+      //compute the body, inst_cond
+      //standard CEGIS refinement : plug in values, assert that d_candidates must satisfy entire specification
+      lem_c.push_back( c_disj );
+    }
+  }
+  Assert( sk_vars.size()==sk_subs.size() );
+  
+  Node base_lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c );
+  
+  Trace("cegqi-refine") << "doRefine : construct and finalize lemmas..." << std::endl;
+  
+  Node lem = base_lem;
+  
+  base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
+  base_lem = Rewriter::rewrite( base_lem );
+  d_refinement_lemmas_base.push_back( base_lem );
+  
+  lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), lem );
+  
+  lem = lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
+  lem = Rewriter::rewrite( lem );
+  d_refinement_lemmas.push_back( lem );
+  lems.push_back( lem );
+
+  d_ce_sk.clear();
+}
+
+void CegConjecture::preregisterConjecture( Node q ) {
+  d_ceg_si->preregisterConjecture( q );
+}
+
+void CegConjecture::getModelValues( std::vector< Node >& n, std::vector< Node >& v ) {
+  Trace("cegqi-engine") << "  * Value is : ";
+  for( unsigned i=0; i<n.size(); i++ ){
+    Node nv = getModelValue( n[i] );
+    v.push_back( nv );
+    if( Trace.isOn("cegqi-engine") ){
+      TypeNode tn = nv.getType();
+      Trace("cegqi-engine") << n[i] << " -> ";
+      std::stringstream ss;
+      std::vector< Node > lvs;
+      TermDbSygus::printSygusTerm( ss, nv, lvs );
+      Trace("cegqi-engine") << ss.str() << " ";
+    }
+    Assert( !nv.isNull() );
+  }
+  Trace("cegqi-engine") << std::endl;
+}
+
+Node CegConjecture::getModelValue( Node n ) {
+  Trace("cegqi-mv") << "getModelValue for : " << n << std::endl;
+  return d_qe->getModel()->getValue( n );
+}
+
+void CegConjecture::debugPrint( const char * c ) {
+  Trace(c) << "Synthesis conjecture : " << d_embed_quant << std::endl;
+  Trace(c) << "  * Candidate program/output symbol : ";
+  for( unsigned i=0; i<d_candidates.size(); i++ ){
+    Trace(c) << d_candidates[i] << " ";
+  }
+  Trace(c) << std::endl;
+  Trace(c) << "  * Candidate ce skolems : ";
+  for( unsigned i=0; i<d_ce_sk.size(); i++ ){
+    Trace(c) << d_ce_sk[i] << " ";
+  }
+}
+
+Node CegConjecture::getCurrentStreamGuard() const {
+  if( d_stream_guards.empty() ){
+    return Node::null();
+  }else{
+    return d_stream_guards.back();
+  }
+}
+
+Node CegConjecture::getNextDecisionRequest( unsigned& priority ) {
+  // first, must try the guard
+  // which denotes "this conjecture is feasible"
+  Node feasible_guard = getGuard();
+  bool value;
+  if( !d_qe->getValuation().hasSatValue( feasible_guard, value ) ) {
+    priority = 0;
+    return feasible_guard;
+  }else{
+    if( value ){  
+      // the conjecture is feasible
+      if( options::sygusStream() ){
+        Assert( !isSingleInvocation() );
+        // if we are in sygus streaming mode, then get the "next guard" 
+        // which denotes "we have not yet generated the next solution to the conjecture"
+        Node curr_stream_guard = getCurrentStreamGuard();
+        bool needs_new_stream_guard = false;
+        if( curr_stream_guard.isNull() ){
+          needs_new_stream_guard = true;
+        }else{
+          // check the polarity of the guard
+          if( !d_qe->getValuation().hasSatValue( curr_stream_guard, value ) ) {
+            priority = 0;
+            return curr_stream_guard;
+          }else{
+            if( !value ){
+              Trace("cegqi-debug") << "getNextDecision : we have a new solution since stream guard was propagated false: " << curr_stream_guard << std::endl;
+              // we have generated a solution, print it
+              // get the current output stream
+              // this output stream should coincide with wherever --dump-synth is output on
+              Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
+              printSynthSolution( *nodeManagerOptions.getOut(), false );
+              // need to make the next stream guard
+              needs_new_stream_guard = true;
+              
+              // We will not refine the current candidate solution since it is a solution
+              // thus, we clear information regarding the current refinement
+              d_ce_sk.clear();
+              // However, we need to exclude the current solution using an explicit refinement 
+              // so that we proceed to the next solution. 
+              std::vector< Node > clist;
+              getCandidateList( clist );
+              Trace("cegqi-debug") << "getNextDecision : solution was : " << std::endl;
+              std::vector< Node > exp;
+              for( unsigned i=0; i<clist.size(); i++ ){
+                Node cprog = clist[i];
+                Node sol = cprog;
+                if( !d_cinfo[cprog].d_inst.empty() ){
+                  sol = d_cinfo[cprog].d_inst.back();
+                  // add to explanation of exclusion
+                  d_qe->getTermDatabaseSygus()->getExplanationForConstantEquality( cprog, sol, exp );
+                }
+                Trace("cegqi-debug") << "  " << cprog << " -> " << sol << std::endl;
+              }
+              Assert( !exp.empty() );
+              Node exc_lem = exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp );
+              exc_lem = exc_lem.negate();
+              Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : " << exc_lem << std::endl;
+              d_qe->getOutputChannel().lemma( exc_lem );
+            }
+          }
+        }
+        if( needs_new_stream_guard ){
+          // generate a new stream guard
+          curr_stream_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G_Stream", NodeManager::currentNM()->booleanType() ) );
+          curr_stream_guard = d_qe->getValuation().ensureLiteral( curr_stream_guard );
+          AlwaysAssert( !curr_stream_guard.isNull() );
+          d_qe->getOutputChannel().requirePhase( curr_stream_guard, true );
+          d_stream_guards.push_back( curr_stream_guard );
+          Trace("cegqi-debug") << "getNextDecision : allocate new stream guard : " << curr_stream_guard << std::endl;
+          // return it as a decision
+          priority = 0;
+          return curr_stream_guard;
+        }
+      }
+    }else{
+      Trace("cegqi-debug") << "getNextDecision : conjecture is infeasible." << std::endl;
+    } 
+  }
+  return Node::null();
+}
+
+void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation ) {
+  Trace("cegqi-debug") << "Printing synth solution..." << std::endl;
+  Assert( d_quant[0].getNumChildren()==d_embed_quant[0].getNumChildren() );
+  for( unsigned i=0; i<d_embed_quant[0].getNumChildren(); i++ ){
+    Node prog = d_embed_quant[0][i];
+    Trace("cegqi-debug") << "  print solution for " << prog << std::endl;
+    std::stringstream ss;
+    ss << prog;
+    std::string f(ss.str());
+    f.erase(f.begin());
+    TypeNode tn = prog.getType();
+    Assert( tn.isDatatype() );
+    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+    Assert( dt.isSygus() );
+    //get the solution
+    Node sol;
+    int status = -1;
+    if( singleInvocation ){
+      Assert( d_ceg_si != NULL );
+      sol = d_ceg_si->getSolution( i, tn, status, true );
+      if( !sol.isNull() ){
+        sol = sol.getKind()==LAMBDA ? sol[1] : sol;
+      }
+    }else{
+      Node cprog = getCandidate( i );
+      if( !d_cinfo[cprog].d_inst.empty() ){
+        // the solution is just the last instantiated term
+        sol = d_cinfo[cprog].d_inst.back();
+        status = 1;
+        
+        //check if there was a template
+        Node sf = d_quant[0][i].getAttribute(SygusSynthFunAttribute());
+        Node templ = d_ceg_si->getTemplate( sf );
+        if( !templ.isNull() ){
+          Trace("cegqi-inv-debug") << sf << " used template : " << templ << std::endl;
+          // if it was not embedded into the grammar
+          if( !options::sygusTemplEmbedGrammar() ){
+            TNode templa = d_ceg_si->getTemplateArg( sf );
+            // make the builtin version of the full solution
+            TermDbSygus* sygusDb = d_qe->getTermDatabase()->getTermDatabaseSygus();
+            sol = sygusDb->sygusToBuiltin( sol, sol.getType() );		
+            Trace("cegqi-inv") << "Builtin version of solution is : "
+                               << sol << ", type : " << sol.getType()
+                               << std::endl;
+            TNode tsol = sol;
+            sol = templ.substitute( templa, tsol );
+            Trace("cegqi-inv-debug") << "With template : " << sol << std::endl;
+            sol = Rewriter::rewrite( sol );
+            Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl;
+            // now, reconstruct to the syntax
+            sol = d_ceg_si->reconstructToSyntax(sol, tn, status, true);
+            sol = sol.getKind()==LAMBDA ? sol[1] : sol;
+            Trace("cegqi-inv-debug") << "Reconstructed to syntax : " << sol << std::endl;
+          }else{
+            Trace("cegqi-inv-debug") << "...was embedding into grammar." << std::endl;
+          }
+        }else{
+          Trace("cegqi-inv-debug") << sf << " did not use template" << std::endl;
+        }
+      }else{
+        Trace("cegqi-warn") << "WARNING : No recorded instantiations for syntax-guided solution!" << std::endl;
+      }
+    }
+    if( !(Trace.isOn("cegqi-stats")) && !sol.isNull() ){
+      out << "(define-fun " << f << " ";
+      if( dt.getSygusVarList().isNull() ){
+        out << "() ";
+      }else{
+        out << dt.getSygusVarList() << " ";
+      }
+      out << dt.getSygusType() << " ";
+      if( status==0 ){
+        out << sol;
+      }else{
+        std::vector< Node > lvs;
+        TermDbSygus::printSygusTerm( out, sol, lvs );
+      }
+      out << ")" << std::endl;
+    }
+  }
+}
+
+}/* namespace CVC4::theory::quantifiers */
+}/* namespace CVC4::theory */
+}/* namespace CVC4 */
diff --git a/src/theory/quantifiers/ce_guided_conjecture.h b/src/theory/quantifiers/ce_guided_conjecture.h
new file mode 100644
index 000000000..1263778d3
--- /dev/null
+++ b/src/theory/quantifiers/ce_guided_conjecture.h
@@ -0,0 +1,170 @@
+/*********************                                                        */
+/*! \file ce_guided_conjecture.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 class that encapsulates counterexample-guided instantiation
+ **        techniques for a single SyGuS synthesis conjecture
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H
+#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H
+
+#include "context/cdhashmap.h"
+#include "theory/quantifiers/ce_guided_single_inv.h"
+#include "theory/quantifiers/ce_guided_pbe.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** a synthesis conjecture */
+class CegConjecture {
+public:
+  CegConjecture( QuantifiersEngine * qe );
+  ~CegConjecture();
+  /** get original version of conjecture */
+  Node getConjecture() { return d_quant; }
+  /** get deep embedding version of conjecture */
+  Node getEmbeddedConjecture() { return d_embed_quant; }
+  /** get next decision request */
+  Node getNextDecisionRequest( unsigned& priority );
+  /** increment the number of times we have successfully done candidate refinement */
+  void incrementRefineCount() { d_refine_count++; }
+  /** whether the conjecture is waiting for a call to do_Check below */
+  bool needsCheck( std::vector< Node >& lem );
+  /** whether the conjecture is waiting for a call to doRefine below */
+  bool needsRefinement();
+  /** get the list of candidates */
+  void getCandidateList( std::vector< Node >& clist, bool forceOrig = false );
+  /** do single invocation check 
+  * This updates Gamma for an iteration of step 2 of Figure 1 of Reynolds et al CAV 2015.
+  */
+  void doSingleInvCheck(std::vector< Node >& lems);
+  /** do syntax-guided enumerative check 
+  * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015.
+  */
+  void doCheck(std::vector< Node >& lems, std::vector< Node >& model_values);
+  /** do basic check 
+  * This is called for non-SyGuS synthesis conjectures
+  */
+  void doBasicCheck(std::vector< Node >& lems);
+  /** do refinement 
+  * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015.
+  */
+  void doRefine(std::vector< Node >& lems);
+  /** Print the synthesis solution
+   * singleInvocation is whether the solution was found by single invocation techniques.
+   */
+  void printSynthSolution( std::ostream& out, bool singleInvocation );
+  /** get guard, this is "G" in Figure 3 of Reynolds et al CAV 2015 */
+  Node getGuard();
+  /** is ground */
+  bool isGround() { return d_inner_vars.empty(); }
+  /** does this conjecture correspond to a syntax-guided synthesis input */
+  bool isSyntaxGuided() const { return d_syntax_guided; }
+  /** are we using single invocation techniques */
+  bool isSingleInvocation() const;
+  /** preregister conjecture 
+  * This is used as a heuristic for solution reconstruction, so that we 
+  * remember expressions in the conjecture before preprocessing, since they
+  * may be helpful during solution reconstruction (Figure 5 of Reynolds et al CAV 2015)
+  */
+  void preregisterConjecture( Node q );
+  /** assign conjecture q to this class */
+  void assign( Node q );
+  /** has a conjecture been assigned to this class */
+  bool isAssigned() { return !d_embed_quant.isNull(); }
+  /** get model values for terms n, store in vector v */
+  void getModelValues( std::vector< Node >& n, std::vector< Node >& v );
+  /** get model value for term n */
+  Node getModelValue( Node n );
+  /** get number of refinement lemmas we have added so far */
+  unsigned getNumRefinementLemmas() { return d_refinement_lemmas.size(); }
+  /** get refinement lemma */
+  Node getRefinementLemma( unsigned i ) { return d_refinement_lemmas[i]; }
+  /** get refinement lemma */
+  Node getRefinementBaseLemma( unsigned i ) { return d_refinement_lemmas_base[i]; }
+  /** print out debug information about this conjecture */
+  void debugPrint( const char * c );
+private:
+  /** reference to quantifier engine */
+  QuantifiersEngine * d_qe;
+  /** single invocation utility */
+  CegConjectureSingleInv * d_ceg_si;
+  /** program by examples utility */
+  CegConjecturePbe * d_ceg_pbe;
+  /** list of constants for quantified formula */
+  std::vector< Node > d_candidates;
+  /** base instantiation */
+  Node d_base_inst;
+  /** expand base inst to disjuncts */
+  std::vector< Node > d_base_disj;
+  /** list of variables on inner quantification */
+  std::vector< Node > d_inner_vars;
+  std::vector< std::vector< Node > > d_inner_vars_disj;
+  /** current extential quantifeirs whose couterexamples we must refine */
+  std::vector< std::vector< Node > > d_ce_sk;
+  /** refinement lemmas */
+  std::vector< Node > d_refinement_lemmas;
+  std::vector< Node > d_refinement_lemmas_base;
+  /** quantified formula asserted */
+  Node d_quant;
+  /** quantified formula (after processing) */
+  Node d_embed_quant;
+  /** candidate information */
+  class CandidateInfo {
+  public:
+    CandidateInfo(){}
+    /** list of terms we have instantiated candidates with */
+    std::vector< Node > d_inst;
+  };
+  std::map< Node, CandidateInfo > d_cinfo;  
+  /** number of times we have called doRefine */
+  unsigned d_refine_count;
+  /** convert node n based on deep embedding (Section 4 of Reynolds et al CAV 2015) */
+  Node convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars, std::map< Node, Node >& visited );
+  /** collect constants */
+  void collectConstants( Node n, std::map< TypeNode, std::vector< Node > >& consts, std::map< Node, bool >& visited );
+  /** construct candidates */
+  bool constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, 
+                            std::vector< Node >& candidate_values, std::vector< Node >& lems );
+  /** get candidadate */
+  Node getCandidate( unsigned int i ) { return d_candidates[i]; }
+  /** record instantiation (this is used to construct solutions later) */
+  void recordInstantiation( std::vector< Node >& vs ) {
+    Assert( vs.size()==d_candidates.size() );
+    for( unsigned i=0; i<vs.size(); i++ ){
+      d_cinfo[d_candidates[i]].d_inst.push_back( vs[i] );
+    }
+  }
+  //-------------------------------- sygus stream
+  /** the streaming guards for sygus streaming mode */
+  std::vector< Node > d_stream_guards;
+  /** get current stream guard */
+  Node getCurrentStreamGuard() const;
+  //-------------------------------- end sygus stream
+  //-------------------------------- non-syntax guided (deprecated)
+  /** Whether we are syntax-guided (e.g. was the input in SyGuS format).
+   * This includes SyGuS inputs where no syntactic restrictions are provided.
+   */
+  bool d_syntax_guided;
+  /** the guard for non-syntax-guided synthesis */
+  Node d_nsg_guard;
+  //-------------------------------- end non-syntax guided (deprecated)
+};
+
+} /* namespace CVC4::theory::quantifiers */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
+
+#endif
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 38247c84c..2ad55bb07 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -10,18 +10,16 @@
  ** directory for licensing information.\endverbatim
  **
  ** \brief counterexample guided instantiation class
+ **   This class is the entry point for both synthesis algorithms in Reynolds et al CAV 2015
  **
  **/
 #include "theory/quantifiers/ce_guided_instantiation.h"
 
-#include "expr/datatype.h"
 #include "options/quantifiers_options.h"
-#include "options/datatypes_options.h"
 #include "smt/smt_statistics_registry.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/term_database_sygus.h"
 #include "theory/theory_engine.h"
-#include "prop/prop_engine.h"
+#include "theory/quantifiers/term_database_sygus.h"
+//FIXME : remove this include (github issue #1156)
 #include "theory/bv/theory_bv_rewriter.h"
 
 using namespace CVC4::kind;
@@ -31,539 +29,8 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-
-CegConjecture::CegConjecture( QuantifiersEngine * qe, context::Context* c )
-    : d_qe( qe ) {
-  d_refine_count = 0;
-  d_ceg_si = new CegConjectureSingleInv( qe, this );
-  d_ceg_pbe = new CegConjecturePbe( qe, this );
-}
-
-CegConjecture::~CegConjecture() {
-  delete d_ceg_si;
-  delete d_ceg_pbe;
-}
-
-Node CegConjecture::convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars, std::map< Node, Node >& visited ){
-  std::map< Node, Node >::iterator it = visited.find( n );
-  if( it==visited.end() ){
-    Node ret = n;
-    
-    std::vector< Node > children;
-    bool childChanged = false;
-    bool madeOp = false;
-    Kind ret_k = n.getKind();
-    Node op;
-    if( n.getNumChildren()>0 ){
-      if( n.getKind()==kind::APPLY_UF ){
-        op = n.getOperator();
-      }
-    }else{
-      op = n;
-    }
-    // is it a synth function?
-    std::map< Node, Node >::iterator its = synth_fun_vars.find( op );
-    if( its!=synth_fun_vars.end() ){
-      Assert( its->second.getType().isDatatype() );
-      // make into evaluation function
-      const Datatype& dt = ((DatatypeType)its->second.getType().toType()).getDatatype();
-      Assert( dt.isSygus() );
-      children.push_back( Node::fromExpr( dt.getSygusEvaluationFunc() ) );
-      children.push_back( its->second );
-      madeOp = true;
-      childChanged = true;
-      ret_k = kind::APPLY_UF;
-    }
-    if( n.getNumChildren()>0 || childChanged ){
-      if( !madeOp ){
-        if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-          children.push_back( n.getOperator() );
-        }
-      }
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        Node nc = convertToEmbedding( n[i], synth_fun_vars, visited ); 
-        childChanged = childChanged || nc!=n[i];
-        children.push_back( nc );
-      }
-      if( childChanged ){
-        ret = NodeManager::currentNM()->mkNode( ret_k, children );
-      }
-    }
-    visited[n] = ret;
-    return ret;
-  }else{
-    return it->second;
-  }
-}
-
-void CegConjecture::collectConstants( Node n, std::map< TypeNode, std::vector< Node > >& consts, std::map< Node, bool >& visited ) {
-  if( visited.find( n )==visited.end() ){
-    visited[n] = true;
-    if( n.isConst() ){
-      TypeNode tn = n.getType();
-      Node nc = n;
-      if( tn.isReal() ){
-        nc = NodeManager::currentNM()->mkConst( n.getConst<Rational>().abs() );
-      }
-      if( std::find( consts[tn].begin(), consts[tn].end(), nc )==consts[tn].end() ){
-        Trace("cegqi-debug") << "...consider const : " << nc << std::endl;
-        consts[tn].push_back( nc );
-      }
-    }
-    
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      collectConstants( n[i], consts, visited );
-    }
-  }
-}
-
-
-void CegConjecture::assign( Node q ) {
-  Assert( d_quant.isNull() );
-  Assert( q.getKind()==FORALL );
-  Trace("cegqi") << "CegConjecture : assign : " << q << std::endl;
-  d_assert_quant = q;
-
-  //register with single invocation if applicable
-  if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){
-    d_ceg_si->initialize( d_assert_quant );
-  }
-
-  // convert to deep embedding and finalize single invocation here
-  // now, construct the grammar
-  Trace("cegqi") << "CegConjecture : convert to deep embedding..." << std::endl;
-  std::map< TypeNode, std::vector< Node > > extra_cons;
-  Trace("cegqi") << "CegConjecture : collect constants..." << std::endl;
-  if( options::sygusAddConstGrammar() ){
-    std::map< Node, bool > visited;
-    collectConstants( q[1], extra_cons, visited );
-  }
-  bool has_ites = true;
-  bool is_syntax_restricted = false;
-  std::vector< Node > qchildren;
-  std::map< Node, Node > visited;
-  std::map< Node, Node > synth_fun_vars;
-  std::vector< Node > ebvl;
-  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-    Node v = q[0][i];
-    Node sf = v.getAttribute(SygusSynthFunAttribute());
-    Assert( !sf.isNull() );
-    Node sfvl = sf.getAttribute(SygusSynthFunVarListAttribute());
-    // sfvl may be null for constant synthesis functions
-    Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " << sfvl << std::endl;
-    TypeNode tn;
-    std::stringstream ss;
-    ss << sf;
-    if( v.getType().isDatatype() && ((DatatypeType)v.getType().toType()).getDatatype().isSygus() ){
-      tn = v.getType();
-    }else{
-      // make the default grammar
-      tn = d_qe->getTermDatabaseSygus()->mkSygusDefaultType( v.getType(), sfvl, ss.str(), extra_cons );
-    }
-    // if there is a template for this argument, make a sygus type on top of it
-    Node templ = d_ceg_si->getTemplate( sf );
-    if( !templ.isNull() ){
-      Node templ_arg = d_ceg_si->getTemplateArg( sf );
-      Assert( !templ_arg.isNull() );
-      if( Trace.isOn("cegqi-debug") ){
-        Trace("cegqi-debug") << "Template for " << sf << " is : " << templ << " with arg " << templ_arg << std::endl;
-        Trace("cegqi-debug") << "  embed this template as a grammar..." << std::endl;
-      }
-      tn = d_qe->getTermDatabaseSygus()->mkSygusTemplateType( templ, templ_arg, tn, sfvl, ss.str() );
-    }
-    d_qe->getTermDatabaseSygus()->registerSygusType( tn );
-    // check grammar restrictions
-    if( !d_qe->getTermDatabaseSygus()->sygusToBuiltinType( tn ).isBoolean() ){
-      if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){
-        has_ites = false;
-      }
-    }
-    Assert( tn.isDatatype() );
-    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-    Assert( dt.isSygus() );
-    if( !dt.getSygusAllowAll() ){
-      is_syntax_restricted = true;
-    }
-
-    // ev is the first-order variable corresponding to this synth fun
-    std::stringstream ssf;
-    ssf << "f" << sf;
-    Node ev = NodeManager::currentNM()->mkBoundVar( ssf.str(), tn );
-    ebvl.push_back( ev );
-    synth_fun_vars[sf] = ev;
-    Trace("cegqi") << "...embedding synth fun : " << sf << " -> " << ev << std::endl;
-  }
-  qchildren.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, ebvl ) );
-  qchildren.push_back( convertToEmbedding( q[1], synth_fun_vars, visited ) );
-  if( q.getNumChildren()==3 ){
-    qchildren.push_back( q[2] );
-  }
-  q = NodeManager::currentNM()->mkNode( kind::FORALL, qchildren );
-  Trace("cegqi") << "CegConjecture : converted to embedding : " << q << std::endl;
-  d_quant = q;
-
-  // we now finalize the single invocation module, based on the syntax restrictions
-  if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){
-    d_ceg_si->finishInit( is_syntax_restricted, has_ites );
-  }
-
-  Assert( d_candidates.empty() );
-  std::vector< Node > vars;
-  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-    vars.push_back( q[0][i] );
-    Node e = NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() );
-    d_candidates.push_back( e );
-  }
-  Trace("cegqi") << "Base quantified formula is : " << q << std::endl;
-  //construct base instantiation
-  d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, vars, d_candidates ) );
-  
-  // register this term with sygus database
-  std::vector< Node > guarded_lemmas;
-  if( !isSingleInvocation() ){
-    if( options::sygusPbe() ){
-      d_ceg_pbe->initialize( d_base_inst, d_candidates, guarded_lemmas );
-    }
-    for( unsigned i=0; i<d_candidates.size(); i++ ){
-      Node e = d_candidates[i];
-      if( options::sygusPbe() ){
-        std::vector< std::vector< Node > > exs;
-        std::vector< Node > exos;
-        std::vector< Node > exts;
-        // use the PBE examples, regardless of the search algorith, since these help search space pruning
-        if( d_ceg_pbe->getPbeExamples( e, exs, exos, exts ) ){
-          d_qe->getTermDatabaseSygus()->registerPbeExamples( e, exs, exos, exts );
-        }
-      }else{
-        d_qe->getTermDatabaseSygus()->registerMeasuredTerm( e, e );
-      }
-    }
-  }
-  
-  Trace("cegqi") << "Base instantiation is :      " << d_base_inst << std::endl;
-  if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){
-    CegInstantiation::collectDisjuncts( d_base_inst, d_base_disj );
-    Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl;
-    //store the inner variables for each disjunct
-    for( unsigned j=0; j<d_base_disj.size(); j++ ){
-      Trace("cegqi") << "  " << j << " : " << d_base_disj[j] << std::endl;
-      d_inner_vars_disj.push_back( std::vector< Node >() );
-      //if the disjunct is an existential, store it
-      if( d_base_disj[j].getKind()==NOT && d_base_disj[j][0].getKind()==FORALL ){
-        for( unsigned k=0; k<d_base_disj[j][0][0].getNumChildren(); k++ ){
-          d_inner_vars.push_back( d_base_disj[j][0][0][k] );
-          d_inner_vars_disj[j].push_back( d_base_disj[j][0][0][k] );
-        }
-      }
-    }
-    d_syntax_guided = true;
-  }else if( d_qe->getTermDatabase()->isQAttrSynthesis( d_assert_quant ) ){
-    d_syntax_guided = false;
-  }else{
-    Assert( false );
-  }
-  
-  // initialize the guard
-  if( !d_syntax_guided ){
-    if( d_nsg_guard.isNull() ){
-      d_nsg_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
-      d_nsg_guard = d_qe->getValuation().ensureLiteral( d_nsg_guard );
-      AlwaysAssert( !d_nsg_guard.isNull() );
-      d_qe->getOutputChannel().requirePhase( d_nsg_guard, true );
-      // negated base as a guarded lemma
-      guarded_lemmas.push_back( d_base_inst.negate() );
-    }
-  }else if( d_ceg_si->d_si_guard.isNull() ){
-    std::vector< Node > lems;
-    d_ceg_si->getInitialSingleInvLemma( lems );
-    for( unsigned i=0; i<lems.size(); i++ ){
-      Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation " << i << " : " << lems[i] << std::endl;
-      d_qe->getOutputChannel().lemma( lems[i] );
-      if( Trace.isOn("cegqi-debug") ){
-        Node rlem = Rewriter::rewrite( lems[i] );
-        Trace("cegqi-debug") << "...rewritten : " << rlem << std::endl;
-      }
-    }
-  }
-  Assert( !getGuard().isNull() );
-  Node gneg = getGuard().negate();
-  for( unsigned i=0; i<guarded_lemmas.size(); i++ ){
-    Node lem = NodeManager::currentNM()->mkNode( OR, gneg, guarded_lemmas[i] );
-    Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem << std::endl;
-    d_qe->getOutputChannel().lemma( lem );
-  }
-  
-  Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() << std::endl;
-}
-
-Node CegConjecture::getGuard() {
-  return !d_syntax_guided ? d_nsg_guard : d_ceg_si->d_si_guard;
-}
-
-bool CegConjecture::isSingleInvocation() const {
-  return d_ceg_si->isSingleInvocation();
-}
-
-bool CegConjecture::needsCheck( std::vector< Node >& lem ) {
-  if( isSingleInvocation() && !d_ceg_si->needsCheck() ){
-    return false;
-  }else{
-    bool value;
-    Assert( !getGuard().isNull() );
-    // non or fully single invocation : look at guard only
-    if( d_qe->getValuation().hasSatValue( getGuard(), value ) ) {
-      if( !value ){
-        Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl;
-        return false;
-      }
-    }else{
-      Assert( false );
-    }
-
-    return true;
-  }
-}
-
-
-void CegConjecture::doCegConjectureSingleInvCheck(std::vector< Node >& lems) {
-  if( d_ceg_si!=NULL ){
-    d_ceg_si->check(lems);
-  }
-}
-
-bool CegConjecture::needsRefinement() { 
-  return !d_ce_sk.empty();
-}
-
-void CegConjecture::getCandidateList( std::vector< Node >& clist, bool forceOrig ) {
-  if( d_ceg_pbe->isPbe() && !forceOrig ){
-    //Assert( isGround() );
-    d_ceg_pbe->getCandidateList( d_candidates, clist );
-  }else{
-    clist.insert( clist.end(), d_candidates.begin(), d_candidates.end() );
-  }
-}
-
-bool CegConjecture::constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, std::vector< Node >& candidate_values, 
-                                         std::vector< Node >& lems ) {
-  Assert( clist.size()==model_values.size() );
-  if( d_ceg_pbe->isPbe() ){
-    //Assert( isGround() );
-    return d_ceg_pbe->constructCandidates( clist, model_values, d_candidates, candidate_values, lems );
-  }else{
-    Assert( model_values.size()==d_candidates.size() );
-    candidate_values.insert( candidate_values.end(), model_values.begin(), model_values.end() );
-  }
-  return true;
-}
-
-void CegConjecture::doCegConjectureCheck(std::vector< Node >& lems, std::vector< Node >& model_values) {
-  std::vector< Node > clist;
-  getCandidateList( clist );
-  std::vector< Node > c_model_values;
-  Trace("cegqi-check") << "CegConjuncture : check, build candidates..." << std::endl;
-  bool constructed_cand = constructCandidates( clist, model_values, c_model_values, lems );
-
-  //must get a counterexample to the value of the current candidate
-  Node inst;
-  if( constructed_cand ){
-    if( Trace.isOn("cegqi-check")  ){
-      Trace("cegqi-check") << "CegConjuncture : check candidate : " << std::endl;
-      for( unsigned i=0; i<c_model_values.size(); i++ ){
-        Trace("cegqi-check") << "  " << i << " : " << d_candidates[i] << " -> " << c_model_values[i] << std::endl;
-      }
-    }
-    Assert( c_model_values.size()==d_candidates.size() );
-    inst = d_base_inst.substitute( d_candidates.begin(), d_candidates.end(), c_model_values.begin(), c_model_values.end() );
-  }else{
-    inst = d_base_inst;
-  }
-  
-  //check whether we will run CEGIS on inner skolem variables
-  bool sk_refine = ( !isGround() || d_refine_count==0 ) && ( !d_ceg_pbe->isPbe() || constructed_cand );
-  if( sk_refine ){
-    Assert( d_ce_sk.empty() );
-    d_ce_sk.push_back( std::vector< Node >() );
-  }else{
-    if( !constructed_cand ){
-      return;
-    }
-  }
-  
-  std::vector< Node > ic;
-  ic.push_back( d_assert_quant.negate() );
-  std::vector< Node > d;
-  CegInstantiation::collectDisjuncts( inst, d );
-  Assert( d.size()==d_base_disj.size() );
-  //immediately skolemize inner existentials
-  for( unsigned i=0; i<d.size(); i++ ){
-    Node dr = Rewriter::rewrite( d[i] );
-    if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){
-      if( constructed_cand ){
-        ic.push_back( d_qe->getTermDatabase()->getSkolemizedBody( dr[0] ).negate() );
-      }
-      if( sk_refine ){
-        Assert( !isGround() );
-        d_ce_sk.back().push_back( dr[0] );
-      }
-    }else{
-      if( constructed_cand ){
-        ic.push_back( dr );
-        if( !d_inner_vars_disj[i].empty() ){
-          Trace("cegqi-debug") << "*** quantified disjunct : " << d[i] << " simplifies to " << dr << std::endl;
-        }
-      }
-      if( sk_refine ){
-        d_ce_sk.back().push_back( Node::null() );
-      }
-    }
-  }
-  if( constructed_cand ){
-    Node lem = NodeManager::currentNM()->mkNode( OR, ic );
-    lem = Rewriter::rewrite( lem );
-    //eagerly unfold applications of evaluation function
-    if( options::sygusDirectEval() ){
-      Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl;
-      std::map< Node, Node > visited_n;
-      lem = d_qe->getTermDatabaseSygus()->getEagerUnfold( lem, visited_n );
-    }
-    lems.push_back( lem );
-    recordInstantiation( c_model_values );
-  }
-}
-        
-void CegConjecture::doCegConjectureRefine( std::vector< Node >& lems ){
-  Assert( lems.empty() );
-  Assert( d_ce_sk.size()==1 );
-
-  //first, make skolem substitution
-  Trace("cegqi-refine") << "doCegConjectureRefine : construct skolem substitution..." << std::endl;
-  std::vector< Node > sk_vars;
-  std::vector< Node > sk_subs;
-  //collect the substitution over all disjuncts
-  for( unsigned k=0; k<d_ce_sk[0].size(); k++ ){
-    Node ce_q = d_ce_sk[0][k];
-    if( !ce_q.isNull() ){
-      Assert( !d_inner_vars_disj[k].empty() );
-      Assert( d_inner_vars_disj[k].size()==d_qe->getTermDatabase()->d_skolem_constants[ce_q].size() );
-      std::vector< Node > model_values;
-      getModelValues( d_qe->getTermDatabase()->d_skolem_constants[ce_q], model_values );
-      sk_vars.insert( sk_vars.end(), d_inner_vars_disj[k].begin(), d_inner_vars_disj[k].end() );
-      sk_subs.insert( sk_subs.end(), model_values.begin(), model_values.end() );
-    }else{
-      if( !d_inner_vars_disj[k].empty() ){
-        //denegrate case : quantified disjunct was trivially true and does not need to be refined
-        //add trivial substitution (in case we need substitution for previous cex's)
-        for( unsigned i=0; i<d_inner_vars_disj[k].size(); i++ ){
-          sk_vars.push_back( d_inner_vars_disj[k][i] );
-          sk_subs.push_back( getModelValue( d_inner_vars_disj[k][i] ) ); // will return dummy value
-        }
-      }
-    }
-  }
-  
-  std::map< Node, Node > csol_active;
-  std::map< Node, std::vector< Node > > csol_ccond_nodes;
-  std::map< Node, std::map< Node, bool > > csol_cpol;    
-  
-  //for conditional evaluation
-  std::map< Node, Node > psubs_visited;
-  std::map< Node, Node > psubs;
-  std::vector< Node > lem_c;
-  Assert( d_ce_sk[0].size()==d_base_disj.size() );
-  std::vector< Node > inst_cond_c;
-  Trace("cegqi-refine") << "doCegConjectureRefine : Construct refinement lemma..." << std::endl;
-  for( unsigned k=0; k<d_ce_sk[0].size(); k++ ){
-    Node ce_q = d_ce_sk[0][k];
-    Trace("cegqi-refine-debug") << "  For counterexample point, disjunct " << k << " : " << ce_q << " " << d_base_disj[k] << std::endl;
-    Node c_disj;
-    if( !ce_q.isNull() ){
-      Assert( d_base_disj[k].getKind()==kind::NOT && d_base_disj[k][0].getKind()==kind::FORALL );
-      c_disj = d_base_disj[k][0][1];
-    }else{
-      if( d_inner_vars_disj[k].empty() ){
-        c_disj = d_base_disj[k].negate();
-      }else{
-        //denegrate case : quantified disjunct was trivially true and does not need to be refined
-        Trace("cegqi-refine-debug") << "*** skip " << d_base_disj[k] << std::endl;
-      }
-    }
-    if( !c_disj.isNull() ){
-      //compute the body, inst_cond
-      //standard CEGIS refinement : plug in values, assert that d_candidates must satisfy entire specification
-      lem_c.push_back( c_disj );
-    }
-  }
-  Assert( sk_vars.size()==sk_subs.size() );
-  //add conditional correctness assumptions
-  std::vector< Node > psubs_cond_ant;
-  std::vector< Node > psubs_cond_conc;
-  std::map< Node, std::vector< Node > > psubs_apply;
-  std::vector< Node > paux_vars;
-  Assert( psubs.empty() );
-  
-  Node base_lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c );
-  
-  Trace("cegqi-refine") << "doCegConjectureRefine : construct and finalize lemmas..." << std::endl;
-  
-  Node lem = base_lem;
-  
-  base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
-  base_lem = Rewriter::rewrite( base_lem );
-  d_refinement_lemmas_base.push_back( base_lem );
-  
-  lem = NodeManager::currentNM()->mkNode( OR, getGuard().negate(), lem );
-  
-  lem = lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() );
-  lem = Rewriter::rewrite( lem );
-  d_refinement_lemmas.push_back( lem );
-  lems.push_back( lem );
-
-  d_ce_sk.clear();
-}
-
-void CegConjecture::preregisterConjecture( Node q ) {
-  d_ceg_si->preregisterConjecture( q );
-}
-
-void CegConjecture::getModelValues( std::vector< Node >& n, std::vector< Node >& v ) {
-  Trace("cegqi-engine") << "  * Value is : ";
-  for( unsigned i=0; i<n.size(); i++ ){
-    Node nv = getModelValue( n[i] );
-    v.push_back( nv );
-    if( Trace.isOn("cegqi-engine") ){
-      TypeNode tn = nv.getType();
-      Trace("cegqi-engine") << n[i] << " -> ";
-      std::stringstream ss;
-      std::vector< Node > lvs;
-      TermDbSygus::printSygusTerm( ss, nv, lvs );
-      Trace("cegqi-engine") << ss.str() << " ";
-    }
-    Assert( !nv.isNull() );
-  }
-  Trace("cegqi-engine") << std::endl;
-}
-
-Node CegConjecture::getModelValue( Node n ) {
-  Trace("cegqi-mv") << "getModelValue for : " << n << std::endl;
-  return d_qe->getModel()->getValue( n );
-}
-
-void CegConjecture::debugPrint( const char * c ) {
-  Trace(c) << "Synthesis conjecture : " << d_quant << std::endl;
-  Trace(c) << "  * Candidate program/output symbol : ";
-  for( unsigned i=0; i<d_candidates.size(); i++ ){
-    Trace(c) << d_candidates[i] << " ";
-  }
-  Trace(c) << std::endl;
-  Trace(c) << "  * Candidate ce skolems : ";
-  for( unsigned i=0; i<d_ce_sk.size(); i++ ){
-    Trace(c) << d_ce_sk[i] << " ";
-  }
-}
-
 CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){
-  d_conj = new CegConjecture( qe, qe->getSatContext() );
+  d_conj = new CegConjecture( qe );
   d_last_inst_si = false;
 }
 
@@ -576,19 +43,17 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) {
 }
 
 unsigned CegInstantiation::needsModel( Theory::Effort e ) {
-  return d_conj->getCegConjectureSingleInv()->isSingleInvocation()
-      ? QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL;
+  return d_conj->isSingleInvocation() ? QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL;
 }
 
 void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
-  unsigned echeck = d_conj->getCegConjectureSingleInv()->isSingleInvocation() ?
-      QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL;
+  unsigned echeck = d_conj->isSingleInvocation() ? QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL;
   if( quant_e==echeck ){
     Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl;
     Trace("cegqi-engine-debug") << std::endl;
     bool active = false;
     bool value;
-    if( d_quantEngine->getValuation().hasSatValue( d_conj->d_assert_quant, value ) ) {
+    if( d_quantEngine->getValuation().hasSatValue( d_conj->getConjecture(), value ) ) {
       active = value;
     }else{
       Trace("cegqi-engine-debug") << "...no value for quantified formula." << std::endl;
@@ -608,83 +73,33 @@ void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
   }
 }
 
-void CegInstantiation::preRegisterQuantifier( Node q ) {
-/*
-  if( options::sygusDirectEval() ){
-    if( q.getNumChildren()==3 && q[2].getKind()==INST_PATTERN_LIST && q[2][0].getKind()==INST_PATTERN ){  
-      //check whether it is an evaluation axiom
-      Node pat = q[2][0][0];
-      if( pat.getKind()==APPLY_UF ){
-        TypeNode tn = pat[0].getType();
-        if( tn.isDatatype() ){
-          const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-          if( dt.isSygus() ){
-            //do unfolding if it induces Boolean structure, 
-            //do direct evaluation if it does not induce Boolean structure,
-            //  the reasoning is unfolding over these terms does not lead to helpful conflict analysis, and introduces many shared terms
-            bool directEval = true;
-            TypeNode ptn = pat.getType();
-            if( ptn.isBoolean() ){
-              directEval = false;
-            }else{
-              unsigned cindex = Datatype::indexOf(pat[0].getOperator().toExpr() );
-              Node base = d_quantEngine->getTermDatabaseSygus()->getGenericBase( tn, dt, cindex );
-              Trace("cegqi-debug") << "Generic base term for " << pat[0] << " is " << base << std::endl;
-              if( base.getKind()==ITE ){
-                directEval = false;
-              }
-            }
-            if( directEval ){
-              //take ownership of this quantified formula (will use direct evaluation instead of unfolding instantiation)
-              d_quantEngine->setOwner( q, this );
-              d_eval_axioms[q] = true;
-            }
-          }
-        }
-      }
-    }
-  } 
-  */ 
-}
-
 void CegInstantiation::registerQuantifier( Node q ) {
   if( d_quantEngine->getOwner( q )==this ){ // && d_eval_axioms.find( q )==d_eval_axioms.end() ){
     if( !d_conj->isAssigned() ){
       Trace("cegqi") << "Register conjecture : " << q << std::endl;
       d_conj->assign( q );
     }else{
-      Assert( d_conj->d_quant==q );
+      Assert( d_conj->getEmbeddedConjecture()==q );
     }
   }else{
     Trace("cegqi-debug") << "Register quantifier : " << q << std::endl;
   }
 }
 
-void CegInstantiation::assertNode( Node n ) {
-}
-
 Node CegInstantiation::getNextDecisionRequest( unsigned& priority ) {
   if( d_conj->isAssigned() ){
-    std::vector< Node > req_dec;
-    req_dec.push_back( d_conj->getGuard() );
-    // other decision requests should ask the conjecture
-    for( unsigned i=0; i<req_dec.size(); i++ ){
-      bool value;
-      if( !d_quantEngine->getValuation().hasSatValue( req_dec[i], value ) ) {
-        Trace("cegqi-debug") << "CEGQI : Decide next on : " << req_dec[i] << "..." << std::endl;
-        priority = 0;
-        return req_dec[i];
-      }else{
-        Trace("cegqi-debug2") << "CEGQI : " << req_dec[i] << " already has value " << value << std::endl;
-      }
+    Node dec_req = d_conj->getNextDecisionRequest( priority );
+    if( !dec_req.isNull() ){
+      Trace("cegqi-debug") << "CEGQI : Decide next on : " << dec_req << "..." << std::endl;
+      return dec_req;
     }
   }
   return Node::null();
 }
 
 void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
-  Node q = conj->d_quant;
-  Node aq = conj->d_assert_quant;
+  Node q = conj->getEmbeddedConjecture();
+  Node aq = conj->getConjecture();
   if( Trace.isOn("cegqi-engine-debug") ){
     conj->debugPrint("cegqi-engine-debug");
     Trace("cegqi-engine-debug") << std::endl;
@@ -692,9 +107,9 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
 
   if( !conj->needsRefinement() ){
     Trace("cegqi-engine-debug") << "Do conjecture check..." << std::endl;
-    if( conj->d_syntax_guided ){
+    if( conj->isSyntaxGuided() ){
       std::vector< Node > clems;
-      conj->doCegConjectureSingleInvCheck( clems );
+      conj->doSingleInvCheck( clems );
       if( !clems.empty() ){
         d_last_inst_si = true;
         for( unsigned j=0; j<clems.size(); j++ ){
@@ -743,7 +158,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
           for( unsigned j=0; j<eager_terms.size(); j++ ){
             Node lem = NodeManager::currentNM()->mkNode( kind::OR, eager_exps[j].negate(), eager_terms[j].eqNode( eager_vals[j] ) );
             if( d_quantEngine->getTheoryEngine()->isTheoryEnabled(THEORY_BV) ){
-              //FIXME: hack to incorporate hacks from BV for division by zero
+              //FIXME: hack to incorporate hacks from BV for division by zero (github issue #1156)
               lem = bv::TheoryBVRewriter::eliminateBVSDiv( lem );
             }
             if( d_quantEngine->addLemma( lem ) ){
@@ -759,7 +174,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
       
       Trace("cegqi-engine") << "  *** Check candidate phase..." << std::endl;
       std::vector< Node > cclems;
-      conj->doCegConjectureCheck( cclems, model_values );
+      conj->doCheck( cclems, model_values );
       bool addedLemma = false;
       for( unsigned i=0; i<cclems.size(); i++ ){
         Node lem = cclems[i];
@@ -788,21 +203,15 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
       } 
     }else{
       Assert( aq==q );
-      std::vector< Node > model_terms;
-      std::vector< Node > clist;
-      conj->getCandidateList( clist, true );
-      Assert( clist.size()==q[0].getNumChildren() );
-      conj->getModelValues( clist, model_terms );
-      if( d_quantEngine->addInstantiation( q, model_terms ) ){
-        conj->recordInstantiation( model_terms );
-      }else{
-        Assert( false );
-      }
+      Trace("cegqi-engine") << "  *** Check candidate phase (non-SyGuS)." << std::endl;
+      std::vector< Node > lems;
+      conj->doBasicCheck(lems);
+      Assert(lems.empty());
     }
   }else{
     Trace("cegqi-engine") << "  *** Refine candidate phase..." << std::endl;
     std::vector< Node > rlems;
-    conj->doCegConjectureRefine( rlems );
+    conj->doRefine( rlems );
     bool addedLemma = false;
     for( unsigned i=0; i<rlems.size(); i++ ){
       Node lem = rlems[i];
@@ -810,7 +219,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
       bool res = d_quantEngine->addLemma( lem );
       if( res ){
         ++(d_statistics.d_cegqi_lemmas_refine);
-        conj->d_refine_count++;
+        conj->incrementRefineCount();
         addedLemma = true;
       }else{
         Trace("cegqi-warn") << "  ...FAILED to add refinement!" << std::endl;
@@ -890,94 +299,13 @@ void CegInstantiation::getCRefEvaluationLemmas( CegConjecture * conj, std::vecto
 
 void CegInstantiation::printSynthSolution( std::ostream& out ) {
   if( d_conj->isAssigned() ){
-    Trace("cegqi-debug") << "Printing synth solution..." << std::endl;
-    //if( !(Trace.isOn("cegqi-stats")) ){
-    //  out << "Solution:" << std::endl;
-    //}
-    for( unsigned i=0; i<d_conj->d_quant[0].getNumChildren(); i++ ){
-      Node prog = d_conj->d_quant[0][i];
-      Trace("cegqi-debug") << "  print solution for " << prog << std::endl;
-      std::stringstream ss;
-      ss << prog;
-      std::string f(ss.str());
-      f.erase(f.begin());
-      TypeNode tn = prog.getType();
-      Assert( tn.isDatatype() );
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      Assert( dt.isSygus() );
-      //get the solution
-      Node sol;
-      int status = -1;
-      if( d_last_inst_si ){
-        Assert( d_conj->getCegConjectureSingleInv() != NULL );
-        sol = d_conj->getSingleInvocationSolution( i, tn, status );
-        if( !sol.isNull() ){
-          sol = sol.getKind()==LAMBDA ? sol[1] : sol;
-        }
-      }else{
-        Node cprog = d_conj->getCandidate( i );
-        if( !d_conj->d_cinfo[cprog].d_inst.empty() ){
-          sol = d_conj->d_cinfo[cprog].d_inst.back();
-          // Check if this was based on a template, if so, we must do
-          // Reconstruction
-          if( d_conj->d_assert_quant!=d_conj->d_quant ){
-            Node sygus_sol = sol;
-            Trace("cegqi-inv") << "Sygus version of solution is : " << sol
-                               << ", type : " << sol.getType() << std::endl;
-            std::vector< Node > subs;
-            Expr svl = dt.getSygusVarList();
-            for( unsigned j=0; j<svl.getNumChildren(); j++ ){
-              subs.push_back( Node::fromExpr( svl[j] ) );
-            }
-            if( sol==sygus_sol ){
-              sol = sygus_sol;
-              status = 1;
-            }else{
-              Trace("cegqi-inv-debug") << "With template : " << sol << std::endl;
-              sol = Rewriter::rewrite( sol );
-              Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl;
-              sol = d_conj->reconstructToSyntaxSingleInvocation(sol, tn, status);
-              sol = sol.getKind()==LAMBDA ? sol[1] : sol;
-            }
-          }else{
-            status = 1;
-          }
-        }else{
-          Trace("cegqi-warn") << "WARNING : No recorded instantiations for syntax-guided solution!" << std::endl;
-        }
-      }
-      if( !(Trace.isOn("cegqi-stats")) && !sol.isNull() ){
-        out << "(define-fun " << f << " ";
-        if( dt.getSygusVarList().isNull() ){
-          out << "() ";
-        }else{
-          out << dt.getSygusVarList() << " ";
-        }
-        out << dt.getSygusType() << " ";
-        if( status==0 ){
-          out << sol;
-        }else{
-          std::vector< Node > lvs;
-          TermDbSygus::printSygusTerm( out, sol, lvs );
-        }
-        out << ")" << std::endl;
-      }
-    }
+    // print the conjecture
+    d_conj->printSynthSolution( out, d_last_inst_si );
   }else{
     Assert( false );
   }
 }
 
-void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) {
-  if( n.getKind()==OR ){
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      collectDisjuncts( n[i], d );
-    }
-  }else{
-    d.push_back( n );
-  }
-}
-
 void CegInstantiation::preregisterAssertion( Node n ) {
   //check if it sygus conjecture
   if( TermDb::isSygusConjecture( n ) ){
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index fd34fc028..5e6cb3864 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -17,137 +17,14 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H
 #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H
 
-#include "context/cdchunk_list.h"
 #include "context/cdhashmap.h"
-#include "options/quantifiers_modes.h"
-#include "options/datatypes_modes.h"
-#include "theory/quantifiers/ce_guided_single_inv.h"
-#include "theory/quantifiers/ce_guided_pbe.h"
+#include "theory/quantifiers/ce_guided_conjecture.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-/** a synthesis conjecture */
-class CegConjecture {
-private:
-  QuantifiersEngine * d_qe;
-  /** list of constants for quantified formula */
-  std::vector< Node > d_candidates;
-  /** base instantiation */
-  Node d_base_inst;
-  /** expand base inst to disjuncts */
-  std::vector< Node > d_base_disj;
-  /** list of variables on inner quantification */
-  std::vector< Node > d_inner_vars;
-  std::vector< std::vector< Node > > d_inner_vars_disj;
-  /** current extential quantifeirs whose couterexamples we must refine */
-  std::vector< std::vector< Node > > d_ce_sk;
-  /** refinement lemmas */
-  std::vector< Node > d_refinement_lemmas;
-  std::vector< Node > d_refinement_lemmas_base;
-private:
-  /** get embedding */
-  Node convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars, std::map< Node, Node >& visited );
-  /** collect constants */
-  void collectConstants( Node n, std::map< TypeNode, std::vector< Node > >& consts, std::map< Node, bool >& visited );
-public:
-  CegConjecture( QuantifiersEngine * qe, context::Context* c );
-  ~CegConjecture();
-
-  /** quantified formula asserted */
-  Node d_assert_quant;
-  /** quantified formula (after processing) */
-  Node d_quant;
-
-  class CandidateInfo {
-  public:
-    CandidateInfo(){}
-    /** list of terms we have instantiated candidates with */
-    std::vector< Node > d_inst;
-  };
-  std::map< Node, CandidateInfo > d_cinfo;
-  
-  /** measure sum size */
-  int d_measure_term_size;
-  /** refine count */
-  unsigned d_refine_count;
-
-  const CegConjectureSingleInv* getCegConjectureSingleInv() const {
-    return d_ceg_si;
-  }
-  
-  bool needsRefinement();
-  void getCandidateList( std::vector< Node >& clist, bool forceOrig = false );
-  bool constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, 
-                            std::vector< Node >& candidate_values, std::vector< Node >& lems );
-
-  void doCegConjectureSingleInvCheck(std::vector< Node >& lems);
-  void doCegConjectureCheck(std::vector< Node >& lems, std::vector< Node >& model_values);
-  void doCegConjectureRefine(std::vector< Node >& lems);
-
-  Node getSingleInvocationSolution(unsigned sol_index, TypeNode stn,
-                                   int& reconstructed, bool rconsSygus=true){
-    return d_ceg_si->getSolution(sol_index, stn, reconstructed, rconsSygus);
-  }
-
-  Node reconstructToSyntaxSingleInvocation(
-      Node s, TypeNode stn, int& reconstructed, bool rconsSygus = true ) {
-    return d_ceg_si->reconstructToSyntax(s, stn, reconstructed, rconsSygus);
-  }
-
-  void recordInstantiation( std::vector< Node >& vs ) {
-    Assert( vs.size()==d_candidates.size() );
-    for( unsigned i=0; i<vs.size(); i++ ){
-      d_cinfo[d_candidates[i]].d_inst.push_back( vs[i] );
-    }
-  }
-  Node getCandidate( unsigned int i ) { return d_candidates[i]; }
-  
-  void debugPrint( const char * c );
-
-private:
-  /** single invocation utility */
-  CegConjectureSingleInv * d_ceg_si;
-  /** program by examples utility */
-  CegConjecturePbe * d_ceg_pbe;
-public: //non-syntax guided (deprecated)
-  /** guard */
-  bool d_syntax_guided;
-  Node d_nsg_guard;
-public:
-  /** get guard */
-  Node getGuard();
-  /** is ground */
-  bool isGround() { return d_inner_vars.empty(); }
-  /** fairness */
-  SygusFairMode getCegqiFairMode();
-  /** is single invocation */
-  bool isSingleInvocation() const;
-  /** is single invocation */
-  bool isFullySingleInvocation();
-  /** needs check */
-  bool needsCheck( std::vector< Node >& lem );
-  /** preregister conjecture */
-  void preregisterConjecture( Node q );
-  /** assign */
-  void assign( Node q );
-  /** is assigned */
-  bool isAssigned() { return !d_quant.isNull(); }
-  /** get model values */
-  void getModelValues( std::vector< Node >& n, std::vector< Node >& v );
-  /** get model value */
-  Node getModelValue( Node n );
-  /** get number of refinement lemmas */
-  unsigned getNumRefinementLemmas() { return d_refinement_lemmas.size(); }
-  /** get refinement lemma */
-  Node getRefinementLemma( unsigned i ) { return d_refinement_lemmas[i]; }
-  /** get refinement lemma */
-  Node getRefinementBaseLemma( unsigned i ) { return d_refinement_lemmas_base[i]; }
-};
-
-
 class CegInstantiation : public QuantifiersModule
 {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
@@ -156,8 +33,6 @@ private:
   CegConjecture * d_conj;
   /** last instantiation by single invocation module? */
   bool d_last_inst_si;
-  /** evaluation axioms */
-  //std::map< Node, bool > d_eval_axioms;
 private: //for direct evaluation
   /** get refinement evaluation */
   void getCRefEvaluationLemmas( CegConjecture * conj, std::vector< Node >& vs, std::vector< Node >& ms, std::vector< Node >& lems );
@@ -173,16 +48,13 @@ public:
   /* Call during quantifier engine's check */
   void check( Theory::Effort e, unsigned quant_e );
   /* Called for new quantifiers */
-  void preRegisterQuantifier( Node q );
   void registerQuantifier( Node q );
-  void assertNode( Node n );
+  /** get the next decision request */
   Node getNextDecisionRequest( unsigned& priority );
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   std::string identify() const { return "CegInstantiation"; }
   /** print solution for synthesis conjectures */
   void printSynthSolution( std::ostream& out );
-  /** collect disjuncts */
-  static void collectDisjuncts( Node n, std::vector< Node >& ex );
   /** preregister assertion (before rewrite) */
   void preregisterAssertion( Node n );
 public:
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 2fa993b97..edd9c4fa3 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -119,6 +119,8 @@ void CegConjectureSingleInv::initialize( Node q ) {
   // can only register one quantified formula with this
   Assert( d_quant.isNull() );
   d_quant = q;
+  d_simp_quant = q;
+  Trace("cegqi-si") << "CegConjectureSingleInv::initialize : " << q << std::endl;
   // infer single invocation-ness
   std::vector< Node > progs;
   std::map< Node, std::vector< Node > > prog_vars;
@@ -140,112 +142,131 @@ void CegConjectureSingleInv::initialize( Node q ) {
       qq = TermDb::simpleNegate( q[1] );
     }
     //process the single invocation-ness of the property
-    d_sip->init( progs, qq );
-    Trace("cegqi-si") << "- Partitioned to single invocation parts : " << std::endl;
-    d_sip->debugPrint( "cegqi-si" );
-
-    //map from program to bound variables
-    std::vector< Node > order_vars;
-    std::map< Node, Node > single_inv_app_map;
-    for( unsigned j=0; j<progs.size(); j++ ){
-      Node prog = progs[j];
-      std::map< Node, Node >::iterator it_fov = d_sip->d_func_fo_var.find( prog );
-      if( it_fov!=d_sip->d_func_fo_var.end() ){
-        Node pv = it_fov->second;
-        Assert( d_sip->d_func_inv.find( prog )!=d_sip->d_func_inv.end() );
-        Node inv = d_sip->d_func_inv[prog];
-        single_inv_app_map[prog] = inv;
-        Trace("cegqi-si") << "  " << pv << ", " << inv << " is associated with program " << prog << std::endl;
-        d_prog_to_sol_index[prog] = order_vars.size();
-        order_vars.push_back( pv );
-      }else{
-        Trace("cegqi-si") << "  " << prog << " has no fo var." << std::endl;
+    if( !d_sip->init( progs, qq ) ){
+      Trace("cegqi-si") << "...not single invocation (type mismatch)" << std::endl;
+    }else{
+      Trace("cegqi-si") << "- Partitioned to single invocation parts : " << std::endl;
+      d_sip->debugPrint( "cegqi-si" );
+
+      //map from program to bound variables
+      std::vector< Node > order_vars;
+      std::map< Node, Node > single_inv_app_map;
+      for( unsigned j=0; j<progs.size(); j++ ){
+        Node prog = progs[j];
+        std::map< Node, Node >::iterator it_fov = d_sip->d_func_fo_var.find( prog );
+        if( it_fov!=d_sip->d_func_fo_var.end() ){
+          Node pv = it_fov->second;
+          Assert( d_sip->d_func_inv.find( prog )!=d_sip->d_func_inv.end() );
+          Node inv = d_sip->d_func_inv[prog];
+          single_inv_app_map[prog] = inv;
+          Trace("cegqi-si") << "  " << pv << ", " << inv << " is associated with program " << prog << std::endl;
+          d_prog_to_sol_index[prog] = order_vars.size();
+          order_vars.push_back( pv );
+        }else{
+          Trace("cegqi-si") << "  " << prog << " has no fo var." << std::endl;
+        }
       }
-    }
-    //reorder the variables
-    Assert( d_sip->d_func_vars.size()==order_vars.size() );
-    d_sip->d_func_vars.clear();
-    d_sip->d_func_vars.insert( d_sip->d_func_vars.begin(), order_vars.begin(), order_vars.end() );
-
-
-    //check if it is single invocation
-    if( !d_sip->d_conjuncts[1].empty() ){
-      if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){
-        //if we are doing invariant templates, then construct the template
-        Trace("cegqi-si") << "- Do transition inference..." << std::endl;
-        d_ti[q].process( qq );
-        Trace("cegqi-inv") << std::endl;
-        if( !d_ti[q].d_func.isNull() ){
-          // map the program back via non-single invocation map
-          Node prog = d_ti[q].d_func;
-          std::vector< Node > prog_templ_vars;
-          prog_templ_vars.insert( prog_templ_vars.end(), d_ti[q].d_vars.begin(), d_ti[q].d_vars.end() );
-          d_trans_pre[prog] = d_ti[q].getComponent( 1 );
-          d_trans_post[prog] = d_ti[q].getComponent( -1 );
-          Trace("cegqi-inv") << "   precondition : " << d_trans_pre[prog] << std::endl;
-          Trace("cegqi-inv") << "  postcondition : " << d_trans_post[prog] << std::endl;
-          Node invariant = single_inv_app_map[prog];
-          invariant = invariant.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), prog_templ_vars.begin(), prog_templ_vars.end() );
-          Trace("cegqi-inv") << "      invariant : " << invariant << std::endl;
-
-          //construct template argument
-          d_templ_arg[prog] = NodeManager::currentNM()->mkSkolem( "I", invariant.getType() );
-          
-          //construct template
-          Node templ;
-          if( options::sygusInvAutoUnfold() ){
-            if( d_ti[q].isComplete() ){
-              Trace("cegqi-inv-auto-unfold") << "Automatic deterministic unfolding... " << std::endl;
-              // auto-unfold
-              DetTrace dt;
-              int init_dt = d_ti[q].initializeTrace( dt );
-              if( init_dt==0 ){
-                Trace("cegqi-inv-auto-unfold") << "  Init : ";
-                dt.print("cegqi-inv-auto-unfold");
-                Trace("cegqi-inv-auto-unfold") << std::endl;
-                unsigned counter = 0;
-                unsigned status = 0;
-                while( counter<100 && status==0 ){
-                  status = d_ti[q].incrementTrace( dt );
-                  counter++;
-                  Trace("cegqi-inv-auto-unfold") << "  #" << counter << " : ";
+      //reorder the variables
+      Assert( d_sip->d_func_vars.size()==order_vars.size() );
+      d_sip->d_func_vars.clear();
+      d_sip->d_func_vars.insert( d_sip->d_func_vars.begin(), order_vars.begin(), order_vars.end() );
+      
+
+      //check if it is single invocation
+      if( !d_sip->d_conjuncts[1].empty() ){
+        if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){
+          //if we are doing invariant templates, then construct the template
+          Trace("cegqi-si") << "- Do transition inference..." << std::endl;
+          d_ti[q].process( qq );
+          Trace("cegqi-inv") << std::endl;
+          if( !d_ti[q].d_func.isNull() ){
+            // map the program back via non-single invocation map
+            Node prog = d_ti[q].d_func;
+            std::vector< Node > prog_templ_vars;
+            prog_templ_vars.insert( prog_templ_vars.end(), d_ti[q].d_vars.begin(), d_ti[q].d_vars.end() );
+            d_trans_pre[prog] = d_ti[q].getComponent( 1 );
+            d_trans_post[prog] = d_ti[q].getComponent( -1 );
+            Trace("cegqi-inv") << "   precondition : " << d_trans_pre[prog] << std::endl;
+            Trace("cegqi-inv") << "  postcondition : " << d_trans_post[prog] << std::endl;
+            Node invariant = single_inv_app_map[prog];
+            invariant = invariant.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), prog_templ_vars.begin(), prog_templ_vars.end() );
+            Trace("cegqi-inv") << "      invariant : " << invariant << std::endl;
+            
+            // store simplified version of quantified formula
+            d_simp_quant = d_sip->d_conjuncts[2].size()==1 ? d_sip->d_conjuncts[2][0] : NodeManager::currentNM()->mkNode( AND, d_sip->d_conjuncts[2] );
+            std::vector< Node > new_bv;
+            for( unsigned j=0; j<d_sip->d_si_vars.size(); j++ ){
+              new_bv.push_back( NodeManager::currentNM()->mkBoundVar( d_sip->d_si_vars[j].getType() ) );
+            }
+            d_simp_quant = d_simp_quant.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), new_bv.begin(), new_bv.end() );
+            Assert( q[1].getKind()==NOT && q[1][0].getKind()==FORALL );
+            for( unsigned j=0; j<q[1][0][0].getNumChildren(); j++ ){
+              new_bv.push_back( q[1][0][0][j] );
+            }
+            d_simp_quant = NodeManager::currentNM()->mkNode( kind::FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, new_bv ), d_simp_quant ).negate();
+            d_simp_quant = Rewriter::rewrite( d_simp_quant );
+            d_simp_quant = NodeManager::currentNM()->mkNode( kind::FORALL, q[0], d_simp_quant, q[2] );
+            Trace("cegqi-si") << "Rewritten quantifier : " << d_simp_quant << std::endl;
+
+            //construct template argument
+            d_templ_arg[prog] = NodeManager::currentNM()->mkSkolem( "I", invariant.getType() );
+            
+            //construct template
+            Node templ;
+            if( options::sygusInvAutoUnfold() ){
+              if( d_ti[q].isComplete() ){
+                Trace("cegqi-inv-auto-unfold") << "Automatic deterministic unfolding... " << std::endl;
+                // auto-unfold
+                DetTrace dt;
+                int init_dt = d_ti[q].initializeTrace( dt );
+                if( init_dt==0 ){
+                  Trace("cegqi-inv-auto-unfold") << "  Init : ";
                   dt.print("cegqi-inv-auto-unfold");
-                  Trace("cegqi-inv-auto-unfold") << "...status = " << status << std::endl;
-                }
-                if( status==1 ){
-                  // we have a trivial invariant
-                  templ = d_ti[q].constructFormulaTrace( dt );
-                  Trace("cegqi-inv") << "By finite deterministic terminating trace, a solution invariant is : " << std::endl;
-                  Trace("cegqi-inv") << "   " << templ << std::endl;
-                  // FIXME : this should be unnecessary
-                  templ = NodeManager::currentNM()->mkNode( AND, templ, d_templ_arg[prog] );
+                  Trace("cegqi-inv-auto-unfold") << std::endl;
+                  unsigned counter = 0;
+                  unsigned status = 0;
+                  while( counter<100 && status==0 ){
+                    status = d_ti[q].incrementTrace( dt );
+                    counter++;
+                    Trace("cegqi-inv-auto-unfold") << "  #" << counter << " : ";
+                    dt.print("cegqi-inv-auto-unfold");
+                    Trace("cegqi-inv-auto-unfold") << "...status = " << status << std::endl;
+                  }
+                  if( status==1 ){
+                    // we have a trivial invariant
+                    templ = d_ti[q].constructFormulaTrace( dt );
+                    Trace("cegqi-inv") << "By finite deterministic terminating trace, a solution invariant is : " << std::endl;
+                    Trace("cegqi-inv") << "   " << templ << std::endl;
+                    // FIXME : this should be unnecessary
+                    templ = NodeManager::currentNM()->mkNode( AND, templ, d_templ_arg[prog] );
+                  }
+                }else{
+                  Trace("cegqi-inv-auto-unfold") << "...failed initialize." << std::endl;
                 }
-              }else{
-                Trace("cegqi-inv-auto-unfold") << "...failed initialize." << std::endl;
               }
             }
-          }
-          if( templ.isNull() ){
-            if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){
-              //d_templ[prog] = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant ), d_trans_post[prog] );
-              templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], d_templ_arg[prog] );
-            }else{
-              Assert( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST );
-              //d_templ[prog] = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant ) );
-              templ = NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], d_templ_arg[prog] );
+            if( templ.isNull() ){
+              if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){
+                //d_templ[prog] = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant ), d_trans_post[prog] );
+                templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], d_templ_arg[prog] );
+              }else{
+                Assert( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST );
+                //d_templ[prog] = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant ) );
+                templ = NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], d_templ_arg[prog] );
+              }
             }
+            Trace("cegqi-inv") << "       template (pre-substitution) : " << templ << std::endl;
+            Assert( !templ.isNull() );
+            // subsitute the template arguments
+            templ = templ.substitute( prog_templ_vars.begin(), prog_templ_vars.end(), prog_vars[prog].begin(), prog_vars[prog].end() );
+            Trace("cegqi-inv") << "       template : " << templ << std::endl;
+            d_templ[prog] = templ;
           }
-          Trace("cegqi-inv") << "       template (pre-substitution) : " << templ << std::endl;
-          Assert( !templ.isNull() );
-          // subsitute the template arguments
-          templ = templ.substitute( prog_templ_vars.begin(), prog_templ_vars.end(), prog_vars[prog].begin(), prog_vars[prog].end() );
-          Trace("cegqi-inv") << "       template : " << templ << std::endl;
-          d_templ[prog] = templ;
         }
+      }else{
+        //we are fully single invocation
+        d_single_invocation = true;
       }
-    }else{
-      //we are fully single invocation
-      d_single_invocation = true;
     }
   }
 }
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index ad0f4f595..ffcdb7075 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -164,11 +164,9 @@ class CegConjectureSingleInv {
   bool isEligibleForInstantiation( Node n );
   // add lemma
   bool addLemma( Node lem );
- public:
-  CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p );
-  ~CegConjectureSingleInv();
   // conjecture
   Node d_quant;
+  Node d_simp_quant;
   // are we single invocation?
   bool d_single_invocation;
   // single invocation portion of quantified formula
@@ -181,6 +179,15 @@ class CegConjectureSingleInv {
   std::map< Node, Node > d_templ;
   // the template argument for each function to synthesize (occurs in exactly one position of its template)
   std::map< Node, Node > d_templ_arg;
+  
+ public:
+  CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p );
+  ~CegConjectureSingleInv();
+
+  // get simplified conjecture
+  Node getSimplifiedConjecture() { return d_simp_quant; }
+  // get single invocation guard
+  Node getGuard() { return d_si_guard; }
  public:
   //get the single invocation lemma(s)
   void getInitialSingleInvLemma( std::vector< Node >& lems );
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 4cb41e19e..02f1b8509 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -931,7 +931,8 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto
       return true;
     }
   }
-  if( ( lit.getKind()==EQUAL && lit[0].getType().isReal() && pol ) || ( ( lit.getKind()==GEQ || lit.getKind()==GT ) && options::varIneqElimQuant() ) ){
+  if( ( lit.getKind()==EQUAL && lit[0].getType().isReal() && pol && options::varElimQuant() ) || 
+      ( ( lit.getKind()==GEQ || lit.getKind()==GT ) && options::varIneqElimQuant() ) ){
     //for arithmetic, solve the (in)equality
     std::map< Node, Node > msum;
     if( QuantArith::getMonomialSumLit( lit, msum ) ){
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index 01f3be1a1..d8f675af1 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -63,7 +63,8 @@ TESTS = commutative.sy \
         qe.sy \
         cggmp.sy \
         parse-bv-let.sy \
-        cegar1.sy
+        cegar1.sy \
+        triv-type-mismatch-si.sy
 
 
 # sygus tests currently taking too long for make regress
diff --git a/test/regress/regress0/sygus/triv-type-mismatch-si.sy b/test/regress/regress0/sygus/triv-type-mismatch-si.sy
new file mode 100644
index 000000000..e2935af51
--- /dev/null
+++ b/test/regress/regress0/sygus/triv-type-mismatch-si.sy
@@ -0,0 +1,13 @@
+; EXPECT: unsat
+; COMMAND-LINE: --no-dump-synth
+(set-logic LIA)
+
+(synth-fun R ((y Int)) Bool)
+(synth-fun e () Int)
+
+(declare-var x Int)
+
+(constraint (=> (= x e) (R x)))
+
+(check-synth)
+