Merge branch 'master' of https://github.com/CVC4/CVC4

47 files changed, 1894 insertions, 744 deletions

diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index b4ecc1d3d..3cbc45cd1 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -70,6 +70,9 @@ operator BITVECTOR_SLE 2 "bit-vector signed less than or equal (the two bit-vect
 operator BITVECTOR_SGT 2 "bit-vector signed greater than (the two bit-vector parameters must have same width)"
 operator BITVECTOR_SGE 2 "bit-vector signed greater than or equal (the two bit-vector parameters must have same width)"
 
+operator BITVECTOR_REDOR 1 "bit-vector redor"
+operator BITVECTOR_REDAND 1 "bit-vector redand"
+
 operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting (internal-only symbol)"
 operator BITVECTOR_ACKERMANIZE_UDIV 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol)"
 operator BITVECTOR_ACKERMANIZE_UREM 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol)"
@@ -171,6 +174,10 @@ typerule BITVECTOR_SLE ::CVC4::theory::bv::BitVectorPredicateTypeRule
 typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule
 typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule
 
+typerule BITVECTOR_REDOR ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule
+typerule BITVECTOR_REDAND ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule
+
+
 typerule BITVECTOR_EAGER_ATOM ::CVC4::theory::bv::BitVectorEagerAtomTypeRule
 typerule BITVECTOR_ACKERMANIZE_UDIV ::CVC4::theory::bv::BitVectorAckermanizationUdivTypeRule
 typerule BITVECTOR_ACKERMANIZE_UREM ::CVC4::theory::bv::BitVectorAckermanizationUremTypeRule
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 3cc1c323c..768923ee6 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -49,6 +49,8 @@ enum RewriteRuleId {
   UgeEliminate,
   SgeEliminate,
   SgtEliminate,
+  RedorEliminate,
+  RedandEliminate,
   SubEliminate,
   SltEliminate,
   SleEliminate,
@@ -188,6 +190,8 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case SgtEliminate:        out << "SgtEliminate";        return out;
   case UgeEliminate:        out << "UgeEliminate";        return out;
   case SgeEliminate:        out << "SgeEliminate";        return out;
+  case RedorEliminate:      out << "RedorEliminate";      return out;
+  case RedandEliminate:     out << "RedandEliminate";     return out;
   case RepeatEliminate:     out << "RepeatEliminate";     return out;
   case RotateLeftEliminate: out << "RotateLeftEliminate"; return out;
   case RotateRightEliminate:out << "RotateRightEliminate";return out;
@@ -522,6 +526,8 @@ struct AllRewriteRules {
   RewriteRule<UltPlusOne> rule119;
   RewriteRule<ConcatToMult> rule120;
   RewriteRule<IsPowerOfTwo> rule121;
+  RewriteRule<RedorEliminate> rule122;
+  RewriteRule<RedandEliminate> rule123;
 };
 
 template<> inline
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 0442c47d9..cd173a6dd 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -479,6 +479,33 @@ Node RewriteRule<SignExtendEliminate>::apply(TNode node) {
   return utils::mkConcat(extension, node[0]);
 }
 
+template<>
+bool RewriteRule<RedorEliminate>::applies(TNode node) {
+  return (node.getKind() == kind::BITVECTOR_REDOR);
+}
+
+template<>
+Node RewriteRule<RedorEliminate>::apply(TNode node) {
+  Debug("bv-rewrite") << "RewriteRule<RedorEliminate>(" << node << ")" << std::endl;
+  TNode a = node[0];
+  unsigned size = utils::getSize(node[0]); 
+  Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, utils::mkConst( size, 0 ) );
+  return result.negate();
+}
+
+template<>
+bool RewriteRule<RedandEliminate>::applies(TNode node) {
+  return (node.getKind() == kind::BITVECTOR_REDAND);
+}
+
+template<>
+Node RewriteRule<RedandEliminate>::apply(TNode node) {
+  Debug("bv-rewrite") << "RewriteRule<RedandEliminate>(" << node << ")" << std::endl;
+  TNode a = node[0];
+  unsigned size = utils::getSize(node[0]); 
+  Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, utils::mkOnes( size ) );
+  return result;
+}
 
 }
 }
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 86f2c6760..f2adea411 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -553,6 +553,22 @@ RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool prerewrite)
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
+RewriteResponse TheoryBVRewriter::RewriteRedor(TNode node, bool prerewrite){
+  Node resultNode = LinearRewriteStrategy
+    < RewriteRule<RedorEliminate>
+    >::apply(node);
+  
+  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+}
+
+RewriteResponse TheoryBVRewriter::RewriteRedand(TNode node, bool prerewrite){
+  Node resultNode = LinearRewriteStrategy
+    < RewriteRule<RedandEliminate>
+    >::apply(node);
+  
+  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+}
+
 RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<BVToNatEliminate>
@@ -651,6 +667,8 @@ void TheoryBVRewriter::initializeRewrites() {
   d_rewriteTable [ kind::BITVECTOR_SIGN_EXTEND ] = RewriteSignExtend;
   d_rewriteTable [ kind::BITVECTOR_ROTATE_RIGHT ] = RewriteRotateRight;
   d_rewriteTable [ kind::BITVECTOR_ROTATE_LEFT ] = RewriteRotateLeft;
+  d_rewriteTable [ kind::BITVECTOR_REDOR ] = RewriteRedor;
+  d_rewriteTable [ kind::BITVECTOR_REDAND ] = RewriteRedand;
 
   d_rewriteTable [ kind::BITVECTOR_TO_NAT ] = RewriteBVToNat;
   d_rewriteTable [ kind::INT_TO_BITVECTOR ] = RewriteIntToBV;
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 42bccb534..3f0fa8194 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -77,6 +77,8 @@ class TheoryBVRewriter {
   static RewriteResponse RewriteSignExtend(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteRotateRight(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteRotateLeft(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteRedor(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteRedand(TNode node, bool prerewrite = false);
 
   static RewriteResponse RewriteBVToNat(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteIntToBV(TNode node, bool prerewrite = false);
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 81a2d9a27..fbb285fe0 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -112,6 +112,20 @@ public:
   }
 };/* class BitVectorPredicateTypeRule */
 
+class BitVectorUnaryPredicateTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    if( check ) {
+      TypeNode type = n[0].getType(check);
+      if (!type.isBitVector()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms");
+      }
+    }
+    return nodeManager->booleanType();
+  }
+};/* class BitVectorUnaryPredicateTypeRule */
+
 class BitVectorEagerAtomTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 6ebc9db92..a8b6887e5 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -385,6 +385,8 @@ inline bool isBVPredicate(TNode node) {
       node.getKind() == kind::BITVECTOR_SGE ||
       node.getKind() == kind::BITVECTOR_ULE || 
       node.getKind() == kind::BITVECTOR_SLE ||
+      node.getKind() == kind::BITVECTOR_REDOR ||
+      node.getKind() == kind::BITVECTOR_REDAND ||
       ( node.getKind() == kind::NOT && (node[0].getKind() == kind::EQUAL ||
                                         node[0].getKind() == kind::BITVECTOR_ULT ||
                                         node[0].getKind() == kind::BITVECTOR_SLT ||
@@ -393,7 +395,9 @@ inline bool isBVPredicate(TNode node) {
                                         node[0].getKind() == kind::BITVECTOR_SGT ||
                                         node[0].getKind() == kind::BITVECTOR_SGE ||
                                         node[0].getKind() == kind::BITVECTOR_ULE || 
-                                        node[0].getKind() == kind::BITVECTOR_SLE)))
+                                        node[0].getKind() == kind::BITVECTOR_SLE ||
+                                        node[0].getKind() == kind::BITVECTOR_REDOR ||
+                                        node[0].getKind() == kind::BITVECTOR_REDAND)))
     {
       return true; 
     }
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index d08c92dd9..3ab29f334 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -88,7 +88,7 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >
             Kind k = d_tds->getArgKind( tnnp, csIndex );
             //size comparison for arguments (if necessary)
             Node sz_leq;
-            if( tn1==tnn && d_tds->isComm( k ) ){
+            if( tn1==tnn && quantifiers::TermDb::isComm( k ) ){
               sz_leq = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkNode( DT_SIZE, n ), NodeManager::currentNM()->mkNode( DT_SIZE, arg1 ) );
             }
             std::map< int, std::vector< int > >::iterator it = d_sygus_pc_arg_pos[tnn][csIndex].find( i );
@@ -327,7 +327,7 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype&
             Assert( d_sygus_pc_nred[tnn][csIndex].find( sIndex )!=d_sygus_pc_nred[tnn][csIndex].end() );
             Assert( d_sygus_pc_nred[tnno][csIndex].find( osIndex )!=d_sygus_pc_nred[tnno][csIndex].end() );
 
-            bool isPComm = d_tds->isComm( parentKind );
+            bool isPComm = quantifiers::TermDb::isComm( parentKind );
             std::map< int, bool > larg_consider;
             for( unsigned i=0; i<dto.getNumConstructors(); i++ ){
               if( d_sygus_pc_nred[tnno][csIndex][osIndex][i] ){
@@ -411,7 +411,7 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt
   int pc = d_tds->getKindArg( tnp, parent );
   if( k==parent ){
     //check for associativity
-    if( d_tds->isAssoc( k ) ){
+    if( quantifiers::TermDb::isAssoc( k ) ){
       //if the operator is associative, then a repeated occurrence should only occur in the leftmost argument position
       int firstArg = getFirstArgOccurrence( pdt[pc], dt );
       Assert( firstArg!=-1 );
@@ -511,8 +511,8 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt
     }
   }
   if( parent==MINUS || parent==BITVECTOR_SUB ){
-    
-    
+
+
   }
   return true;
 }
@@ -650,12 +650,22 @@ void SygusSymBreak::addTester( Node tst ) {
     std::map< Node, ProgSearch * >::iterator it = d_prog_search.find( a );
     ProgSearch * ps;
     if( it==d_prog_search.end() ){
-      ps = new ProgSearch( this, a, d_context );
+      //check if sygus type
+      TypeNode tn = a.getType();
+      Assert( DatatypesRewriter::isTypeDatatype( tn ) );
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      if( dt.isSygus() ){
+        ps = new ProgSearch( this, a, d_context );
+      }else{
+        ps = NULL;
+      }
       d_prog_search[a] = ps;
     }else{
       ps = it->second;
     }
-    ps->addTester( tst );
+    if( ps ){
+      ps->addTester( tst );
+    }
   }
 }
 
@@ -781,7 +791,7 @@ bool SygusSymBreak::ProgSearch::processSubprograms( Node n, int depth, int odept
 Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, Node parent, std::map< TypeNode, int >& var_count,
                                                             std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u ) {
   Assert( depth>=curr_depth );
-  Trace("sygus-sym-break-debug") << "Reconstructing program for " << prog << " at depth " << curr_depth << "/" << depth << std::endl;
+  Trace("sygus-sym-break-debug") << "Reconstructing program for " << prog << " at depth " << curr_depth << "/" << depth << " " << prog.getType() << std::endl;
   NodeMap::const_iterator it = d_testers.find( prog );
   if( it!=d_testers.end() ){
     Node tst = (*it).second;
@@ -820,10 +830,10 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node
     Node progr = d_tds->getNormalized( at, prog );
     Node rep_prog;
     std::map< Node, Node >::iterator itnp = d_normalized_to_orig[at].find( progr );
-    int tsize = d_tds->getTermSize( prog );
+    int tsize = d_tds->getSygusTermSize( prog );
     if( itnp==d_normalized_to_orig[at].end() ){
       d_normalized_to_orig[at][progr] = prog;
-      if( progr.getKind()==SKOLEM && d_tds->getSygusType( progr )==at ){
+      if( progr.getKind()==SKOLEM && d_tds->getSygusTypeForVar( progr )==at ){
         Trace("sygus-nf") << "* Sygus sym break : " << prog << " rewrites to variable " << progr << " of same type as self" << std::endl;
         d_redundant[at][prog] = true;
         red = true;
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
new file mode 100755
index 000000000..e4dcccdff
--- /dev/null
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -0,0 +1,105 @@
+/*********************                                                        */
+/*! \file alpha_equivalence.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2015  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Alpha equivalence checking
+ **
+ **/
+
+#include "theory/quantifiers/alpha_equivalence.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace CVC4;
+using namespace std;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::kind;
+
+struct sortTypeOrder {
+  TermDb* d_tdb;
+  bool operator() (TypeNode i, TypeNode j) {
+    return d_tdb->getIdForType( i )<d_tdb->getIdForType( j );
+  }
+};
+
+bool AlphaEquivalenceNode::registerNode( QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) {
+  if( tt.size()==arg_index.size()+1 ){
+    Node t = tt.back();
+    Node op = t.hasOperator() ? t.getOperator() : t;
+    arg_index.push_back( 0 );
+    Trace("aeq-debug") << op << " ";
+    return d_children[op][t.getNumChildren()].registerNode( qe, q, tt, arg_index );
+  }else if( tt.empty() ){
+    //we are finished
+    Trace("aeq-debug") << std::endl;
+    if( d_quant.isNull() ){
+      d_quant = q;
+      return true;
+    }else{
+      //lemma ( q <=> d_quant )
+      Trace("alpha-eq") << "Alpha equivalent : " << std::endl;
+      Trace("alpha-eq") << "  " << q << std::endl;
+      Trace("alpha-eq") << "  " << d_quant << std::endl;
+      qe->getOutputChannel().lemma( q.iffNode( d_quant ) );
+      return false;
+    }
+  }else{
+    Node t = tt.back();
+    int i = arg_index.back();
+    if( i==(int)t.getNumChildren() ){
+      tt.pop_back();
+      arg_index.pop_back();
+    }else{
+      tt.push_back( t[i] );
+      arg_index[arg_index.size()-1]++;
+    }
+    return registerNode( qe, q, tt, arg_index );
+  }
+}
+
+bool AlphaEquivalenceTypeNode::registerNode( QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index ){
+  if( index==(int)typs.size() ){
+    std::vector< Node > tt;
+    std::vector< int > arg_index;
+    tt.push_back( t );
+    Trace("aeq-debug") << " : ";
+    return d_data.registerNode( qe, q, tt, arg_index );
+  }else{
+    TypeNode curr = typs[index];
+    Assert( typ_count.find( curr )!=typ_count.end() );
+    Trace("aeq-debug") << "[" << curr << " " << typ_count[curr] << "] ";
+    return d_children[curr][typ_count[curr]].registerNode( qe, q, t, typs, typ_count, index+1 );
+  }
+}
+
+bool AlphaEquivalence::registerQuantifier( Node q ) {
+  Assert( q.getKind()==FORALL );
+  Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
+  //construct canonical quantified formula
+  Node t = d_qe->getTermDatabase()->getCanonicalTerm( q[1], true );
+  Trace("aeq") << "  canonical form: " << t << std::endl;
+  //compute variable type counts
+  std::map< TypeNode, int > typ_count;
+  std::vector< TypeNode > typs;
+  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+    TypeNode tn = q[0][i].getType();
+    typ_count[tn]++;
+    if( std::find( typs.begin(), typs.end(), tn )==typs.end() ){
+      typs.push_back( tn );
+    }
+  }
+  sortTypeOrder sto;
+  sto.d_tdb = d_qe->getTermDatabase();
+  std::sort( typs.begin(), typs.end(), sto );
+  Trace("aeq-debug") << "  ";
+  bool ret = d_ae_typ_trie.registerNode( d_qe, q, t, typs, typ_count );
+  Trace("aeq") << "  ...result : " << ret << std::endl;
+  return ret;
+}
diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h
new file mode 100755
index 000000000..fa2109ccc
--- /dev/null
+++ b/src/theory/quantifiers/alpha_equivalence.h
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file alpha_equivalence.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2015  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Alpha equivalence checking
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__ALPHA_EQUIVALENCE_H
+#define __CVC4__ALPHA_EQUIVALENCE_H
+
+
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class AlphaEquivalenceNode {
+public:
+  std::map< Node, std::map< int, AlphaEquivalenceNode > > d_children;
+  Node d_quant;
+  bool registerNode( QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index );
+};
+
+class AlphaEquivalenceTypeNode {
+public:
+  std::map< TypeNode, std::map< int, AlphaEquivalenceTypeNode > > d_children;
+  AlphaEquivalenceNode d_data;
+  bool registerNode( QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index = 0 );
+};
+
+class AlphaEquivalence {
+private:
+  QuantifiersEngine* d_qe;
+  //per # of variables per type
+  AlphaEquivalenceTypeNode d_ae_typ_trie;
+public:
+  AlphaEquivalence( QuantifiersEngine* qe ) : d_qe( qe ){}
+  ~AlphaEquivalence(){}
+
+  bool registerQuantifier( Node q );
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 5f3498f49..e10ba0fef 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -37,14 +37,25 @@ CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_in
 void CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
   Assert( d_quant.isNull() );
   Assert( q.getKind()==FORALL );
+  d_assert_quant = q;
+  //register with single invocation if applicable
+  if( qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) && options::cegqiSingleInv() ){
+    d_ceg_si->initialize( qe, q );
+    if( q!=d_ceg_si->d_quant ){
+      //Node red_lem = NodeManager::currentNM()->mkNode( OR, q.negate(), d_cegqi_si->d_quant );
+      //may have rewritten quantified formula (for invariant synthesis)
+      q = d_ceg_si->d_quant;
+    }
+  }
   d_quant = q;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() ) );
   }
+  Trace("cegqi") << "Base quantified fm is : " << q << std::endl;
   //construct base instantiation
   d_base_inst = Rewriter::rewrite( qe->getInstantiation( q, d_candidates ) );
   Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl;
-  if( qe->getTermDatabase()->isQAttrSygus( q ) ){
+  if( 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
@@ -59,10 +70,7 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
       }
     }
     d_syntax_guided = true;
-    if( options::cegqiSingleInv() ){
-      d_ceg_si->initialize( qe, q );
-    }
-  }else if( qe->getTermDatabase()->isQAttrSynthesis( q ) ){
+  }else if( qe->getTermDatabase()->isQAttrSynthesis( d_assert_quant ) ){
     d_syntax_guided = false;
   }else{
     Assert( false );
@@ -70,7 +78,7 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
 }
 
 void CegConjecture::initializeGuard( QuantifiersEngine * qe ){
-  if( d_guard.isNull() ){
+  if( isAssigned() && d_guard.isNull() ){
     d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
     //specify guard behavior
     d_guard = qe->getValuation().ensureLiteral( d_guard );
@@ -137,6 +145,10 @@ bool CegConjecture::isSingleInvocation() {
   return d_ceg_si->isSingleInvocation();
 }
 
+bool CegConjecture::needsCheck() {
+  return d_active && !d_infeasible && ( !isSingleInvocation() || d_ceg_si->needsCheck() );
+}
+
 CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){
   d_conj = new CegConjecture( qe->getSatContext() );
   d_last_inst_si = false;
@@ -155,7 +167,7 @@ void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
     Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl;
     Trace("cegqi-engine-debug") << std::endl;
     Trace("cegqi-engine-debug") << "Current conjecture status : active : " << d_conj->d_active << " feasible : " << !d_conj->d_infeasible << std::endl;
-    if( d_conj->d_active && !d_conj->d_infeasible ){
+    if( d_conj->needsCheck() ){
       checkCegConjecture( d_conj );
     }
     Trace("cegqi-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl;
@@ -207,35 +219,38 @@ void CegInstantiation::assertNode( Node n ) {
     //d_guard_assertions[lit] = pol;
     d_conj->d_infeasible = !pol;
   }
-  if( lit==d_conj->d_quant ){
+  if( lit==d_conj->d_assert_quant ){
     d_conj->d_active = true;
   }
 }
 
 Node CegInstantiation::getNextDecisionRequest() {
-  d_conj->initializeGuard( d_quantEngine );
-  bool value;
-  if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) {
-    //if( d_conj->d_guard_split.isNull() ){
-    //  Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard );
-    //  d_quantEngine->getOutputChannel().lemma( lem );
-    //}
-    Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl;
-    return d_conj->d_guard;
-  }
   //enforce fairness
-  if( d_conj->isAssigned() && d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
-    Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
-    if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) {
-      if( !value ){
-        d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 );
-        lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
-        Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl;
+  if( d_conj->isAssigned() ){
+    d_conj->initializeGuard( d_quantEngine );
+    bool value;
+    if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) {
+      //if( d_conj->d_guard_split.isNull() ){
+      //  Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard );
+      //  d_quantEngine->getOutputChannel().lemma( lem );
+      //}
+      Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl;
+      return d_conj->d_guard;
+    }
+
+    if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
+      Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
+      if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) {
+        if( !value ){
+          d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 );
+          lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
+          Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl;
+          return lit;
+        }
+      }else{
+        Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl;
         return lit;
       }
-    }else{
-      Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl;
-      return lit;
     }
   }
 
@@ -244,6 +259,7 @@ Node CegInstantiation::getNextDecisionRequest() {
 
 void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
   Node q = conj->d_quant;
+  Node aq = conj->d_assert_quant;
   Trace("cegqi-engine-debug") << "Synthesis conjecture : " << q << std::endl;
   Trace("cegqi-engine-debug") << "  * Candidate program/output symbol : ";
   for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
@@ -256,7 +272,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
 
   if( conj->d_ce_sk.empty() ){
     Trace("cegqi-engine") << "  *** Check candidate phase..." << std::endl;
-    if( getTermDatabase()->isQAttrSygus( q ) ){
+    if( conj->d_syntax_guided ){
       if( conj->d_ceg_si ){
         std::vector< Node > lems;
         conj->d_ceg_si->check( lems );
@@ -296,7 +312,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
           conj->d_ce_sk.push_back( std::vector< Node >() );
         }
         std::vector< Node > ic;
-        ic.push_back( q.negate() );
+        ic.push_back( aq.negate() );
         std::vector< Node > d;
         collectDisjuncts( inst, d );
         Assert( d.size()==conj->d_base_disj.size() );
@@ -327,7 +343,8 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
         Trace("cegqi-engine") << "  ...find counterexample." << std::endl;
       }
 
-    }else if( getTermDatabase()->isQAttrSynthesis( q ) ){
+    }else{
+      Assert( aq==q );
       std::vector< Node > model_terms;
       if( getModelValues( conj, conj->d_candidates, model_terms ) ){
         d_quantEngine->addInstantiation( q, model_terms, false );
@@ -484,16 +501,18 @@ void CegInstantiation::getMeasureLemmas( Node n, Node v, std::vector< Node >& le
 }
 
 void CegInstantiation::printSynthSolution( std::ostream& out ) {
-  if( d_conj ){
+  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_candidates.size(); i++ ){
+      Node prog = d_conj->d_quant[0][i];
       std::stringstream ss;
-      ss << d_conj->d_quant[0][i];
+      ss << prog;
       std::string f(ss.str());
       f.erase(f.begin());
-      TypeNode tn = d_conj->d_quant[0][i].getType();
+      TypeNode tn = prog.getType();
       Assert( datatypes::DatatypesRewriter::isTypeDatatype( tn ) );
       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
       Assert( dt.isSygus() );
@@ -506,7 +525,34 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
       }else{
         if( !d_conj->d_candidate_inst[i].empty() ){
           sol = d_conj->d_candidate_inst[i].back();
-          status = 1;
+          //check if this was based on a template, if so, we must do reconstruction
+          if( d_conj->d_assert_quant!=d_conj->d_quant ){
+            Trace("cegqi-inv") << "Sygus version of solution is : " << sol << ", type : " << sol.getType() << std::endl;
+            sol = getTermDatabase()->getTermDatabaseSygus()->sygusToBuiltin( sol, sol.getType() );
+            Trace("cegqi-inv") << "Builtin 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( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){
+              Node pre = d_conj->d_ceg_si->d_trans_pre[prog];
+              pre = pre.substitute( d_conj->d_ceg_si->d_prog_templ_vars[prog].begin(), d_conj->d_ceg_si->d_prog_templ_vars[prog].end(),
+                                    subs.begin(), subs.end() );
+              sol = NodeManager::currentNM()->mkNode( OR, sol, pre );
+            }else if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST ){
+              Node post = d_conj->d_ceg_si->d_trans_post[prog];
+              post = post.substitute( d_conj->d_ceg_si->d_prog_templ_vars[prog].begin(), d_conj->d_ceg_si->d_prog_templ_vars[prog].end(),
+                                      subs.begin(), subs.end() );
+              sol = NodeManager::currentNM()->mkNode( AND, sol, post );
+            }
+            Trace("cegqi-inv-debug") << "With template : " << sol << std::endl;
+            sol = Rewriter::rewrite( sol );
+            Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl;
+            sol = d_conj->d_ceg_si->reconstructToSyntax( sol, tn, status );
+          }else{
+            status = 1;
+          }
         }
       }
       if( !(Trace.isOn("cegqi-stats")) ){
@@ -530,6 +576,8 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
         out << ")" << std::endl;
       }
     }
+  }else{
+    Assert( false );
   }
 }
 
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 74e9b0aba..af3a19d62 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -35,7 +35,9 @@ public:
   context::CDO< bool > d_active;
   /** is conjecture infeasible */
   context::CDO< bool > d_infeasible;
-  /** quantified formula */
+  /** quantified formula asserted */
+  Node d_assert_quant;
+  /** quantified formula (after processing) */
   Node d_quant;
   /** guard */
   Node d_guard;
@@ -83,6 +85,8 @@ public:  //for fairness
   CegqiFairMode getCegqiFairMode();
   /** is single invocation */
   bool isSingleInvocation();
+  /** needs check */
+  bool needsCheck();
 };
 
 
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 22ffcd278..ef2e3005e 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -538,6 +538,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
         d_qe->getOutputChannel().lemma( delta_lem );
       }
       subs[i] = NodeManager::currentNM()->mkNode( subs_typ[i]==2 ? PLUS : MINUS, subs[i], d_n_delta );
+      d_used_delta = true;
     }
   }
   //check if we have already added this instantiation
@@ -706,7 +707,7 @@ void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) {
   */
 }
 
-void CegInstantiator::check() {
+bool CegInstantiator::check() {
 
   for( unsigned r=0; r<2; r++ ){
     std::vector< Node > subs;
@@ -716,10 +717,11 @@ void CegInstantiator::check() {
     std::vector< int > subs_typ;
     //try to add an instantiation
     if( addInstantiation( subs, vars, coeff, has_coeff, subs_typ, 0, r==0 ? 0 : 2 ) ){
-      return;
+      return true;
     }
   }
   Trace("cegqi-engine") << "  WARNING : unable to find CEGQI single invocation instantiation." << std::endl;
+  return false;
 }
 
 
@@ -740,29 +742,38 @@ CegConjectureSingleInv::CegConjectureSingleInv( CegConjecture * p ) : d_parent(
   d_sol = NULL;
   d_c_inst_match_trie = NULL;
   d_cinst = NULL;
+  d_has_ites = true;
 }
 
 Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) {
   if( !d_single_inv.isNull() ) {
-    Assert( d_single_inv.getKind()==FORALL );
     d_single_inv_var.clear();
     d_single_inv_sk.clear();
-    for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
-      std::stringstream ss;
-      ss << "k_" << d_single_inv[0][i];
-      Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" );
-      d_single_inv_var.push_back( d_single_inv[0][i] );
-      d_single_inv_sk.push_back( k );
-      d_single_inv_sk_index[k] = i;
+    Node inst;
+    if( d_single_inv.getKind()==FORALL ){
+      for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
+        std::stringstream ss;
+        ss << "k_" << d_single_inv[0][i];
+        Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" );
+        d_single_inv_var.push_back( d_single_inv[0][i] );
+        d_single_inv_sk.push_back( k );
+        d_single_inv_sk_index[k] = i;
+      }
+      inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
+    }else{
+      inst = d_single_inv;
     }
-    Node inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
     inst = TermDb::simpleNegate( inst );
     Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl;
 
     //initialize the instantiator for this
-    CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this );
-    d_cinst = new CegInstantiator( d_qe, cosi );
-    d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
+    if( !d_single_inv_sk.empty() ){
+      CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this );
+      d_cinst = new CegInstantiator( d_qe, cosi );
+      d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
+    }else{
+      d_cinst = NULL;
+    }
 
     return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst );
   }else{
@@ -788,9 +799,18 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
   std::map< Node, std::map< Node, bool > > contains;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     progs.push_back( q[0][i] );
+    //check whether all types have ITE
+    TypeNode tn = q[0][i].getType();
+    d_qe->getTermDatabaseSygus()->registerSygusType( tn );
+    if( !d_qe->getTermDatabaseSygus()->sygusToBuiltinType( tn ).isBoolean() ){
+      if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){
+        d_has_ites = false;
+      }
+    }
   }
   //collect information about conjunctions
   bool singleInvocation = false;
+  bool invExtractPrePost = false;
   if( analyzeSygusConjunct( Node::null(), q[1], children, prog_invoke, progs, contains, true ) ){
     singleInvocation = true;
     //try to phrase as single invocation property
@@ -807,7 +827,6 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
           for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){
             if( it2->second.size()>1 ){
               singleInvocation = false;
-              break;
             }else if( it2->second.size()==1 ){
               Node prog = it2->first;
               Node inv = it2->second[0];
@@ -821,15 +840,26 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
                   single_invoke_args[prog][k-1].push_back( arg );
                 }
               }
+              if( inv.getType().isBoolean() ){
+                //conjunct defines pre and/or post conditions
+                if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){
+                  invExtractPrePost = true;
+                }
+              }
             }
           }
         }
       }
     }
-    if( singleInvocation ){
+    if( singleInvocation || invExtractPrePost ){
+      //no value in extracting pre/post if we are single invocation
+      if( singleInvocation ){
+        invExtractPrePost = false;
+      }
       Trace("cegqi-si") << "Property is single invocation with : " << std::endl;
       std::vector< Node > pbvs;
       std::vector< Node > new_vars;
+      std::map< Node, std::vector< Node > > prog_vars;
       std::map< Node, std::vector< Node > > new_assumptions;
       for( std::map< Node, std::vector< Node > >::iterator it = invocations.begin(); it != invocations.end(); ++it ){
         Assert( !it->second.empty() );
@@ -849,12 +879,14 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
           Assert( !single_invoke_args[prog][k-1].empty() );
           if( single_invoke_args[prog][k-1].size()==1 && single_invoke_args[prog][k-1][0].getKind()==BOUND_VARIABLE ){
             invc.push_back( single_invoke_args[prog][k-1][0] );
+            prog_vars[prog].push_back( single_invoke_args[prog][k-1][0] );
           }else{
             //introduce fresh variable, assign all
             Node v = NodeManager::currentNM()->mkSkolem( "a", single_invoke_args[prog][k-1][0].getType(), "single invocation arg" );
             new_vars.push_back( v );
             invc.push_back( v );
             d_single_inv_arg_sk.push_back( v );
+            prog_vars[prog].push_back( v );
 
             for( unsigned i=0; i<single_invoke_args[prog][k-1].size(); i++ ){
               Node arg = single_invoke_args[prog][k-1][i];
@@ -878,13 +910,16 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
       }
       //construct the single invocation version of the property
       Trace("cegqi-si") << "Single invocation formula conjuncts are : " << std::endl;
-      //std::vector< Node > si_conj;
-      Assert( !pbvs.empty() );
-      Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs );
+      Node pbvl;
+      if( !pbvs.empty() ){
+        pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs );
+      }
       for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){
         //should hold since we prevent miniscoping
         Assert( d_single_inv.isNull() );
         std::vector< Node > conjuncts;
+        std::vector< Node > conjuncts_si_progs;
+        std::vector< Node > conjuncts_si_invokes;
         for( unsigned i=0; i<it->second.size(); i++ ){
           Node c = it->second[i];
           std::vector< Node > disj;
@@ -896,17 +931,32 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
           if( itp!=prog_invoke.end() ){
             std::vector< Node > terms;
             std::vector< Node > subs;
+            std::vector< Node > progs;
             for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){
-              if( !it2->second.empty() ){
+              if( it2->second.size()==1 ){
                 Node prog = it2->first;
                 Node inv = it2->second[0];
                 Assert( it2->second.size()==1 );
                 terms.push_back( inv );
                 subs.push_back( d_single_inv_map[prog] );
+                progs.push_back( prog );
                 Trace("cegqi-si-debug2") << "subs : " << inv << " -> var for " << prog << " : " << d_single_inv_map[prog] << std::endl;
               }
             }
-            cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
+            if( singleInvocation ){
+              cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
+            }else{
+              cr = c;
+              if( invExtractPrePost ){
+                if( terms.size()==1 ){
+                  conjuncts_si_progs.push_back( progs[0] );
+                  conjuncts_si_invokes.push_back( terms[0] );
+                }else if( terms.size()>1 ){
+                  //abort when mixing multiple invariants?  TODO
+                  invExtractPrePost = false;
+                }
+              }
+            }
           }else{
             cr = c;
           }
@@ -920,6 +970,10 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
           Node curr = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj );
           curr = TermDb::simpleNegate( curr );
           Trace("cegqi-si") << "    " << curr;
+          if( invExtractPrePost && conjuncts.size()==conjuncts_si_progs.size() ){
+            conjuncts_si_progs.push_back( Node::null() );
+            conjuncts_si_invokes.push_back( Node::null() );
+          }
           conjuncts.push_back( curr );
           if( !it->first.isNull() ){
             Trace("cegqi-si-debug") << " under " << it->first;
@@ -927,68 +981,162 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
           Trace("cegqi-si") << std::endl;
         }
         Assert( !conjuncts.empty() );
-        //make the skolems for the existential
-        if( !it->first.isNull() ){
-          std::vector< Node > vars;
-          std::vector< Node > sks;
-          for( unsigned j=0; j<it->first.getNumChildren(); j++ ){
-            std::stringstream ss;
-            ss << "a_" << it->first[j];
-            Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" );
-            vars.push_back( it->first[j] );
-            sks.push_back( v );
+        //CASE 1 : rewrite based on a template for invariants
+        if( invExtractPrePost ){
+          //for invariant synthesis
+          std::map< Node, bool > has_inv;
+          std::map< Node, std::vector< Node > > inv_pre_post[2];
+          for( unsigned c=0; c<conjuncts.size(); c++ ){
+            Node inv = conjuncts_si_invokes[c];
+            Node prog = conjuncts_si_progs[c];
+            Trace("cegqi-si-inv-debug") << "Conjunct #" << c << ": " << conjuncts[c] << std::endl;
+            if( !prog.isNull() ){
+              Trace("cegqi-si-inv-debug") << "...has program " << prog << " invoked once: " << inv << std::endl;
+              std::vector< Node > curr_disj;
+              //find the polarity of the invocation : this determines pre vs. post
+              int pol = extractInvariantPolarity( conjuncts[c], inv, curr_disj, true );
+              Trace("cegqi-si-inv-debug") << "...polarity is " << pol << std::endl;
+              if( ( pol==1 && !curr_disj.empty() ) || pol==0 ){
+                //conjunct is part of pre/post condition : will add to template of invariant
+                Node nc = curr_disj.empty() ? NodeManager::currentNM()->mkConst( true ) :
+                           ( curr_disj.size()==1 ? curr_disj[0] : NodeManager::currentNM()->mkNode( AND, curr_disj ) );
+                nc = pol==0 ? nc : TermDb::simpleNegate( nc );
+                Trace("cegqi-si-inv-debug") << "  -> " << nc << " is " << ( pol==0 ? "pre" : "post" ) << "condition of invariant " << prog << "." << std::endl;
+                inv_pre_post[pol][prog].push_back( nc );
+                has_inv[prog] = true;
+              }
+            }
           }
-          //substitute conjunctions
-          for( unsigned i=0; i<conjuncts.size(); i++ ){
-            conjuncts[i] = conjuncts[i].substitute( vars.begin(), vars.end(), sks.begin(), sks.end() );
+          Trace("cegqi-si-inv") << "Constructing invariant templates..." << std::endl;
+          //now, contruct the template for the invariant(s)
+          std::map< Node, Node > prog_templ;
+          for( std::map< Node, bool >::iterator iti = has_inv.begin(); iti != has_inv.end(); ++iti ){
+            Node prog = iti->first;
+            Trace("cegqi-si-inv") << "...for " << prog << "..." << std::endl;
+            Trace("cegqi-si-inv") << "   args : ";
+            for( unsigned j=0; j<prog_vars[prog].size(); j++ ){
+              Node v = NodeManager::currentNM()->mkBoundVar( prog_vars[prog][j].getType() );
+              d_prog_templ_vars[prog].push_back( v );
+              Trace("cegqi-si-inv") << v << " ";
+            }
+            Trace("cegqi-si-inv") << std::endl;
+            Node pre = inv_pre_post[0][prog].empty() ? NodeManager::currentNM()->mkConst( false ) :
+                       ( inv_pre_post[0][prog].size()==1 ? inv_pre_post[0][prog][0] : NodeManager::currentNM()->mkNode( OR, inv_pre_post[0][prog] ) );
+            d_trans_pre[prog] = pre.substitute( prog_vars[prog].begin(), prog_vars[prog].end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() );
+            Node post = inv_pre_post[1][prog].empty() ? NodeManager::currentNM()->mkConst( true ) :
+                        ( inv_pre_post[1][prog].size()==1 ? inv_pre_post[1][prog][0] : NodeManager::currentNM()->mkNode( AND, inv_pre_post[1][prog] ) );
+            d_trans_post[prog] = post.substitute( prog_vars[prog].begin(), prog_vars[prog].end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() );
+            Trace("cegqi-si-inv") << "   precondition : " << d_trans_pre[prog] << std::endl;
+            Trace("cegqi-si-inv") << "  postcondition : " << d_trans_post[prog] << std::endl;
+            Node invariant = d_single_inv_app_map[prog];
+            invariant = invariant.substitute( prog_vars[prog].begin(), prog_vars[prog].end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() );
+            Trace("cegqi-si-inv") << "      invariant : " << invariant << std::endl;
+            //construct template
+            Node templ;
+            if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){
+              //templ = 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], invariant );
+            }else{
+              Assert( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST );
+              //templ = 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], invariant );
+            }
+            Trace("cegqi-si-inv") << "       template : " << templ << std::endl;
+            prog_templ[prog] = templ;
           }
-          d_single_inv_arg_sk.insert( d_single_inv_arg_sk.end(), sks.begin(), sks.end() );
-          //substitute single invocation applications
-          for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){
-            Node n = itam->second;
-            d_single_inv_app_map[itam->first] = n.substitute( vars.begin(), vars.end(), sks.begin(), sks.end() );
+          Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts );
+          Trace("cegqi-si-inv") << "           body : " << bd << std::endl;
+          bd = substituteInvariantTemplates( bd, prog_templ, d_prog_templ_vars );
+          Trace("cegqi-si-inv-debug") << "     templ-subs body : " << bd << std::endl;
+          //make inner existential
+          std::vector< Node > new_var_bv;
+          for( unsigned j=0; j<new_vars.size(); j++ ){
+            new_var_bv.push_back( NodeManager::currentNM()->mkBoundVar( new_vars[j].getType() ) );
           }
-        }
-        //ensure that this is a ground property
-        for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){
-          Node n = itam->second;
-          //check if all variables are arguments of this
-          std::vector< Node > n_args;
-          for( unsigned i=1; i<n.getNumChildren(); i++ ){
-            n_args.push_back( n[i] );
+          bd = bd.substitute( new_vars.begin(), new_vars.end(), new_var_bv.begin(), new_var_bv.end() );
+          for( unsigned j=0; j<q[1][0][0].getNumChildren(); j++ ){
+            new_var_bv.push_back( q[1][0][0][j] );
           }
-          for( int i=0; i<(int)d_single_inv_arg_sk.size(); i++ ){
-            if( std::find( n_args.begin(), n_args.end(), d_single_inv_arg_sk[i] )==n_args.end() ){
-              Trace("cegqi-si") << "...property is not ground: program invocation " << n << " does not contain variable " << d_single_inv_arg_sk[i] << "." << std::endl;
-              //try to do variable elimination on d_single_inv_arg_sk[i]
-              if( doVariableElimination( d_single_inv_arg_sk[i], conjuncts ) ){
-                Trace("cegqi-si") << "...did variable elimination on " << d_single_inv_arg_sk[i] << std::endl;
-                d_single_inv_arg_sk.erase( d_single_inv_arg_sk.begin() + i, d_single_inv_arg_sk.begin() + i + 1 );
-                i--;
-              }else{
-                singleInvocation = false;
-                //exit( 57 );
+          if( !new_var_bv.empty() ){
+            Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, new_var_bv );
+            bd = NodeManager::currentNM()->mkNode( FORALL, bvl, TermDb::simpleNegate( bd ) ).negate();
+          }
+          //make outer universal
+          bd = NodeManager::currentNM()->mkNode( FORALL, q[0], bd );
+          bd = Rewriter::rewrite( bd );
+          Trace("cegqi-si-inv") << "  rtempl-subs body : " << bd << std::endl;
+          d_quant = bd;
+        //CASE 2 : rewrite based on single invocation
+        }else{
+          //make the skolems for the existential
+          if( !it->first.isNull() ){
+            std::vector< Node > vars;
+            std::vector< Node > sks;
+            for( unsigned j=0; j<it->first.getNumChildren(); j++ ){
+              std::stringstream ss;
+              ss << "a_" << it->first[j];
+              Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" );
+              vars.push_back( it->first[j] );
+              sks.push_back( v );
+            }
+            //substitute conjunctions
+            for( unsigned i=0; i<conjuncts.size(); i++ ){
+              conjuncts[i] = conjuncts[i].substitute( vars.begin(), vars.end(), sks.begin(), sks.end() );
+            }
+            d_single_inv_arg_sk.insert( d_single_inv_arg_sk.end(), sks.begin(), sks.end() );
+            //substitute single invocation applications
+            for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){
+              Node n = itam->second;
+              d_single_inv_app_map[itam->first] = n.substitute( vars.begin(), vars.end(), sks.begin(), sks.end() );
+            }
+          }
+          //ensure that this is a ground property
+          for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){
+            Node n = itam->second;
+            //check if all variables are arguments of this
+            std::vector< Node > n_args;
+            for( unsigned i=1; i<n.getNumChildren(); i++ ){
+              n_args.push_back( n[i] );
+            }
+            for( int i=0; i<(int)d_single_inv_arg_sk.size(); i++ ){
+              if( std::find( n_args.begin(), n_args.end(), d_single_inv_arg_sk[i] )==n_args.end() ){
+                Trace("cegqi-si") << "...property is not ground: program invocation " << n << " does not contain variable " << d_single_inv_arg_sk[i] << "." << std::endl;
+                //try to do variable elimination on d_single_inv_arg_sk[i]
+                if( doVariableElimination( d_single_inv_arg_sk[i], conjuncts ) ){
+                  Trace("cegqi-si") << "...did variable elimination on " << d_single_inv_arg_sk[i] << std::endl;
+                  d_single_inv_arg_sk.erase( d_single_inv_arg_sk.begin() + i, d_single_inv_arg_sk.begin() + i + 1 );
+                  i--;
+                }else{
+                  singleInvocation = false;
+                  //exit( 57 );
+                }
+                break;
               }
-              break;
             }
           }
-        }
 
-        if( singleInvocation ){
-          Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts );
-          d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
-          Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl;
-          if( options::eMatching.wasSetByUser() ){
-            Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv );
-            std::vector< Node > patTerms;
-            std::vector< Node > exclude;
-            inst::Trigger::collectPatTerms( d_qe, d_single_inv, bd, patTerms, inst::Trigger::TS_ALL, exclude );
-            if( !patTerms.empty() ){
-              Trace("cegqi-si-em") << "Triggers : " << std::endl;
-              for( unsigned i=0; i<patTerms.size(); i++ ){
-                Trace("cegqi-si-em") << "   " << patTerms[i] << std::endl;
+          if( singleInvocation ){
+            Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts );
+            if( pbvl.isNull() ){
+              d_single_inv = bd;
+            }else{
+              d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
+            }
+            Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl;
+            /*
+            if( options::eMatching() && options::eMatching.wasSetByUser() ){
+              Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv );
+              std::vector< Node > patTerms;
+              std::vector< Node > exclude;
+              inst::Trigger::collectPatTerms( d_qe, d_single_inv, bd, patTerms, inst::Trigger::TS_ALL, exclude );
+              if( !patTerms.empty() ){
+                Trace("cegqi-si-em") << "Triggers : " << std::endl;
+                for( unsigned i=0; i<patTerms.size(); i++ ){
+                  Trace("cegqi-si-em") << "   " << patTerms[i] << std::endl;
+                }
               }
             }
+            */
           }
         }
       }
@@ -997,9 +1145,68 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
   if( !singleInvocation ){
     Trace("cegqi-si") << "Property is not single invocation." << std::endl;
     if( options::cegqiSingleInvAbort() ){
-      Message() << "Property is not single invocation." << std::endl;
+      Notice() << "Property is not single invocation." << std::endl;
       exit( 0 );
     }
+  }else{
+    if( options::cegqiSingleInvPreRegInst() && d_single_inv.getKind()==FORALL ){
+      Trace("cegqi-si-presolve") << "Check " << d_single_inv << std::endl;
+      //at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing
+      std::vector< Node > vars;
+      std::map< Node, std::vector< Node > > teq;
+      for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
+        vars.push_back( d_single_inv[0][i] );
+        teq[d_single_inv[0][i]].clear();
+      }
+      collectPresolveEqTerms( d_single_inv[1], teq );
+      std::vector< Node > terms;
+      std::vector< Node > conj;
+      getPresolveEqConjuncts( vars, terms, teq, d_single_inv, conj );
+
+      if( !conj.empty() ){
+        Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
+        Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() );
+        lem = NodeManager::currentNM()->mkNode( OR, g, lem );
+        d_qe->getOutputChannel().lemma( lem, false, true );
+      }
+    }
+  }
+}
+
+void CegConjectureSingleInv::collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ) {
+  if( n.getKind()==EQUAL ){
+    for( unsigned i=0; i<2; i++ ){
+      std::map< Node, std::vector< Node > >::iterator it = teq.find( n[i] );
+      if( it!=teq.end() ){
+        Node nn = n[ i==0 ? 1 : 0 ];
+        if( std::find( it->second.begin(), it->second.end(), nn )==it->second.end() ){
+          it->second.push_back( nn );
+          Trace("cegqi-si-presolve") << "  - " << n[i] << " = " << nn << std::endl;
+        }
+      }
+    }
+  }
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    collectPresolveEqTerms( n[i], teq );
+  }
+}
+
+void CegConjectureSingleInv::getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms,
+                                                     std::map< Node, std::vector< Node > >& teq, Node f, std::vector< Node >& conj ) {
+  if( conj.size()<1000 ){
+    if( terms.size()==f[0].getNumChildren() ){
+      Node c = f[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+      conj.push_back( c );
+    }else{
+      unsigned i = terms.size();
+      Node v = f[0][i];
+      terms.push_back( Node::null() );
+      for( unsigned j=0; j<teq[v].size(); j++ ){
+        terms[i] = teq[v][j];
+        getPresolveEqConjuncts( vars, terms, teq, f, conj );
+      }
+      terms.pop_back();
+    }
   }
 }
 
@@ -1060,9 +1267,66 @@ bool CegConjectureSingleInv::getVariableEliminationTerm( bool pol, bool hasPol,
   return false;
 }
 
+int CegConjectureSingleInv::extractInvariantPolarity( Node n, Node inv, std::vector< Node >& curr_disj, bool pol ) {
+  if( n.getKind()==NOT ){
+    return extractInvariantPolarity( n[0], inv, curr_disj, !pol );
+  }else if( ( n.getKind()==AND && pol ) || ( n.getKind()==OR && !pol ) ){
+    int curr_pol = -1;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      int eipc = extractInvariantPolarity( n[i], inv, curr_disj, pol );
+      if( eipc!=-1 ){
+        if( curr_pol==-1 ){
+          curr_pol = eipc;
+        }else{
+          return -1;
+        }
+      }else{
+        curr_disj.push_back( pol ? n[i] : TermDb::simpleNegate( n[i] ) );
+      }
+    }
+    return curr_pol;
+  }else if( n==inv ){
+    return pol ? 1 : 0;
+  }else{
+    return -1;
+  }
+}
+
+Node CegConjectureSingleInv::substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars ) {
+  if( n.getKind()==APPLY_UF && n.getNumChildren()>0 ){
+    std::map< Node, Node >::iterator it = prog_templ.find( n[0] );
+    if( it!=prog_templ.end() ){
+      std::vector< Node > children;
+      for( unsigned i=1; i<n.getNumChildren(); i++ ){
+        children.push_back( n[i] );
+      }
+      std::map< Node, std::vector< Node > >::iterator itv = prog_templ_vars.find( n[0] );
+      Assert( itv!=prog_templ_vars.end() );
+      Assert( children.size()==itv->second.size() );
+      Node newc = it->second.substitute( itv->second.begin(), itv->second.end(), children.begin(), children.end() );
+      return newc;
+    }
+  }
+  bool childChanged = false;
+  std::vector< Node > children;
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    Node nn = substituteInvariantTemplates( n[i], prog_templ, prog_templ_vars );
+    children.push_back( nn );
+    childChanged = childChanged || ( nn!=n[i] );
+  }
+  if( childChanged ){
+    if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+      children.insert( children.begin(), n.getOperator() );
+    }
+    return NodeManager::currentNM()->mkNode( n.getKind(), children );
+  }else{
+    return n;
+  }
+}
+
 bool CegConjectureSingleInv::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children,
-                                                            std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
-                                                            std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) {
+                                                   std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
+                                                   std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) {
   if( ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ) ){
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       if( !analyzeSygusConjunct( p, n[i], children, prog_invoke, progs, contains, pol ) ){
@@ -1169,8 +1433,7 @@ bool CegConjectureSingleInv::addLemma( Node n ) {
 }
 
 void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
-  if( !d_single_inv.isNull() ) {
-    Assert( d_cinst!=NULL );
+  if( !d_single_inv.isNull() && d_cinst!=NULL ) {
     d_curr_lemmas.clear();
     //check if there are delta lemmas
     d_cinst->getDeltaLemmas( lems );
@@ -1184,20 +1447,61 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
   }
 }
 
-Node CegConjectureSingleInv::constructSolution( unsigned i, unsigned index ) {
+Node CegConjectureSingleInv::constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index ) {
   Assert( index<d_inst.size() );
   Assert( i<d_inst[index].size() );
+  unsigned uindex = indices[index];
   if( index==d_inst.size()-1 ){
-    return d_inst[index][i];
+    return d_inst[uindex][i];
   }else{
-    Node cond = d_lemmas_produced[index];
+    Node cond = d_lemmas_produced[uindex];
     cond = TermDb::simpleNegate( cond );
-    Node ite1 = d_inst[index][i];
-    Node ite2 = constructSolution( i, index+1 );
+    Node ite1 = d_inst[uindex][i];
+    Node ite2 = constructSolution( indices, i, index+1 );
     return NodeManager::currentNM()->mkNode( ITE, cond, ite1, ite2 );
   }
 }
 
+//TODO: use term size?
+struct sortSiInstanceIndices {
+  CegConjectureSingleInv* d_ccsi;
+  int d_i;
+  bool operator() (unsigned i, unsigned j) {
+    if( d_ccsi->d_inst[i][d_i].isConst() && !d_ccsi->d_inst[j][d_i].isConst() ){
+      return true;
+    }else{
+      return false;
+    }
+  }
+};
+
+/*
+Node removeBooleanIte( Node n ){
+  if( n.getKind()==ITE && n.getType().isBoolean() ){
+    Node n1 = removeBooleanIte( n[1] );
+    Node n2 = removeBooleanIte( n[2] );
+    return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n[0], n1 ),
+                                                 NodeManager::currentNM()->mkNode( AND, n[0].negate(), n2 ) );
+  }else{
+    bool childChanged = false;
+    std::vector< Node > children;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      Node nn = removeBooleanIte( n[i] );
+      children.push_back( nn );
+      childChanged = childChanged || nn!=n[i];
+    }
+    if( childChanged ){
+      if( n.hasOperator() ){
+        children.insert( children.begin(), n.getOperator() );
+      }
+      return NodeManager::currentNM()->mkNode( n.getKind(), children );
+    }else{
+      return n;
+    }
+  }
+}
+*/
+
 Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ){
   Assert( d_sol!=NULL );
   Assert( !d_lemmas_produced.empty() );
@@ -1223,7 +1527,21 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
     d_sol->d_varList.push_back( varList[i-1] );
   }
   //construct the solution
-  Node s = constructSolution( sol_index, 0 );
+  Trace("csi-sol") << "Sort solution return values " << sol_index << std::endl;
+  Assert( d_lemmas_produced.size()==d_inst.size() );
+  std::vector< unsigned > indices;
+  for( unsigned i=0; i<d_lemmas_produced.size(); i++ ){
+    Assert( sol_index<d_inst[i].size() );
+    indices.push_back( i );
+  }
+  //sort indices based on heuristic : currently, do all constant returns first (leads to simpler conditions)
+  // TODO : to minimize solution size, put the largest term last
+  sortSiInstanceIndices ssii;
+  ssii.d_ccsi = this;
+  ssii.d_i = sol_index;
+  std::sort( indices.begin(), indices.end(), ssii );
+  Trace("csi-sol") << "Construct solution" << std::endl;
+  Node s = constructSolution( indices, sol_index, 0 );
   s = s.substitute( vars.begin(), vars.end(), d_varList.begin(), d_varList.end() );
   d_orig_solution = s;
 
@@ -1231,7 +1549,12 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
   Trace("csi-sol") << "Solution (pre-simplification): " << d_orig_solution << std::endl;
   s = d_sol->simplifySolution( s, stn );
   Trace("csi-sol") << "Solution (post-simplification): " << s << std::endl;
+  return reconstructToSyntax( s, stn, reconstructed );
+}
+
+Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& reconstructed ) {
   d_solution = s;
+  const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
 
   //reconstruct the solution into sygus if necessary
   reconstructed = 0;
@@ -1240,6 +1563,10 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
     if( reconstructed==1 ){
       Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << d_sygus_solution << std::endl;
     }
+  }else{
+    ////remove boolean ITE (not allowed for sygus comp 2015)
+    //d_solution = removeBooleanIte( d_solution );
+    //Trace("csi-sol") << "Solution (after remove boolean ITE) : " << d_solution << std::endl;
   }
 
 
@@ -1276,4 +1603,14 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
   }
 }
 
+bool CegConjectureSingleInv::needsCheck() {
+  if( options::cegqiSingleInvMultiInstAbort() ){
+    if( !hasITEs() ){
+      return d_inst.empty();
+    }
+  }
+  return true;
+}
+
+
 }
\ No newline at end of file
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index 54f762720..f0d00b61c 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -71,8 +71,9 @@ public:
   std::vector< Node > d_vars;
   //delta
   Node d_n_delta;
+  bool d_used_delta;
   //check : add instantiations based on valuation of d_vars
-  void check();
+  bool check();
   // get delta lemmas : on-demand force minimality of d_n_delta
   void getDeltaLemmas( std::vector< Node >& lems );
 };
@@ -110,8 +111,14 @@ private:
   bool processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals );
   bool doVariableElimination( Node v, std::vector< Node >& conjuncts );
   bool getVariableEliminationTerm( bool pol, bool active, Node v, Node n, TNode& s, int& status );
+  //for recognizing templates for invariant synthesis
+  int extractInvariantPolarity( Node n, Node inv, std::vector< Node >& curr_disj, bool pol );
+  Node substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars );
+  //presolve
+  void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq );
+  void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj );
   //constructing solution
-  Node constructSolution( unsigned i, unsigned index );
+  Node constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index );
 private:
   //map from programs to variables in single invocation property
   std::map< Node, Node > d_single_inv_map;
@@ -126,8 +133,6 @@ private:
   //list of skolems for each program
   std::vector< Node > d_single_inv_var;
   //lemmas produced
-  std::vector< Node > d_lemmas_produced;
-  std::vector< std::vector< Node > > d_inst;
   inst::InstMatchTrie d_inst_match_trie;
   inst::CDInstMatchTrie * d_c_inst_match_trie;
   // solution
@@ -135,6 +140,11 @@ private:
   Node d_orig_solution;
   Node d_solution;
   Node d_sygus_solution;
+  bool d_has_ites;
+public:
+  //lemmas produced
+  std::vector< Node > d_lemmas_produced;
+  std::vector< std::vector< Node > > d_inst;
 private:
   std::vector< Node > d_curr_lemmas;
   //add instantiation
@@ -149,6 +159,10 @@ public:
   Node d_quant;
   // single invocation version of quant
   Node d_single_inv;
+  // transition relation version per program
+  std::map< Node, Node > d_trans_pre;
+  std::map< Node, Node > d_trans_post;
+  std::map< Node, std::vector< Node > > d_prog_templ_vars;
 public:
   //get the single invocation lemma
   Node getSingleInvLemma( Node guard );
@@ -158,8 +172,14 @@ public:
   void check( std::vector< Node >& lems );
   //get solution
   Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed );
+  //reconstruct to syntax
+  Node reconstructToSyntax( Node s, TypeNode stn, int& reconstructed );
+  // has ites
+  bool hasITEs() { return d_has_ites; }
   // is single invocation
   bool isSingleInvocation() { return !d_single_inv.isNull(); }
+  //needs check
+  bool needsCheck();
 };
 
 }
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
index 845e20795..413fd9ba2 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
@@ -86,8 +86,11 @@ Node CegConjectureSingleInvSol::pullITEs( Node s ) {
         Trace("csi-sol-debug") << "For " << s << ", can pull " << cond << " -> " << t << " with remainder " << rem << std::endl;
         t = pullITEs( t );
         rem = pullITEs( rem );
+        Trace("csi-pull-ite") << "PI: Rewrite : " << s << std::endl;
+        Node prev = s;
         s = NodeManager::currentNM()->mkNode( ITE, TermDb::simpleNegate( cond ), t, rem );
-        //Trace("csi-debug-sol") << "Now : " << s << std::endl;
+        Trace("csi-pull-ite") << "PI: Rewrite Now : " << s << std::endl;
+        Trace("csi-pull-ite") << "(= " << prev << " " << s << ")" << std::endl;
         success = true;
       }
     }while( success );
@@ -99,11 +102,13 @@ Node CegConjectureSingleInvSol::pullITEs( Node s ) {
 bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::vector< Node >& conj, Node& t, Node& rem, int depth ) {
   Assert( n_ite.getKind()==ITE );
   std::vector< Node > curr_conj;
+  std::vector< Node > orig_conj;
   bool isAnd;
   if( n_ite[0].getKind()==AND || n_ite[0].getKind()==OR ){
     isAnd = n_ite[0].getKind()==AND;
     for( unsigned i=0; i<n_ite[0].getNumChildren(); i++ ){
       Node cond = n_ite[0][i];
+      orig_conj.push_back( cond );
       if( n_ite[0].getKind()==OR ){
         cond = TermDb::simpleNegate( cond );
       }
@@ -112,12 +117,15 @@ bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::ve
   }else{
     Node neg = n_ite[0].negate();
     if( std::find( conj.begin(), conj.end(), neg )!=conj.end() ){
+      //if negation of condition exists, use it
       isAnd = false;
       curr_conj.push_back( neg );
     }else{
+      //otherwise, use condition
       isAnd = true;
       curr_conj.push_back( n_ite[0] );
     }
+    orig_conj.push_back( n_ite[0] );
   }
   // take intersection with current conditions
   std::vector< Node > new_conj;
@@ -162,13 +170,14 @@ bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::ve
     //make remainder : strip out conditions in conj
     Assert( !conj.empty() );
     std::vector< Node > cond_c;
+    Assert( orig_conj.size()==curr_conj.size() );
     for( unsigned i=0; i<curr_conj.size(); i++ ){
       if( std::find( conj.begin(), conj.end(), curr_conj[i] )==conj.end() ){
-        cond_c.push_back( curr_conj[i] );
+        cond_c.push_back( orig_conj[i] );
       }
     }
     if( cond_c.empty() ){
-      rem = isAnd ? tval : rem;
+      rem = tval;
     }else{
       Node new_cond = cond_c.size()==1 ? cond_c[0] : NodeManager::currentNM()->mkNode( n_ite[0].getKind(), cond_c );
       rem = NodeManager::currentNM()->mkNode( ITE, new_cond, isAnd ? tval : rem, isAnd ? rem : tval );
@@ -309,7 +318,7 @@ Node CegConjectureSingleInvSol::simplifySolution( Node sol, TypeNode stn ){
   }
   Node sol0 = Rewriter::rewrite( sol );
   Trace("csi-sol") << "now : " << sol0 << std::endl;
-  
+
   Node curr_sol = sol0;
   Node prev_sol;
   do{
@@ -359,7 +368,7 @@ Node CegConjectureSingleInvSol::simplifySolution( Node sol, TypeNode stn ){
       curr_sol = sol4;
     }
   }while( curr_sol!=prev_sol );
-  
+
   return curr_sol;
 }
 
@@ -437,7 +446,7 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st
               ret = NodeManager::currentNM()->mkNode( ITE, exp_c, ret[1], ret[2] );
             }
             if( !d_qe->getTermDatabaseSygus()->hasKind( stnc[0], ret[0].getKind() ) ){
-              Trace("csi-sol") << "Flatten based on " << ret[0] << "." << std::endl;
+              Trace("csi-simp-debug") << "Flatten based on " << ret[0] << "." << std::endl;
               ret = flattenITEs( ret, false );
             }
           }
@@ -510,7 +519,7 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st
       }
       if( !new_vars.empty() ){
         if( !inc.empty() ){
-          Node ret = inc.size()==1 ? sol[0] : NodeManager::currentNM()->mkNode( sol.getKind(), inc );
+          Node ret = inc.size()==1 ? inc[0] : NodeManager::currentNM()->mkNode( sol.getKind(), inc );
           Trace("csi-simp") << "Base return is : " << ret << std::endl;
           // apply substitution
           ret = ret.substitute( new_vars.begin(), new_vars.end(), new_subs.begin(), new_subs.end() );
@@ -726,7 +735,7 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in
       if( karg!=-1 ){
         //collect the children of min_t
         std::vector< Node > tchildren;
-        if( min_t.getNumChildren()>dt[karg].getNumArgs() && d_qe->getTermDatabaseSygus()->isAssoc( min_t.getKind() ) && dt[karg].getNumArgs()==2 ){
+        if( min_t.getNumChildren()>dt[karg].getNumArgs() && quantifiers::TermDb::isAssoc( min_t.getKind() ) && dt[karg].getNumArgs()==2 ){
           tchildren.push_back( min_t[0] );
           std::vector< Node > rem_children;
           for( unsigned i=1; i<min_t.getNumChildren(); i++ ){
@@ -848,12 +857,10 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in
                     }
                   }while( !new_t.isNull() );
                 }
+                //get decompositions
                 for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
                   Kind k = d_qe->getTermDatabaseSygus()->getArgKind( stn, i );
-                  if( k==AND || k==OR ){
-                    equiv.push_back( NodeManager::currentNM()->mkNode( k, min_t, min_t ) );
-                    equiv.push_back( NodeManager::currentNM()->mkNode( k, min_t, NodeManager::currentNM()->mkConst( k==AND ) ) );
-                  }
+                  getEquivalentTerms( k, min_t, equiv );
                 }
                 //assign ids to terms
                 Trace("csi-rcons-debug") << "Term " << id << " is equivalent to " << equiv.size() << " terms : " << std::endl;
@@ -1046,4 +1053,62 @@ void CegConjectureSingleInvSol::setReconstructed( int id, Node n ) {
   }
 }
 
+void CegConjectureSingleInvSol::getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv ) {
+  if( k==AND || k==OR ){
+    equiv.push_back( NodeManager::currentNM()->mkNode( k, n, n ) );
+    equiv.push_back( NodeManager::currentNM()->mkNode( k, n, NodeManager::currentNM()->mkConst( k==AND ) ) );
+  }
+  //multiplication for integers
+  //TODO for bitvectors
+  Kind mk = ( k==PLUS || k==MINUS ) ? MULT : UNDEFINED_KIND;
+  if( mk!=UNDEFINED_KIND ){
+    if( n.getKind()==mk && n[0].isConst() && n[0].getType().isInteger() ){
+      bool success = true;
+      for( unsigned i=0; i<2; i++ ){
+        Node eq;
+        if( k==PLUS || k==MINUS ){
+          Node oth = NodeManager::currentNM()->mkConst( Rational(i==0 ? 1000 : -1000) );
+          eq = i==0 ? NodeManager::currentNM()->mkNode( LEQ, n[0], oth ) : NodeManager::currentNM()->mkNode( GEQ, n[0], oth );
+        }
+        if( !eq.isNull() ){
+          eq = Rewriter::rewrite( eq );
+          if( eq!=d_qe->getTermDatabase()->d_true ){
+            success = false;
+            break;
+          }
+        }
+      }
+      if( success ){
+        Node var = n[1];
+        Node rem;
+        if( k==PLUS || k==MINUS ){
+          int rem_coeff = (int)n[0].getConst<Rational>().getNumerator().getSignedInt();
+          if( rem_coeff>0 && k==PLUS ){
+            rem_coeff--;
+          }else if( rem_coeff<0 && k==MINUS ){
+            rem_coeff++;
+          }else{
+            success = false;
+          }
+          if( success ){
+            rem = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(rem_coeff) ), var );
+            rem = Rewriter::rewrite( rem );
+          }
+        }
+        if( !rem.isNull() ){
+          equiv.push_back( NodeManager::currentNM()->mkNode( k, rem, var ) );
+        }
+      }
+    }
+  }
+  //negative constants
+  if( k==MINUS ){
+    if( n.isConst() && n.getType().isInteger() && n.getConst<Rational>().getNumerator().strictlyNegative() ){
+      Node nn = NodeManager::currentNM()->mkNode( UMINUS, n );
+      nn = Rewriter::rewrite( nn );
+      equiv.push_back( NodeManager::currentNM()->mkNode( MINUS, NodeManager::currentNM()->mkConst( Rational(0) ), nn ) );
+    }
+  }  
+}
+  
 }
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.h b/src/theory/quantifiers/ce_guided_single_inv_sol.h
index 6a4b6f90f..1d84986b4 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.h
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.h
@@ -78,6 +78,8 @@ private:
   bool collectReconstructNodes( int pid, std::vector< Node >& ts, const DatatypeConstructor& dtc, std::vector< int >& ids, int& status );
   bool getPathToRoot( int id );
   void setReconstructed( int id, Node n );
+  //get equivalent terms to n with top symbol k
+  void getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv );
 public:
   Node reconstructSolution( Node sol, TypeNode stn, int& reconstructed );
 public:
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 4167c3ad9..da3c0cce0 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -281,61 +281,7 @@ TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) {
 }
 
 Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {
-  Assert( !tn.isNull() );
-  while( d_free_var[tn].size()<=i ){
-    std::stringstream oss;
-    oss << tn;
-    std::string typ_name = oss.str();
-    while( typ_name[0]=='(' ){
-      typ_name.erase( typ_name.begin() );
-    }
-    std::stringstream os;
-    os << typ_name[0] << i;
-    Node x = NodeManager::currentNM()->mkBoundVar( os.str().c_str(), tn );
-    d_free_var_num[x] = d_free_var[tn].size();
-    d_free_var[tn].push_back( x );
-  }
-  return d_free_var[tn][i];
-}
-
-
-
-Node ConjectureGenerator::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs ) {
-  if( n.getKind()==BOUND_VARIABLE ){
-    std::map< TNode, TNode >::iterator it = subs.find( n );
-    if( it==subs.end() ){
-      TypeNode tn = n.getType();
-      //allocate variable
-      unsigned vn = var_count[tn];
-      var_count[tn]++;
-      subs[n] = getFreeVar( tn, vn );
-      return subs[n];
-    }else{
-      return it->second;
-    }
-  }else{
-    std::vector< Node > children;
-    if( n.getKind()!=EQUAL ){
-      if( n.hasOperator() ){
-        TNode op = n.getOperator();
-        if( !d_tge.isRelevantFunc( op ) ){
-          return Node::null();
-        }
-        children.push_back( op );
-      }else{
-        return Node::null();
-      }
-    }
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      Node cn = getCanonicalTerm( n[i], var_count, subs );
-      if( cn.isNull() ){
-        return Node::null();
-      }else{
-        children.push_back( cn );
-      }
-    }
-    return NodeManager::currentNM()->mkNode( n.getKind(), children );
-  }
+  return d_quantEngine->getTermDatabase()->getCanonicalFreeVar( tn, i );
 }
 
 bool ConjectureGenerator::isHandledTerm( TNode n ){
@@ -555,11 +501,14 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
             TNode nr = q[1][r==0 ? 1 : 0];
             Node eq = nl.eqNode( nr );
             if( r==1 || std::find( d_conjectures.begin(), d_conjectures.end(), q )==d_conjectures.end() ){
-              //must make it canonical
-              std::map< TypeNode, unsigned > var_count;
-              std::map< TNode, TNode > subs;
-              Trace("sg-proc-debug") << "get canonical " << eq << std::endl;
-              eq = getCanonicalTerm( eq, var_count, subs );
+              //check if it contains only relevant functions
+              if( d_tge.isRelevantTerm( eq ) ){
+                //make it canonical
+                Trace("sg-proc-debug") << "get canonical " << eq << std::endl;
+                eq = d_quantEngine->getTermDatabase()->getCanonicalTerm( eq );
+              }else{
+                eq = Node::null();
+              }
             }
             if( !eq.isNull() ){
               if( r==0 ){
@@ -697,7 +646,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
                 typ_to_subs_index[it->first] = sum;
                 sum += it->second;
                 for( unsigned i=0; i<it->second; i++ ){
-                  gsubs_vars.push_back( getFreeVar( it->first, i ) );
+                  gsubs_vars.push_back( d_quantEngine->getTermDatabase()->getCanonicalFreeVar( it->first, i ) );
                 }
               }
             }
@@ -993,7 +942,7 @@ unsigned ConjectureGenerator::collectFunctions( TNode opat, TNode pat, std::map<
       }else{
         //check for max/min
         TypeNode tn = pat.getType();
-        unsigned vn = d_free_var_num[pat];
+        unsigned vn = pat.getAttribute(InstVarNumAttribute());
         std::map< TypeNode, unsigned >::iterator it = mnvn.find( tn );
         if( it!=mnvn.end() ){
           if( vn<it->second ){
@@ -1768,15 +1717,18 @@ void TermGenEnv::collectSignatureInformation() {
   for( std::map< Node, TermArgTrie >::iterator it = getTermDatabase()->d_func_map_trie.begin(); it != getTermDatabase()->d_func_map_trie.end(); ++it ){
     if( !getTermDatabase()->d_op_map[it->first].empty() ){
       Node nn = getTermDatabase()->d_op_map[it->first][0];
+      Trace("sg-rel-sig-debug") << "Check in signature : " << nn << std::endl;
       if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){
         bool do_enum = true;
         //check if we have enumerated ground terms
         if( nn.getKind()==APPLY_UF ){
+          Trace("sg-rel-sig-debug") << "Check enumeration..." << std::endl;
           if( !d_cg->hasEnumeratedUf( nn ) ){
             do_enum = false;
           }
         }
         if( do_enum ){
+          Trace("sg-rel-sig-debug") << "Set enumeration..." << std::endl;
           d_funcs.push_back( it->first );
           for( unsigned i=0; i<nn.getNumChildren(); i++ ){
             d_func_args[it->first].push_back( nn[i].getType() );
@@ -1789,6 +1741,7 @@ void TermGenEnv::collectSignatureInformation() {
           getTermDatabase()->computeUfEqcTerms( it->first );
         }
       }
+      Trace("sg-rel-sig-debug") << "Done check in signature : " << nn << std::endl;
     }
   }
   //shuffle functions
@@ -2012,6 +1965,28 @@ bool TermGenEnv::considerCurrentTermCanon( unsigned tg_id ){
 bool TermGenEnv::isRelevantFunc( Node f ) {
   return std::find( d_funcs.begin(), d_funcs.end(), f )!=d_funcs.end();
 }
+
+bool TermGenEnv::isRelevantTerm( Node t ) {
+  if( t.getKind()!=BOUND_VARIABLE ){
+    if( t.getKind()!=EQUAL ){
+      if( t.hasOperator() ){
+        TNode op = t.getOperator();
+        if( !isRelevantFunc( op ) ){
+          return false;
+        }
+      }else{
+        return false;
+      }
+    }
+    for( unsigned i=0; i<t.getNumChildren(); i++ ){
+      if( !isRelevantTerm( t[i] ) ){
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
 TermDb * TermGenEnv::getTermDatabase() {
   return d_cg->getTermDatabase();
 }
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 6f99777f4..3aa932296 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -171,6 +171,7 @@ public:
   bool considerCurrentTermCanon( unsigned tg_id );
   void changeContext( bool add );
   bool isRelevantFunc( Node f );
+  bool isRelevantTerm( Node t );
   //carry
   TermDb * getTermDatabase();
   Node getGroundEqc( TNode r );
@@ -307,14 +308,8 @@ private:  //information regarding the conjectures
   /** conjecture index */
   TheoremIndex d_thm_index;
 private:  //free variable list
-  //free variables
-  std::map< TypeNode, std::vector< Node > > d_free_var;
-  //map from free variable to FV#
-  std::map< TNode, unsigned > d_free_var_num;
   // get canonical free variable #i of type tn
   Node getFreeVar( TypeNode tn, unsigned i );
-  // get canonical term, return null if it contains a term apart from handled signature
-  Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs );
 private:  //information regarding the terms
   //relevant patterns (the LHS's)
   std::map< TypeNode, std::vector< Node > > d_rel_patterns;
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 5cb8cf278..346631889 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -675,10 +675,11 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
       //check if it is a constant introduced as a representative not existing in the model's equality engine
       if( !d_rep_set.hasRep( tn, v ) ){
         if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && !d_rep_set.d_type_reps[ tn ].empty() ){
-          //see full_model_check.cpp line 366
           v = d_rep_set.d_type_reps[tn][ d_rep_set.d_type_reps[tn].size()-1 ];
         }else{
-          Assert( false );
+          //can happen for types not involved in quantified formulas
+          Trace("fmc-model-func") << "No type rep for " << tn << std::endl;
+          v = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 );
         }
         Trace("fmc-model-func") << "No term, assign " << v << std::endl;
       }
diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp
deleted file mode 100644
index 23e18bb02..000000000
--- a/src/theory/quantifiers/first_order_reasoning.cpp
+++ /dev/null
@@ -1,175 +0,0 @@
-/*********************                                                        */
-/*! \file first_order_reasoning.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief first order reasoning module
- **
- **/
-
-#include <vector>
-
-#include "theory/quantifiers/first_order_reasoning.h"
-#include "theory/rewriter.h"
-#include "proof/proof_manager.h"
-
-using namespace CVC4;
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::kind;
-
-
-void FirstOrderPropagation::collectLits( Node n, std::vector<Node> & lits ){
-  if( n.getKind()==FORALL ){
-    collectLits( n[1], lits );
-  }else if( n.getKind()==OR ){
-    for(unsigned j=0; j<n.getNumChildren(); j++) {
-      collectLits(n[j], lits );
-    }
-  }else{
-    lits.push_back( n );
-  }
-}
-
-void FirstOrderPropagation::simplify( std::vector< Node >& assertions ){
-  for( unsigned i=0; i<assertions.size(); i++) {
-    Trace("fo-rsn") << "Assert : " << assertions[i] << std::endl;
-  }
-
-  //process all assertions
-  int num_processed;
-  int num_true = 0;
-  int num_rounds = 0;
-  do {
-    num_processed = 0;
-    for( unsigned i=0; i<assertions.size(); i++ ){
-      if( d_assertion_true.find(assertions[i])==d_assertion_true.end() ){
-        std::vector< Node > fo_lits;
-        collectLits( assertions[i], fo_lits );
-        Node unitLit = process( assertions[i], fo_lits );
-        if( !unitLit.isNull() ){
-          Trace("fo-rsn-debug") << "...possible unit literal : " << unitLit << " from " << assertions[i] << std::endl;
-          bool pol = unitLit.getKind()!=NOT;
-          unitLit = unitLit.getKind()==NOT ? unitLit[0] : unitLit;
-          if( unitLit.getKind()==EQUAL ){
-
-          }else if( unitLit.getKind()==APPLY_UF ){
-            //make sure all are unique vars;
-            bool success = true;
-            std::vector< Node > unique_vars;
-            for( unsigned j=0; j<unitLit.getNumChildren(); j++) {
-              if( unitLit[j].getKind()==BOUND_VARIABLE ){
-                if( std::find(unique_vars.begin(), unique_vars.end(), unitLit[j])==unique_vars.end() ){
-                  unique_vars.push_back( unitLit[j] );
-                }else{
-                  success = false;
-                  break;
-                }
-              }else{
-                success = false;
-                break;
-              }
-            }
-            if( success ){
-              d_const_def[unitLit.getOperator()] = NodeManager::currentNM()->mkConst(pol);
-              Trace("fo-rsn") << "Propagate : " << unitLit.getOperator() << " == " << pol << std::endl;
-              Trace("fo-rsn") << "    from : " << assertions[i] << std::endl;
-              d_assertion_true[assertions[i]] = true;
-              num_processed++;
-            }
-          }else if( unitLit.getKind()==VARIABLE ){
-            d_const_def[unitLit] = NodeManager::currentNM()->mkConst(pol);
-            Trace("fo-rsn") << "Propagate variable : " << unitLit << " == " << pol << std::endl;
-            Trace("fo-rsn") << "    from : " << assertions[i] << std::endl;
-            d_assertion_true[assertions[i]] = true;
-            num_processed++;
-          }
-        }
-        if( d_assertion_true.find(assertions[i])!=d_assertion_true.end() ){
-          num_true++;
-        }
-      }
-    }
-    num_rounds++;
-  }while( num_processed>0 );
-  Trace("fo-rsn-sum") << "Simplified " << num_true << " / " << assertions.size() << " in " << num_rounds << " rounds." << std::endl;
-  for( unsigned i=0; i<assertions.size(); i++ ){
-    Node curr = simplify( assertions[i] );
-    if( curr!=assertions[i] ){
-      curr = Rewriter::rewrite( curr );
-      PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); );
-      assertions[i] = curr;
-    }
-  }
-}
-
-Node FirstOrderPropagation::process(Node a, std::vector< Node > & lits) {
-  int index = -1;
-  for( unsigned i=0; i<lits.size(); i++) {
-    bool pol = lits[i].getKind()!=NOT;
-    Node n = lits[i].getKind()==NOT ? lits[i][0] : lits[i];
-    Node litDef;
-    if( n.getKind()==APPLY_UF ){
-      if( d_const_def.find(n.getOperator())!=d_const_def.end() ){
-        litDef = d_const_def[n.getOperator()];
-      }
-    }else if( n.getKind()==VARIABLE ){
-      if( d_const_def.find(n)!=d_const_def.end() ){
-        litDef = d_const_def[n];
-      }
-    }
-    if( !litDef.isNull() ){
-      Node poln = NodeManager::currentNM()->mkConst( pol );
-      if( litDef==poln ){
-        Trace("fo-rsn-debug") << "Assertion " << a << " is true because of " << lits[i] << std::endl;
-        d_assertion_true[a] = true;
-        return Node::null();
-      }
-    }
-    if( litDef.isNull() ){
-      if( index==-1 ){
-        //store undefined index
-        index = i;
-      }else{
-        //two undefined, return null
-        return Node::null();
-      }
-    }
-  }
-  if( index!=-1 ){
-    return lits[index];
-  }else{
-    return Node::null();
-  }
-}
-
-Node FirstOrderPropagation::simplify( Node n ) {
-  if( n.getKind()==VARIABLE ){
-    if( d_const_def.find(n)!=d_const_def.end() ){
-      return d_const_def[n];
-    }
-  }else if( n.getKind()==APPLY_UF ){
-    if( d_const_def.find(n.getOperator())!=d_const_def.end() ){
-      return d_const_def[n.getOperator()];
-    }
-  }
-  if( n.getNumChildren()==0 ){
-    return n;
-  }else{
-    std::vector< Node > children;
-    if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-      children.push_back( n.getOperator() );
-    }
-    for(unsigned i=0; i<n.getNumChildren(); i++) {
-      children.push_back( simplify(n[i]) );
-    }
-    return NodeManager::currentNM()->mkNode( n.getKind(), children );
-  }
-}
diff --git a/src/theory/quantifiers/first_order_reasoning.h b/src/theory/quantifiers/first_order_reasoning.h
deleted file mode 100644
index 100cf34b6..000000000
--- a/src/theory/quantifiers/first_order_reasoning.h
+++ /dev/null
@@ -1,49 +0,0 @@
-/*********************                                                        */
-/*! \file first_order_reasoning.h
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Pre-process step for first-order reasoning
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__FIRST_ORDER_REASONING_H
-#define __CVC4__FIRST_ORDER_REASONING_H
-
-#include <iostream>
-#include <string>
-#include <vector>
-#include <map>
-#include "expr/node.h"
-#include "expr/type_node.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class FirstOrderPropagation {
-private:
-  std::map< Node, Node > d_const_def;
-  std::map< Node, bool > d_assertion_true;
-  Node process(Node a, std::vector< Node > & lits);
-  void collectLits( Node n, std::vector<Node> & lits );
-  Node simplify( Node n );
-public:
-  FirstOrderPropagation(){}
-  ~FirstOrderPropagation(){}
-
-  void simplify( std::vector< Node >& assertions );
-};
-
-}
-}
-}
-
-#endif
diff --git a/src/theory/quantifiers/fun_def_engine.cpp b/src/theory/quantifiers/fun_def_engine.cpp
new file mode 100644
index 000000000..56214f540
--- /dev/null
+++ b/src/theory/quantifiers/fun_def_engine.cpp
@@ -0,0 +1,54 @@
+/*********************                                                        */
+/*! \file fun_def_process.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** This class implements specialized techniques for (recursively) defined functions
+ **/
+
+#include <vector>
+
+#include "theory/quantifiers/fun_def_engine.h"
+#include "theory/rewriter.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace CVC4;
+using namespace std;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::kind;
+
+FunDefEngine::FunDefEngine( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ) {
+  
+}
+
+/* whether this module needs to check this round */
+bool FunDefEngine::needsCheck( Theory::Effort e ) { 
+  return e>=Theory::EFFORT_LAST_CALL; 
+}
+
+/* reset at a round */
+void FunDefEngine::reset_round( Theory::Effort e ){
+  //TODO
+}
+
+/* Call during quantifier engine's check */
+void FunDefEngine::check( Theory::Effort e, unsigned quant_e ) {
+  //TODO
+}
+
+/* Called for new quantifiers */
+void FunDefEngine::registerQuantifier( Node q ) {
+  //TODO
+}
+
+/** called for everything that gets asserted */
+void FunDefEngine::assertNode( Node n ) {
+  //TODO
+}
diff --git a/src/theory/quantifiers/fun_def_engine.h b/src/theory/quantifiers/fun_def_engine.h
new file mode 100644
index 000000000..be73d51a9
--- /dev/null
+++ b/src/theory/quantifiers/fun_def_engine.h
@@ -0,0 +1,59 @@
+/*********************                                                        */
+/*! \file fun_def_engine.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Specialized techniques for (recursively) defined functions
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__QUANTIFIERS_FUN_DEF_ENGINE_H
+#define __CVC4__QUANTIFIERS_FUN_DEF_ENGINE_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <map>
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+//module for handling (recursively) defined functions
+class FunDefEngine : public QuantifiersModule {
+private:
+
+public:
+  FunDefEngine( QuantifiersEngine * qe, context::Context* c );
+  ~FunDefEngine(){}
+
+  /* whether this module needs to check this round */
+  bool needsCheck( Theory::Effort e );
+  /* reset at a round */
+  void reset_round( Theory::Effort e );
+  /* Call during quantifier engine's check */
+  void check( Theory::Effort e, unsigned quant_e );
+  /* Called for new quantifiers */
+  void registerQuantifier( Node q );
+  /** called for everything that gets asserted */
+  void assertNode( Node n );
+  /** Identify this module (for debugging, dynamic configuration, etc..) */
+  std::string identify() const { return "FunDefEngine"; }
+};
+
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 941eaf89b..f7dc709d9 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -463,13 +463,17 @@ bool VarMatchGeneratorTermSubs::getNextMatch( Node f, InstMatch& m, QuantifiersE
     s = Rewriter::rewrite( s );
     Trace("var-trigger-matching") << "...got " << s << std::endl;
     d_eq_class = Node::null();
-    d_rm_prev = m.get( d_var_num[0] ).isNull();
-    if( !m.set( qe, d_var_num[0], s ) ){
-      return false;
-    }else{
-      if( continueNextMatch( f, m, qe ) ){
-        return true;
+    if( s.getType().isSubtypeOf( d_var.getType() ) ){
+      d_rm_prev = m.get( d_var_num[0] ).isNull();
+      if( !m.set( qe, d_var_num[0], s ) ){
+        return false;
+      }else{
+        if( continueNextMatch( f, m, qe ) ){
+          return true;
+        }
       }
+    }else{
+      Trace("var-trigger-matching") << "Violates type requirement." << std::endl;
     }
   }
   if( d_rm_prev ){
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index cbf0dbbd9..dab32af71 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -126,9 +126,9 @@ void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder<
 }
 
 int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
-  if( e<2 ){
+  if( e<1 ){
     return STATUS_UNFINISHED;
-  }else if( e==2 ){
+  }else if( e==1 ){
     if( d_quantActive.find( f )!=d_quantActive.end() ){
       //the point instantiation
       InstMatch m_point( f );
@@ -369,12 +369,13 @@ InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategy( q
 
 void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) {
   d_check_delta_lemma = true;
+  d_check_delta_lemma_lc = true;
 }
 
 int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
-  if( e<2 ){
+  if( e<1 ){
     return STATUS_UNFINISHED;
-  }else if( e==2 ){
+  }else if( e==1 ){
     CegInstantiator * cinst;
     std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( f );
     if( it==d_cinst.end() ){
@@ -383,6 +384,9 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
         d_n_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for cegqi inst strategy" );
         Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) );
         d_quantEngine->getOutputChannel().lemma( delta_lem );
+        d_n_delta_ub = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) );
+        Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, d_n_delta, d_n_delta_ub );
+        d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
       }
       cinst->d_n_delta = d_n_delta;
       for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
@@ -412,8 +416,19 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
     }
     Trace("inst-alg") << "-> Run cegqi for " << f << std::endl;
     d_curr_quant = f;
-    cinst->check();
+    bool addedLemma = cinst->check();
+    d_used_delta = d_used_delta || cinst->d_used_delta;
     d_curr_quant = Node::null();
+    return addedLemma ? STATUS_UNKNOWN : STATUS_UNFINISHED;
+  }else if( e==2 ){
+    if( d_check_delta_lemma_lc && d_used_delta ){
+      d_check_delta_lemma_lc = false;
+      d_n_delta_ub = NodeManager::currentNM()->mkNode( MULT, d_n_delta_ub, d_n_delta_ub );
+      d_n_delta_ub = Rewriter::rewrite( d_n_delta_ub );
+      Trace("cegqi") << "Delta lemma for " << d_n_delta_ub << std::endl;
+      Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, d_n_delta, d_n_delta_ub );
+      d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
+    }
   }
   return STATUS_UNKNOWN;
 }
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 586cd492c..d59690c84 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -100,8 +100,11 @@ private:
   CegqiOutputInstStrategy * d_out;
   std::map< Node, CegInstantiator * > d_cinst;
   Node d_n_delta;
+  Node d_n_delta_ub;
   Node d_curr_quant;
   bool d_check_delta_lemma;
+  bool d_check_delta_lemma_lc;
+  bool d_used_delta;
   /** process functions */
   void processResetInstantiationRound( Theory::Effort effort );
   int process( Node f, Theory::Effort effort, int e );
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 81771c374..8958034df 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -467,12 +467,13 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
   }else{
     //first, try from relevant domain
     RelevantDomain * rd = d_quantEngine->getRelevantDomain();
-    for( unsigned r=0; r<2; r++ ){
-      if( rd || r==1 ){
+    unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1;
+    for( unsigned r=rstart; r<2; r++ ){
+      if( rd || r>0 ){
         if( r==0 ){
           Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl;
         }else{
-          Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
+          Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl;
         }
         rd->compute();
         unsigned final_max_i = 0;
@@ -550,6 +551,7 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
         }
       }
       if( r==0 ){
+        //complete guess
         if( d_guessed.find( f )==d_guessed.end() ){
           Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
           d_guessed[f] = true;
@@ -561,6 +563,7 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
         }
       }
     }
+    //term enumerator?
   }
   return STATUS_UNKNOWN;
 }
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 4fbf298f4..631216507 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -66,11 +66,10 @@ void InstantiationEngine::finishInit(){
 
   //counterexample-based quantifier instantiation
   if( options::cbqi() ){
-    if( !options::cbqi2() || options::cbqi.wasSetByUser() ){
+    if( !options::cbqi2() ){
       d_i_splx = new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine );
       d_instStrategies.push_back( d_i_splx );
-    }
-    if( options::cbqi2() ){
+    }else{
       d_i_cegqi = new InstStrategyCegqi( d_quantEngine );
       d_instStrategies.push_back( d_i_cegqi );
     }
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 53f55e70b..e297e138c 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -176,7 +176,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
         }
 
         //if applicable, find exceptions to model via inst-gen
-        if( optInstGen() ){
+        if( options::fmfInstGen() ){
           d_didInstGen = true;
           d_instGenMatches = 0;
           d_numQuantSat = 0;
@@ -201,7 +201,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
               }else{
                 d_numQuantNoSelForm++;
               }
-              if( optOneQuantPerRoundInstGen() && lems>0 ){
+              if( options::fmfInstGenOneQuantPerRound() && lems>0 ){
                 break;
               }
             }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){
@@ -341,14 +341,6 @@ bool QModelBuilderIG::hasConstantDefinition( Node n ){
   return false;
 }
 
-bool QModelBuilderIG::optInstGen(){
-  return options::fmfInstGen();
-}
-
-bool QModelBuilderIG::optOneQuantPerRoundInstGen(){
-  return options::fmfInstGenOneQuantPerRound();
-}
-
 QModelBuilderIG::Statistics::Statistics():
   d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0),
   d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0),
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index d9ed3f092..8e84f15e2 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -123,10 +123,6 @@ public:
   QModelBuilderIG( context::Context* c, QuantifiersEngine* qe );
   virtual ~QModelBuilderIG() throw() {}
 public:
-  //whether to add inst-gen lemmas
-  virtual bool optInstGen();
-  //whether to only consider only quantifier per round of inst-gen
-  virtual bool optOneQuantPerRoundInstGen();
   /** statistics class */
   class Statistics {
   public:
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index ce780a29b..2ad8be3a1 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -157,15 +157,19 @@ int ModelEngine::checkModel(){
       if( it->first.isSort() ){
         Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
         if( Trace.isOn("model-engine-debug") ){
-          Trace("model-engine-debug") << "   ";
-          Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
+          Trace("model-engine-debug") << "        Reps : ";
+          for( size_t i=0; i<it->second.size(); i++ ){
+            Trace("model-engine-debug") << it->second[i] << "  ";
+          }
+          Trace("model-engine-debug") << std::endl;
+          Trace("model-engine-debug") << "   Term reps : ";
           for( size_t i=0; i<it->second.size(); i++ ){
-            //Trace("model-engine-debug") << it->second[i] << "  ";
             Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 );
             Trace("model-engine-debug") << r << " ";
           }
           Trace("model-engine-debug") << std::endl;
-          Trace("model-engine-debug") << "  Model basis term : " << mbt << std::endl;
+          Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
+          Trace("model-engine-debug") << "  Basis term : " << mbt << std::endl;
         }
       }
     }
@@ -200,6 +204,7 @@ int ModelEngine::checkModel(){
         for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
           Node f = fm->getAssertedQuantifier( i );
           bool isAx = getTermDatabase()->isQAttrAxiom( f );
+          Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl;
           //determine if we should check this quantifier
           if( ( ( effort==1 && ( options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT || isAx ) ) || ( effort==0 && !isAx ) ) && mb->isQuantifierActive( f ) ){
             exhaustiveInstantiate( f, e );
@@ -214,7 +219,7 @@ int ModelEngine::checkModel(){
               break;
             }
           }else{
-            Trace("inst-fmf-ei") << "-> Inactive : " << f << std::endl;
+            Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl;
           }
         }
       }
@@ -240,43 +245,46 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
   mb->d_addedLemmas = 0;
   mb->d_incomplete_check = false;
   if( mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){
-    Trace("inst-fmf-ei") << "-> Builder determined instantiation(s)." << std::endl;
+    Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl;
     d_triedLemmas += mb->d_triedLemmas;
     d_addedLemmas += mb->d_addedLemmas;
     d_incomplete_check = d_incomplete_check || mb->d_incomplete_check;
     d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas;
   }else{
-    Trace("inst-fmf-ei") << "-> Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl;
-    Debug("inst-fmf-ei") << "   Instantiation Constants: ";
+    Trace("fmf-exh-inst-debug") << "   Instantiation Constants: ";
     for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-      Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
+      Trace("fmf-exh-inst-debug") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
     }
-    Debug("inst-fmf-ei") << std::endl;
+    Trace("fmf-exh-inst-debug") << std::endl;
     //create a rep set iterator and iterate over the (relevant) domain of the quantifier
     RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
     if( riter.setQuantifier( f ) ){
-      Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
-      int triedLemmas = 0;
-      int addedLemmas = 0;
-      while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
-        //instantiation was not shown to be true, construct the match
-        InstMatch m( f );
-        for( int i=0; i<riter.getNumTerms(); i++ ){
-          m.set( d_quantEngine, riter.d_index_order[i], riter.getTerm( i ) );
-        }
-        Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
-        triedLemmas++;
-        //add as instantiation
-        if( d_quantEngine->addInstantiation( f, m ) ){
-          addedLemmas++;
-        }else{
-          Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
+      Trace("fmf-exh-inst") << "...exhaustive instantiation incomplete=" << riter.d_incomplete << "..." << std::endl;
+      if( !riter.d_incomplete || options::fmfFullSaturate() ){
+        int triedLemmas = 0;
+        int addedLemmas = 0;
+        while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
+          //instantiation was not shown to be true, construct the match
+          InstMatch m( f );
+          for( int i=0; i<riter.getNumTerms(); i++ ){
+            m.set( d_quantEngine, riter.d_index_order[i], riter.getTerm( i ) );
+          }
+          Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
+          triedLemmas++;
+          //add as instantiation
+          if( d_quantEngine->addInstantiation( f, m ) ){
+            addedLemmas++;
+          }else{
+            Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
+          }
+          riter.increment();
         }
-        riter.increment();
+        d_addedLemmas += addedLemmas;
+        d_triedLemmas += triedLemmas;
+        d_statistics.d_exh_inst_lemmas += addedLemmas;
       }
-      d_addedLemmas += addedLemmas;
-      d_triedLemmas += triedLemmas;
-      d_statistics.d_exh_inst_lemmas += addedLemmas;
+    }else{
+      Assert( riter.d_incomplete );
     }
     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
     d_incomplete_check = d_incomplete_check || riter.d_incomplete;
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 47cb62715..af2d88e94 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -143,6 +143,23 @@ typedef enum {
   TERM_DB_RELEVANT,
 } TermDbMode;
 
+typedef enum {
+  /** do not lift ITEs in quantified formulas */
+  ITE_LIFT_QUANT_MODE_NONE,
+  /** only lift ITEs in quantified formulas if reduces the term size */
+  ITE_LIFT_QUANT_MODE_SIMPLE,
+  /** lift ITEs  */
+  ITE_LIFT_QUANT_MODE_ALL,
+} IteLiftQuantMode;
+
+typedef enum {
+  /** synthesize I( x ) */
+  SYGUS_INV_TEMPL_MODE_NONE,
+  /** synthesize ( pre( x ) V I( x ) ) */
+  SYGUS_INV_TEMPL_MODE_PRE,
+  /** synthesize ( post( x ) ^ I( x ) ) */
+  SYGUS_INV_TEMPL_MODE_POST,
+} SygusInvTemplMode;
 
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index fe81df7f8..5cb9062e4 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -19,7 +19,7 @@ option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write
  disable miniscope quantifiers for ground subformulas
 # Whether to prenex (nested universal) quantifiers
 option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToPrenexQuantMode :handler-include "theory/quantifiers/options_handlers.h"
- disable prenexing of quantified formulas
+ prenex mode for quantified formulas
 # Whether to variable-eliminate quantifiers.
 # For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to
 #   forall y. P( c, y )
@@ -27,13 +27,16 @@ option varElimQuant --var-elim-quant bool :default true
  disable simple variable elimination for quantified formulas
 option dtVarExpandQuant --dt-var-exp-quant bool :default true
  expand datatype variables bound to one constructor in quantifiers
+#ite lift mode for quantified formulas
+option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuantMode :default CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToIteLiftQuantMode :handler-include "theory/quantifiers/options_handlers.h"
+ ite lifting mode for quantified formulas
 option iteCondVarSplitQuant --ite-cond-var-split-quant bool :default true
  split variables occurring as conditions of ITE in quantifiers
-option simpleIteLiftQuant --ite-lift-quant bool :default true
- disable simple ite lifting for quantified formulas
+option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default false
+ split ites with dt testers as conditions
 # Whether to CNF quantifier bodies
-option cnfQuant --cnf-quant bool :default false
- apply CNF conversion to quantified formulas
+# option cnfQuant --cnf-quant bool :default false
+#  apply CNF conversion to quantified formulas
 # Whether to NNF quantifier bodies
 option nnfQuant --nnf-quant bool :default true
  apply NNF conversion to quantified formulas
@@ -54,10 +57,10 @@ option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
 # Whether to perform quantifier macro expansion
 option macrosQuant --macros-quant bool :default false
  perform quantifiers macro expansions
-# Whether to perform first-order propagation
-option foPropQuant --fo-prop-quant bool :default false
- perform first-order propagation on quantifiers
-
+# Whether to CNF quantifier bodies
+option elimTautQuant --elim-taut-quant bool :default true
+ eliminate tautological disjuncts of quantified formulas
+ 
 #### E-matching options
  
 option eMatching --e-matching bool :read-write :default true
@@ -83,6 +86,8 @@ option purifyDtTriggers --purify-dt-triggers bool :default false :read-write
  purify dt triggers, match all constructors of correct form instead of selectors
 option pureThTriggers --pure-th-triggers bool :default false :read-write
  use pure theory terms as single triggers
+option partialTriggers --partial-triggers bool :default false :read-write
+ use triggers that do not contain all free variables
 option multiTriggerWhenSingle --multi-trigger-when-single bool :default false
  select multi triggers when single triggers exist
 option multiTriggerPriority --multi-trigger-priority bool :default false
@@ -110,6 +115,8 @@ option eagerInstQuant --eager-inst-quant bool :default false
 
 option fullSaturateQuant --full-saturate-quant bool :default false
  when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown
+option fullSaturateQuantRd --full-saturate-quant-rd bool :default true
+ whether to use relevant domain first for full saturation instantiation strategy
 
 option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h"
  choose literal matching mode
@@ -137,8 +144,10 @@ option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
 
 option fmfInstEngine --fmf-inst-engine bool :default false
  use instantiation engine in conjunction with finite model finding
+option fmfFullSaturate --fmf-full-saturate bool :default false
+ instantiate with all known ground terms for infinite domain quantifiers when finite model finding
 option fmfInstGen --fmf-inst-gen bool :default true
- disable Inst-Gen instantiation techniques for finite model finding
+ disable Inst-Gen instantiation techniques for finite model finding 
 option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false
  only perform Inst-Gen instantiation techniques on one quantifier per round
 option fmfFreshDistConst --fmf-fresh-dc bool :default false
@@ -160,6 +169,8 @@ option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :
  when to invoke conflict find mechanism for quantifiers
 option qcfTConstraint --qcf-tconstraint bool :read-write :default false
  enable entailment checks for t-constraints in qcf algorithm
+option qcfAllConflict --qcf-all-conflict bool :read-write :default false
+ add all available conflicting instances during conflict-based instantiation
 
 option instNoEntail --inst-no-entail bool :read-write :default true
  do not consider instances of quantified formulas that are currently entailed
@@ -192,7 +203,7 @@ option conjectureFilterCanonical --conjecture-filter-canonical bool :read-write
  filter based on canonicity
 option conjectureFilterModel --conjecture-filter-model bool :read-write :default true
  filter based on model
-option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 0
+option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 50
  number of ground terms to generate for model filtering
 option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false
  more aggressive merging for universal equality engine, introduces terms
@@ -209,8 +220,12 @@ option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true
   reconstruct solutions for single invocation conjectures in original grammar
 option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true
   include constants when reconstruct solutions for single invocation conjectures in original grammar
+option cegqiSingleInvPreRegInst --cegqi-si-prereg-inst bool :default true
+  preregister ground instantiations when single invocation
 option cegqiSingleInvAbort --cegqi-si-abort bool :default false
-  abort if our synthesis conjecture is not single invocation
+  abort if synthesis conjecture is not single invocation
+option cegqiSingleInvMultiInstAbort --cegqi-si-multi-inst-abort bool :default false
+  abort if synthesis conjecture is single invocation with no ITE in grammar and multiple instantiations are tried
   
 option sygusNormalForm --sygus-nf bool :default true
   only search for sygus builtin terms that are in normal form
@@ -225,7 +240,10 @@ option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true
 option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true
   generalize based on content in global search space narrowing
   
-# older implementation
+option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToSygusInvTemplMode :handler-include "theory/quantifiers/options_handlers.h"
+  template mode for sygus invariant synthesis
+
+# approach applied to general quantified formulas
 option cbqi --cbqi bool :read-write :default false
  turns on counterexample-based quantifier instantiation
 option cbqi2 --cbqi2 bool :read-write :default false
@@ -244,4 +262,14 @@ option ltePartialInst --lte-partial-inst bool :default false
 option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false
   treat arguments of inst closure as restricted terms for instantiation
  
+### reduction options
+
+option quantAlphaEquiv --quant-alpha-equiv bool :default true
+  infer alpha equivalence between quantified formulas
+
+### recursive function options
+
+#option funDefs --fun-defs bool :default false
+#  enable specialized techniques for recursive function definitions
+ 
 endmodule
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 9fb5dd69d..4d2276621 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -204,6 +204,32 @@ relevant \n\
 + Quantifiers module considers only ground terms connected to current assertions. \n\
 \n\
 ";
+static const std::string iteLiftQuantHelp = "\
+Modes for term database, supported by --ite-lift-quant:\n\
+\n\
+all  \n\
++ Do not lift if-then-else in quantified formulas.\n\
+\n\
+simple  \n\
++ Lift if-then-else in quantified formulas if results in smaller term size.\n\
+\n\
+none \n\
++ Lift if-then-else in quantified formulas. \n\
+\n\
+";
+static const std::string sygusInvTemplHelp = "\
+Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\
+\n\
+none  \n\
++ Synthesize invariant directly.\n\
+\n\
+pre  \n\
++ Synthesize invariant based on weakening of precondition .\n\
+\n\
+post \n\
++ Synthesize invariant based on strengthening of postcondition. \n\
+\n\
+";
 
 inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg == "pre-full") {
@@ -414,6 +440,38 @@ inline TermDbMode stringToTermDbMode(std::string option, std::string optarg, Smt
   }
 }
 
+inline IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "all" ) {
+    return ITE_LIFT_QUANT_MODE_ALL;
+  } else if(optarg == "simple") {
+    return ITE_LIFT_QUANT_MODE_SIMPLE;
+  } else if(optarg == "none") {
+    return ITE_LIFT_QUANT_MODE_NONE;
+  } else if(optarg ==  "help") {
+    puts(iteLiftQuantHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --ite-lift-quant: `") +
+                          optarg + "'.  Try --ite-lift-quant help.");
+  }
+}
+
+inline SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "none" ) {
+    return SYGUS_INV_TEMPL_MODE_NONE;
+  } else if(optarg == "pre") {
+    return SYGUS_INV_TEMPL_MODE_PRE;
+  } else if(optarg == "post") {
+    return SYGUS_INV_TEMPL_MODE_POST;
+  } else if(optarg ==  "help") {
+    puts(sygusInvTemplHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --sygus-inv-templ: `") +
+                          optarg + "'.  Try --sygus-inv-templ help.");
+  }
+}
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 18bffe908..47c2e1c5b 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1971,6 +1971,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
         Trace("qcf-debug") << std::endl;
       }
       short end_e = getMaxQcfEffort();
+      bool isConflict = false;
       for( short e = effort_conflict; e<=end_e; e++ ){
         d_effort = e;
         Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;
@@ -2014,8 +2015,12 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                       ++addedLemmas;
                       if( e==effort_conflict ){
                         d_quant_order.insert( d_quant_order.begin(), q );
-                        d_conflict.set( true );
                         ++(d_statistics.d_conflict_inst);
+                        if( options::qcfAllConflict() ){
+                          isConflict = true;
+                        }else{
+                          d_conflict.set( true );
+                        }
                         break;
                       }else if( e==effort_prop_eq ){
                         ++(d_statistics.d_prop_inst);
@@ -2044,6 +2049,9 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
           break;
         }
       }
+      if( isConflict ){
+        d_conflict.set( true );
+      }
       if( Trace.isOn("qcf-engine") ){
         double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
         Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet);
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index ca24de5f7..5e0f511e0 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -110,8 +110,6 @@ public:
   virtual eq::EqualityEngine* getEngine() = 0;
   /** get the equivalence class of a */
   virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
-
-  virtual void setLiberal( bool l ) = 0;
 };/* class EqualityQuery */
 
 
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 0afdece82..6a95e243d 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -340,64 +340,141 @@ Node QuantifiersRewriter::computeNNF( Node body ){
   }
 }
 
+
+void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, 
+                                                   std::vector< Node >& conj ){
+  if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){
+  Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl;
+    Node x = n[0][0];
+    std::map< Node, Node >::iterator itp = pcons.find( x );
+    if( itp!=pcons.end() ){
+      Trace("quantifiers-rewrite-ite-debug") << "...condition already set " << itp->second << std::endl;
+      computeDtTesterIteSplit( n[ itp->second==n[0] ? 1 : 2 ], pcons, ncons, conj );
+    }else{
+      Expr testerExpr = n[0].getOperator().toExpr();
+      int index = Datatype::indexOf( testerExpr );
+      std::map< int, Node >::iterator itn = ncons[x].find( index );
+      if( itn!=ncons[x].end() ){
+        Trace("quantifiers-rewrite-ite-debug") << "...condition negated " << itn->second << std::endl;
+        computeDtTesterIteSplit( n[ 2 ], pcons, ncons, conj );
+      }else{
+        for( unsigned i=0; i<2; i++ ){
+          if( i==0 ){
+            pcons[x] = n[0];
+          }else{
+            pcons.erase( x );
+            ncons[x][index] = n[0].negate();
+          }
+          computeDtTesterIteSplit( n[i+1], pcons, ncons, conj );
+        }
+        ncons[x].erase( index );
+      }
+    }
+  }else{
+    Trace("quantifiers-rewrite-ite-debug") << "Return value : " << n << std::endl;
+    std::vector< Node > children;
+    children.push_back( n );
+    std::vector< Node > vars;
+    //add all positive testers 
+    for( std::map< Node, Node >::iterator it = pcons.begin(); it != pcons.end(); ++it ){
+      children.push_back( it->second.negate() );
+      vars.push_back( it->first );
+    }
+    //add all negative testers
+    for( std::map< Node, std::map< int, Node > >::iterator it = ncons.begin(); it != ncons.end(); ++it ){
+      Node x = it->first;
+      //only if we haven't settled on a positive tester
+      if( std::find( vars.begin(), vars.end(), x )==vars.end() ){
+        //check if we have exhausted all options but one
+        const Datatype& dt = DatatypeType(x.getType().toType()).getDatatype();
+        std::vector< Node > nchildren;
+        int pos_cons = -1;
+        for( int i=0; i<(int)dt.getNumConstructors(); i++ ){
+          std::map< int, Node >::iterator itt = it->second.find( i );
+          if( itt==it->second.end() ){
+            pos_cons = pos_cons==-1 ? i : -2;
+          }else{
+            nchildren.push_back( itt->second.negate() );
+          }
+        }
+        if( pos_cons>=0 ){
+          const DatatypeConstructor& c = dt[pos_cons];
+          Expr tester = c.getTester();
+          children.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), x ).negate() );
+        }else{
+          children.insert( children.end(), nchildren.begin(), nchildren.end() );
+        }
+      }
+    }
+    //make condition/output pair
+    Node c = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children );
+    conj.push_back( c );
+  }
+}
+
 Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol ) {
   if( body.getType().isBoolean() ){
-    if( body.getKind()==EQUAL && options::simpleIteLiftQuant() ){
+    if( body.getKind()==EQUAL && options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE ){
       for( size_t i=0; i<2; i++ ){
         if( body[i].getKind()==ITE ){
           Node no = i==0 ? body[1] : body[0];
-          bool doRewrite = false;
-          std::vector< Node > children;
-          children.push_back( body[i][0] );
-          for( size_t j=1; j<=2; j++ ){
-            //check if it rewrites to a constant
-            Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] );
-            nn = Rewriter::rewrite( nn );
-            children.push_back( nn );
-            if( nn.isConst() ){
-              doRewrite = true;
+          if( no.getKind()!=ITE ){
+            bool doRewrite = options::iteLiftQuant()==ITE_LIFT_QUANT_MODE_ALL;
+            std::vector< Node > children;
+            children.push_back( body[i][0] );
+            for( size_t j=1; j<=2; j++ ){
+              //check if it rewrites to a constant
+              Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] );
+              nn = Rewriter::rewrite( nn );
+              children.push_back( nn );
+              if( nn.isConst() ){
+                doRewrite = true;
+              }
+            }
+            if( doRewrite ){
+              return NodeManager::currentNM()->mkNode( ITE, children );
             }
-          }
-          if( doRewrite ){
-            return NodeManager::currentNM()->mkNode( ITE, children );
           }
         }
       }
-    }else if( body.getKind()==ITE && hasPol && options::iteCondVarSplitQuant() ){
-      for( unsigned r=0; r<2; r++ ){
-        //check if there is a variable elimination
-        Node b = r==0 ? body[0] : body[0].negate();
-        QuantPhaseReq qpr( b );
-        std::vector< Node > vars;
-        std::vector< Node > subs;
-        Trace("ite-var-split-quant") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl;
-        for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
-          Trace("ite-var-split-quant") << "phase req " << it->first << " -> " << it->second << std::endl;
-          if( it->second ){
-            if( it->first.getKind()==EQUAL ){
-              for( unsigned i=0; i<2; i++ ){
-                if( it->first[i].getKind()==BOUND_VARIABLE ){
-                  unsigned j = i==0 ? 1 : 0;
-                  if( !hasArg1( it->first[i], it->first[j] ) ){
-                    vars.push_back( it->first[i] );
-                    subs.push_back( it->first[j] );
-                    break;
+    }else if( body.getKind()==ITE && hasPol ){
+      if( options::iteCondVarSplitQuant() ){
+        Trace("quantifiers-rewrite-ite-debug") << "Conditional var eq split " << body << std::endl;
+        for( unsigned r=0; r<2; r++ ){
+          //check if there is a variable elimination
+          Node b = r==0 ? body[0] : body[0].negate();
+          QuantPhaseReq qpr( b );
+          std::vector< Node > vars;
+          std::vector< Node > subs;
+          Trace("quantifiers-rewrite-ite-debug") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl;
+          for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
+            Trace("quantifiers-rewrite-ite-debug") << "phase req " << it->first << " -> " << it->second << std::endl;
+            if( it->second ){
+              if( it->first.getKind()==EQUAL ){
+                for( unsigned i=0; i<2; i++ ){
+                  if( it->first[i].getKind()==BOUND_VARIABLE ){
+                    unsigned j = i==0 ? 1 : 0;
+                    if( !hasArg1( it->first[i], it->first[j] ) ){
+                      vars.push_back( it->first[i] );
+                      subs.push_back( it->first[j] );
+                      break;
+                    }
                   }
                 }
               }
             }
           }
-        }
-        if( !vars.empty() ){
-          //bool cpol = (r==1);
-          Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] );
-          //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-          //pos = Rewriter::rewrite( pos );
-          Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] );
-          //Trace("ite-var-split-quant") << "Split ITE " << body << " into : " << std::endl;
-          //Trace("ite-var-split-quant") << "   " << pos << std::endl;
-          //Trace("ite-var-split-quant") << "   " << neg << std::endl;
-          return NodeManager::currentNM()->mkNode( AND, pos, neg );
+          if( !vars.empty() ){
+            //bool cpol = (r==1);
+            Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] );
+            //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+            //pos = Rewriter::rewrite( pos );
+            Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] );
+            Trace("quantifiers-rewrite-ite") << "*** Split ITE (conditional variable eq) " << body << " into : " << std::endl;
+            Trace("quantifiers-rewrite-ite") << "   " << pos << std::endl;
+            Trace("quantifiers-rewrite-ite") << "   " << neg << std::endl;
+            return NodeManager::currentNM()->mkNode( AND, pos, neg );
+          }
         }
       }
     }
@@ -420,6 +497,26 @@ Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol )
   return body;
 }
 
+Node QuantifiersRewriter::computeProcessIte2( Node body ){
+  if( body.getKind()==ITE ){
+    if( options::iteDtTesterSplitQuant() ){
+      Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl;
+      std::map< Node, Node > pcons;
+      std::map< Node, std::map< int, Node > > ncons;
+      std::vector< Node > conj;
+      computeDtTesterIteSplit( body, pcons, ncons, conj );
+      Assert( !conj.empty() );
+      if( conj.size()>1 ){
+        Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body << " into : " << std::endl;
+        for( unsigned i=0; i<conj.size(); i++ ){
+          Trace("quantifiers-rewrite-ite") << "   " << conj[i] << std::endl;
+        }
+        return NodeManager::currentNM()->mkNode( AND, conj );
+      }
+    }
+  }
+  return body;
+}
 
 
 Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){
@@ -677,6 +774,30 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
   }
 }
 
+Node QuantifiersRewriter::computeElimTaut( Node body ) {
+  if( body.getKind()==OR ){
+    std::vector< Node > children;
+    std::map< Node, bool > lit_pol;
+    for( unsigned i=0; i<body.getNumChildren(); i++ ){
+      Node lit = body[i].getKind()==NOT ? body[i][0] : body[i];
+      bool pol = body[i].getKind()!=NOT;
+      std::map< Node, bool >::iterator it = lit_pol.find( lit );
+      if( it==lit_pol.end() ){
+        lit_pol[lit] = pol;
+        children.push_back( body[i] );
+      }else{
+        if( it->second!=pol ){
+          return NodeManager::currentNM()->mkConst( true );
+        }
+      }
+    }
+    if( children.size()!=body.getNumChildren() ){
+      return children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children );
+    }
+  }
+  return body;
+}
+  
 Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >& vars ) {
   if( body.getKind()==OR ){
     size_t var_found_count = 0;
@@ -784,7 +905,21 @@ Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >&
 
 Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){
   std::vector< Node > activeArgs;
-  computeArgVec2( args, activeArgs, body, ipl );
+  //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables 
+  if( options::ceGuidedInst() && !ipl.isNull() ){
+    for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
+      Trace("quant-attr-debug") << "Check : " << ipl[i] << " " << ipl[i].getKind() << std::endl;
+      if( ipl[i].getKind()==INST_ATTRIBUTE ){
+        Node avar = ipl[i][0];
+        if( avar.getAttribute(SygusAttribute()) ){
+          activeArgs.insert( activeArgs.end(), args.begin(), args.end() );
+        }
+      }
+    }
+  }
+  if( activeArgs.empty() ){
+    computeArgVec2( args, activeArgs, body, ipl );
+  }
   if( activeArgs.empty() ){
     return body;
   }else{
@@ -1002,9 +1137,13 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
   }else if( computeOption==COMPUTE_NNF ){
     return options::nnfQuant();
   }else if( computeOption==COMPUTE_PROCESS_ITE ){
-    return options::iteCondVarSplitQuant() || options::simpleIteLiftQuant();
+    return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant();
+  }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){
+    return options::iteDtTesterSplitQuant();
   }else if( computeOption==COMPUTE_PRENEX ){
     return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant();
+  }else if( computeOption==COMPUTE_ELIM_TAUT ){
+    return options::elimTautQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
     return options::varElimQuant() || options::dtVarExpandQuant();
   }else if( computeOption==COMPUTE_CNF ){
@@ -1041,8 +1180,12 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp
       n = computeNNF( n );
     }else if( computeOption==COMPUTE_PROCESS_ITE ){
       n = computeProcessIte( n, true, true );
+    }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){
+      n = computeProcessIte2( n );
     }else if( computeOption==COMPUTE_PRENEX ){
       n = computePrenex( n, args, true );
+    }else if( computeOption==COMPUTE_ELIM_TAUT ){
+      n = computeElimTaut( n );
     }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
       Node prev;
       do{
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 838eff57b..d01677171 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -40,15 +40,18 @@ private:
   static bool hasArg( std::vector< Node >& args, Node n );
   static bool hasArg1( Node a, Node n );
   static Node computeClause( Node n );
+  static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj );
 private:
   static Node computeElimSymbols( Node body );
   static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl );
   static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
   static Node computeNNF( Node body );
   static Node computeProcessIte( Node body, bool hasPol, bool pol );
+  static Node computeProcessIte2( Node body );
   static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl );
   static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred );
   static Node computePrenex( Node body, std::vector< Node >& args, bool pol );
+  static Node computeElimTaut( Node body );
   static Node computeSplit( Node f, Node body, std::vector< Node >& args );
 private:
   enum{
@@ -57,7 +60,9 @@ private:
     COMPUTE_AGGRESSIVE_MINISCOPING,
     COMPUTE_NNF,
     COMPUTE_PROCESS_ITE,
+    COMPUTE_PROCESS_ITE_2,
     COMPUTE_PRENEX,
+    COMPUTE_ELIM_TAUT,
     COMPUTE_VAR_ELIMINATION,
     //COMPUTE_FLATTEN_ARGS_UF,
     COMPUTE_CNF,
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 2671f616b..c6115195d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -23,6 +23,7 @@
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/rewrite_engine.h"
+#include "theory/quantifiers/fun_def_engine.h"
 
 //for sygus
 #include "theory/bv/theory_bv_utils.h"
@@ -77,7 +78,7 @@ void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) {
   }
 }
 
-TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ) {
+TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ), d_op_id_count( 0 ), d_typ_id_count( 0 ) {
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
   if( options::ceGuidedInst() ){
@@ -129,11 +130,12 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
   bool rec = false;
   if( d_processed.find( n )==d_processed.end() ){
     d_processed.insert(n);
-    d_type_map[ n.getType() ].push_back( n );
-    //if this is an atomic trigger, consider adding it
-    //Call the children?
-    if( inst::Trigger::isAtomicTrigger( n ) ){
-      if( !TermDb::hasInstConstAttr(n) ){
+    if( !TermDb::hasInstConstAttr(n) ){
+      Trace("term-db-debug") << "register term : " << n << std::endl;
+      d_type_map[ n.getType() ].push_back( n );
+      //if this is an atomic trigger, consider adding it
+      //Call the children?
+      if( inst::Trigger::isAtomicTrigger( n ) ){
         Trace("term-db") << "register term in db " << n << std::endl;
         Node op = getOperator( n );
         /*
@@ -166,7 +168,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
     d_iclosure_processed.insert( n );
     rec = true;
   }
-  if( rec ){
+  if( rec && n.getKind()!=FORALL ){
     for( size_t i=0; i<n.getNumChildren(); i++ ){
       addTerm( n[i], added, withinQuant, withinInstClosure );
     }
@@ -409,7 +411,7 @@ bool TermDb::isInstClosure( Node r ) {
   return d_iclosure_processed.find( r )!=d_iclosure_processed.end();
 }
 
-//checks whether a type is reasonably small enough such that all of its domain elements can be enumerated
+//checks whether a type is not Array and is reasonably small enough (<1000) such that all of its domain elements can be enumerated
 bool TermDb::mayComplete( TypeNode tn ) {
   std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn );
   if( it==d_may_complete.end() ){
@@ -779,6 +781,7 @@ Node TermDb::getCounterexampleLiteral( Node f ){
 }
 
 Node TermDb::getInstConstantNode( Node n, Node f ){
+  Assert( d_inst_constants.find( f )!=d_inst_constants.end() );
   return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]);
 }
 
@@ -945,6 +948,7 @@ Node TermDb::getSkolemizedBody( Node f ){
 }
 
 Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) {
+  Trace("term-db-enum") << "Get enumerate term " << tn << " " << index << std::endl;
   std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn );
   unsigned teIndex;
   if( it==d_typ_enum_map.end() ){
@@ -1154,6 +1158,156 @@ void TermDb::filterInstances( std::vector< Node >& nodes ){
   nodes.insert( nodes.begin(), temp.begin(), temp.end() );
 }
 
+int TermDb::getIdForOperator( Node op ) {
+  std::map< Node, int >::iterator it = d_op_id.find( op );
+  if( it==d_op_id.end() ){
+    d_op_id[op] = d_op_id_count;
+    d_op_id_count++;
+    return d_op_id[op];
+  }else{
+    return it->second;
+  }
+}
+
+int TermDb::getIdForType( TypeNode t ) {
+  std::map< TypeNode, int >::iterator it = d_typ_id.find( t );
+  if( it==d_typ_id.end() ){
+    d_typ_id[t] = d_typ_id_count;
+    d_typ_id_count++;
+    return d_typ_id[t];
+  }else{
+    return it->second;
+  }
+}
+
+bool TermDb::getTermOrder( Node a, Node b ) {
+  if( a.getKind()==BOUND_VARIABLE ){
+    if( b.getKind()==BOUND_VARIABLE ){
+      return a.getAttribute(InstVarNumAttribute())<b.getAttribute(InstVarNumAttribute());
+    }else{
+      return true;
+    }
+  }else if( b.getKind()!=BOUND_VARIABLE ){
+    Node aop = a.hasOperator() ? a.getOperator() : a;
+    Node bop = b.hasOperator() ? b.getOperator() : b;
+    Trace("aeq-debug2") << a << "...op..." << aop << std::endl;
+    Trace("aeq-debug2") << b << "...op..." << bop << std::endl;
+    if( aop==bop ){
+      if( a.getNumChildren()==b.getNumChildren() ){
+        for( unsigned i=0; i<a.getNumChildren(); i++ ){
+          if( a[i]!=b[i] ){
+            //first distinct child determines the ordering
+            return getTermOrder( a[i], b[i] );
+          }
+        }
+      }else{
+        return aop.getNumChildren()<bop.getNumChildren();
+      }
+    }else{
+      return getIdForOperator( aop )<getIdForOperator( bop );
+    }
+  }
+  return false;
+}
+
+
+
+Node TermDb::getCanonicalFreeVar( TypeNode tn, unsigned i ) {
+  Assert( !tn.isNull() );
+  while( d_cn_free_var[tn].size()<=i ){
+    std::stringstream oss;
+    oss << tn;
+    std::string typ_name = oss.str();
+    while( typ_name[0]=='(' ){
+      typ_name.erase( typ_name.begin() );
+    }
+    std::stringstream os;
+    os << typ_name[0] << i;
+    Node x = NodeManager::currentNM()->mkBoundVar( os.str().c_str(), tn );
+    InstVarNumAttribute ivna;
+    x.setAttribute(ivna,d_cn_free_var[tn].size());
+    d_cn_free_var[tn].push_back( x );
+  }
+  return d_cn_free_var[tn][i];
+}
+
+struct sortTermOrder {
+  TermDb* d_tdb;
+  //std::map< Node, std::map< Node, bool > > d_cache;
+  bool operator() (Node i, Node j) {
+    /*
+    //must consult cache since term order is partial?
+    std::map< Node, bool >::iterator it = d_cache[j].find( i );
+    if( it!=d_cache[j].end() && it->second ){
+      return false;
+    }else{
+      bool ret = d_tdb->getTermOrder( i, j );
+      d_cache[i][j] = ret;
+      return ret;
+    }
+    */
+    return d_tdb->getTermOrder( i, j );
+  }
+};
+
+//this function makes a canonical representation of a term (
+//  - orders variables left to right
+//  - if apply_torder, then sort direct subterms of commutative operators
+Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder ) {
+  Trace("canon-term-debug") << "Get canonical term for " << n << std::endl;
+  if( n.getKind()==BOUND_VARIABLE ){
+    std::map< TNode, TNode >::iterator it = subs.find( n );
+    if( it==subs.end() ){
+      TypeNode tn = n.getType();
+      //allocate variable
+      unsigned vn = var_count[tn];
+      var_count[tn]++;
+      subs[n] = getCanonicalFreeVar( tn, vn );
+      Trace("canon-term-debug") << "...allocate variable." << std::endl;
+      return subs[n];
+    }else{
+      Trace("canon-term-debug") << "...return variable in subs." << std::endl;
+      return it->second;
+    }
+  }else if( n.getNumChildren()>0 ){
+    //collect children
+    Trace("canon-term-debug") << "Collect children" << std::endl;
+    std::vector< Node > cchildren;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      cchildren.push_back( n[i] );
+    }
+    //if applicable, first sort by term order
+    if( apply_torder && isComm( n.getKind() ) ){
+      Trace("canon-term-debug") << "Sort based on commutative operator " << n.getKind() << std::endl;
+      sortTermOrder sto;
+      sto.d_tdb = this;
+      std::sort( cchildren.begin(), cchildren.end(), sto );
+    }
+    //now make canonical
+    Trace("canon-term-debug") << "Make canonical children" << std::endl;
+    for( unsigned i=0; i<cchildren.size(); i++ ){
+      cchildren[i] = getCanonicalTerm( cchildren[i], var_count, subs, apply_torder );
+    }
+    if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+      Trace("canon-term-debug") << "Insert operator " << n.getOperator() << std::endl;
+      cchildren.insert( cchildren.begin(), n.getOperator() );
+    }
+    Trace("canon-term-debug") << "...constructing for " << n << "." << std::endl;
+    Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cchildren );
+    Trace("canon-term-debug") << "...constructed " << ret << " for " << n << "." << std::endl;
+    return ret;
+  }else{
+    Trace("canon-term-debug") << "...return 0-child term." << std::endl;
+    return n;
+  }
+}
+
+Node TermDb::getCanonicalTerm( TNode n, bool apply_torder ){
+  std::map< TypeNode, unsigned > var_count;
+  std::map< TNode, TNode > subs;
+  return getCanonicalTerm( n, var_count, subs, apply_torder );
+}
+
 bool TermDb::containsTerm( Node n, Node t ) {
   if( n==t ){
     return true;
@@ -1179,6 +1333,15 @@ Node TermDb::simpleNegate( Node n ){
   }
 }
 
+bool TermDb::isAssoc( Kind k ) {
+  return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
+         k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT;
+}
+
+bool TermDb::isComm( Kind k ) {
+  return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
+         k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR;
+}
 
 void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
   if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){
@@ -1270,6 +1433,7 @@ void TermDb::computeAttributes( Node q ) {
             exit( 0 );
           }
           d_fun_defs[f] = true;
+          d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine() );
         }
         if( avar.getAttribute(SygusAttribute()) ){
           //not necessarily nested existential
@@ -1417,7 +1581,7 @@ TNode TermDbSygus::getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count
   }
 }
 
-TypeNode TermDbSygus::getSygusType( Node v ) {
+TypeNode TermDbSygus::getSygusTypeForVar( Node v ) {
   Assert( d_fv_stype.find( v )!=d_fv_stype.end() );
   return d_fv_stype[v];
 }
@@ -1440,7 +1604,7 @@ bool TermDbSygus::getMatch2( Node p, Node n, std::map< int, Node >& s, std::vect
     return p==n;
   }else if( n.getKind()==p.getKind() && n.getNumChildren()==p.getNumChildren() ){
     //try both ways?
-    unsigned rmax = isComm( n.getKind() ) && n.getNumChildren()==2 ? 2 : 1;
+    unsigned rmax = TermDb::isComm( n.getKind() ) && n.getNumChildren()==2 ? 2 : 1;
     std::vector< int > new_tmp;
     for( unsigned r=0; r<rmax; r++ ){
       bool success = true;
@@ -1579,7 +1743,7 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int
       Node n = NodeManager::currentNM()->mkNode( APPLY, children );
       //must expand definitions
       Node ne = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( n.toExpr() ) );
-      Trace("sygus-util-debug") << "Expanded definitions in " << n << " to " << ne << std::endl;
+      Trace("sygus-db-debug") << "Expanded definitions in " << n << " to " << ne << std::endl;
       return ne;
       */
     }
@@ -1591,6 +1755,7 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int
 Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
   std::map< Node, Node >::iterator it = d_sygus_to_builtin[tn].find( n );
   if( it==d_sygus_to_builtin[tn].end() ){
+    Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n << ", type = " << tn << std::endl;
     Assert( n.getKind()==APPLY_CONSTRUCTOR );
     const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
     unsigned i = Datatype::indexOf( n.getOperator().toExpr() );
@@ -1666,7 +1831,7 @@ Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn, int rcons_depth ) {
                 int end = d_const_list[tn1].size()-d_const_list_pos[tn1];
                 for( int i=start; i>=end; --i ){
                   Node c1 = d_const_list[tn1][i];
-                  //only consider if smaller than c, and 
+                  //only consider if smaller than c, and
                   if( doCompare( c1, c, ck ) ){
                     Node c2 = NodeManager::currentNM()->mkNode( pkm, c, c1 );
                     c2 = Rewriter::rewrite( c2 );
@@ -1756,28 +1921,18 @@ Node TermDbSygus::getNormalized( TypeNode t, Node prog, bool do_pre_norm, bool d
   }
 }
 
-int TermDbSygus::getTermSize( Node n ){
+int TermDbSygus::getSygusTermSize( Node n ){
   if( isVar( n ) ){
     return 0;
   }else{
     int sum = 0;
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      sum += getTermSize( n[i] );
+      sum += getSygusTermSize( n[i] );
     }
     return 1+sum;
   }
 }
 
-bool TermDbSygus::isAssoc( Kind k ) {
-  return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
-         k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT;
-}
-
-bool TermDbSygus::isComm( Kind k ) {
-  return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
-         k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR;
-}
-
 bool TermDbSygus::isAntisymmetric( Kind k, Kind& dk ) {
   if( k==GT ){
     dk = LT;
@@ -1942,10 +2097,10 @@ void TermDbSygus::registerSygusType( TypeNode tn ){
       d_register[tn] = TypeNode::null();
     }else{
       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      Trace("sygus-util") << "Register type " << dt.getName() << "..." << std::endl;
+      Trace("sygus-db") << "Register type " << dt.getName() << "..." << std::endl;
       d_register[tn] = TypeNode::fromType( dt.getSygusType() );
       if( d_register[tn].isNull() ){
-        Trace("sygus-util") << "...not sygus." << std::endl;
+        Trace("sygus-db") << "...not sygus." << std::endl;
       }else{
         //for constant reconstruction
         Kind ck = getComparisonKind( TypeNode::fromType( dt.getSygusType() ) );
@@ -1956,14 +2111,14 @@ void TermDbSygus::registerSygusType( TypeNode tn ){
           Expr sop = dt[i].getSygusOp();
           Assert( !sop.isNull() );
           Node n = Node::fromExpr( sop );
-          Trace("sygus-util") << "  Operator #" << i << " : " << sop;
+          Trace("sygus-db") << "  Operator #" << i << " : " << sop;
           if( sop.getKind() == kind::BUILTIN ){
             Kind sk = NodeManager::operatorToKind( n );
-            Trace("sygus-util") << ", kind = " << sk;
+            Trace("sygus-db") << ", kind = " << sk;
             d_kinds[tn][sk] = i;
             d_arg_kind[tn][i] = sk;
           }else if( sop.isConst() ){
-            Trace("sygus-util") << ", constant";
+            Trace("sygus-db") << ", constant";
             d_consts[tn][n] = i;
             d_arg_const[tn][i] = n;
             d_const_list[tn].push_back( n );
@@ -1976,7 +2131,7 @@ void TermDbSygus::registerSygusType( TypeNode tn ){
           }
           d_ops[tn][n] = i;
           d_arg_ops[tn][i] = n;
-          Trace("sygus-util") << std::endl;
+          Trace("sygus-db") << std::endl;
         }
         //sort the constant list
         if( !d_const_list[tn].empty() ){
@@ -1986,12 +2141,12 @@ void TermDbSygus::registerSygusType( TypeNode tn ){
             sc.d_tds = this;
             std::sort( d_const_list[tn].begin(), d_const_list[tn].end(), sc );
           }
-          Trace("sygus-util") << "Type has " << d_const_list[tn].size() << " constants..." << std::endl << "  ";
+          Trace("sygus-db") << "Type has " << d_const_list[tn].size() << " constants..." << std::endl << "  ";
           for( unsigned i=0; i<d_const_list[tn].size(); i++ ){
-            Trace("sygus-util") << d_const_list[tn][i] << " ";
+            Trace("sygus-db") << d_const_list[tn][i] << " ";
           }
-          Trace("sygus-util") << std::endl;
-          Trace("sygus-util") << "Of these, " << d_const_list_pos[tn] << " are marked as positive." << std::endl;
+          Trace("sygus-db") << std::endl;
+          Trace("sygus-db") << "Of these, " << d_const_list_pos[tn] << " are marked as positive." << std::endl;
         }
         //register connected types
         for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
@@ -2008,6 +2163,11 @@ bool TermDbSygus::isRegistered( TypeNode tn ) {
   return d_register.find( tn )!=d_register.end();
 }
 
+TypeNode TermDbSygus::sygusToBuiltinType( TypeNode tn ) {
+  Assert( isRegistered( tn ) );
+  return d_register[tn];
+}
+
 int TermDbSygus::getKindArg( TypeNode tn, Kind k ) {
   Assert( isRegistered( tn ) );
   std::map< TypeNode, std::map< Kind, int > >::iterator itt = d_kinds.find( tn );
@@ -2197,6 +2357,7 @@ bool TermDbSygus::doCompare( Node a, Node b, Kind k ) {
   return com==d_true;
 }
 
+
 void doStrReplace(std::string& str, const std::string& oldStr, const std::string& newStr){
   size_t pos = 0;
   while((pos = str.find(oldStr, pos)) != std::string::npos){
@@ -2216,7 +2377,20 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
         if( n.getNumChildren()>0 ){
           out << "(";
         }
-        out << dt[cIndex].getSygusOp();
+        Node op = dt[cIndex].getSygusOp();
+        if( op.getType().isBitVector() && op.isConst() ){
+          //print in the style it was given
+          Trace("sygus-print-bvc") << "[Print " << op << " " << dt[cIndex].getName() << "]" << std::endl;
+          std::stringstream ss;
+          ss << dt[cIndex].getName();
+          std::string str = ss.str();
+          std::size_t found = str.find_last_of("_");
+          Assert( found!=std::string::npos );
+          std::string name = std::string( str.begin() + found +1, str.end() );
+          out << name;
+        }else{
+          out << op;
+        }
         if( n.getNumChildren()>0 ){
           for( unsigned i=0; i<n.getNumChildren(); i++ ){
             out << " ";
@@ -2225,9 +2399,10 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
           out << ")";
         }
       }else{
+        std::stringstream let_out;
         //print as let term
         if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
-          out << "(let (";
+          let_out << "(let (";
         }
         std::vector< Node > subs_lvs;
         std::vector< Node > new_lvs;
@@ -2241,23 +2416,26 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
           //map free variables to proper terms
           if( i<dt[cIndex].getNumSygusLetInputArgs() ){
             //it should be printed as a let argument
-            out << "(";
-            out << lv << " " << lv.getType() << " ";
-            printSygusTerm( out, n[i], lvs );
-            out << ")";
+            let_out << "(";
+            let_out << lv << " " << lv.getType() << " ";
+            printSygusTerm( let_out, n[i], lvs );
+            let_out << ")";
           }
         }
         if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
-          out << ") ";
+          let_out << ") ";
         }
         //print the body
         Node let_body = Node::fromExpr( dt[cIndex].getSygusLetBody() );
         let_body = let_body.substitute( subs_lvs.begin(), subs_lvs.end(), new_lvs.begin(), new_lvs.end() );
         new_lvs.insert( new_lvs.end(), lvs.begin(), lvs.end() );
-        std::stringstream body_out;
-        printSygusTerm( body_out, let_body, new_lvs );
-        std::string body = body_out.str();
-        for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){ 
+        printSygusTerm( let_out, let_body, new_lvs );
+        if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
+          let_out << ")";
+        }
+        //do variable substitutions since ASSUMING : let_vars are interpreted literally and do not represent a class of variables
+        std::string lbody = let_out.str();
+        for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){
           std::stringstream old_str;
           old_str << new_lvs[i];
           std::stringstream new_str;
@@ -2266,12 +2444,9 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
           }else{
             new_str << Node::fromExpr( dt[cIndex].getSygusLetArg( i ) );
           }
-          doStrReplace( body, old_str.str().c_str(), new_str.str().c_str() );
-        }
-        out << body;
-        if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
-          out << ")";
+          doStrReplace( lbody, old_str.str().c_str(), new_str.str().c_str() );
         }
+        out << lbody;
       }
       return;
     }
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index b7fa4e999..1ffe0e29e 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -149,13 +149,13 @@ public:
   unsigned getNumGroundTerms( Node f );
   /** count number of non-redundant ground terms per operator */
   std::map< Node, int > d_op_nonred_count;
-  /** map from APPLY_UF operators to ground terms for that operator */
+  /** map from operators to ground terms for that operator */
   std::map< Node, std::vector< Node > > d_op_map;
   /** has map */
   std::map< Node, bool > d_has_map;
   /** map from reps to a term in eqc in d_has_map */
   std::map< Node, Node > d_term_elig_eqc;
-  /** map from APPLY_UF functions to trie */
+  /** map from operators to trie */
   std::map< Node, TermArgTrie > d_func_map_trie;
   std::map< Node, TermArgTrie > d_func_map_eqc_trie;
   /**mapping from UF terms to representatives of their arguments */
@@ -326,12 +326,42 @@ public:
   /** filter all nodes that have instances */
   void filterInstances( std::vector< Node >& nodes );
 
+//for term ordering
+private:
+  /** operator id count */
+  int d_op_id_count;
+  /** map from operators to id */
+  std::map< Node, int > d_op_id;
+  /** type id count */
+  int d_typ_id_count;
+  /** map from type to id */
+  std::map< TypeNode, int > d_typ_id;
+  //free variables
+  std::map< TypeNode, std::vector< Node > > d_cn_free_var;
+  // get canonical term, return null if it contains a term apart from handled signature
+  Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder );
+public:
+  /** get id for operator */
+  int getIdForOperator( Node op );
+  /** get id for type */
+  int getIdForType( TypeNode t );
+  /** get term order */
+  bool getTermOrder( Node a, Node b );
+  /** get canonical free variable #i of type tn */
+  Node getCanonicalFreeVar( TypeNode tn, unsigned i );
+  /** get canonical term */
+  Node getCanonicalTerm( TNode n, bool apply_torder = false );
+
 //general utilities
 public:
   /** simple check for contains term */
   static bool containsTerm( Node n, Node t );
   /** simple negate */
   static Node simpleNegate( Node n );
+  /** is assoc */
+  static bool isAssoc( Kind k );
+  /** is comm */
+  static bool isComm( Kind k );
 
 //for sygus
 private:
@@ -403,7 +433,7 @@ public:
   bool getMatch( Node n, TypeNode st, int& index_found, std::vector< Node >& args, int index_exc = -1, int index_start = 0 );
 private:
   //information for sygus types
-  std::map< TypeNode, TypeNode > d_register;  //stores sygus type
+  std::map< TypeNode, TypeNode > d_register;  //stores sygus -> builtin type
   std::map< TypeNode, std::map< int, Kind > > d_arg_kind;
   std::map< TypeNode, std::map< Kind, int > > d_kinds;
   std::map< TypeNode, std::map< int, Node > > d_arg_const;
@@ -425,6 +455,7 @@ private:
 public:
   TermDbSygus();
   bool isRegistered( TypeNode tn );
+  TypeNode sygusToBuiltinType( TypeNode tn );
   int getKindArg( TypeNode tn, Kind k );
   int getConstArg( TypeNode tn, Node n );
   int getOpArg( TypeNode tn, Node n );
@@ -441,10 +472,6 @@ public:
   void registerSygusType( TypeNode tn );
   /** get arg type */
   TypeNode getArgType( const DatatypeConstructor& c, int i );
-  /** is assoc */
-  bool isAssoc( Kind k );
-  /** is comm */
-  bool isComm( Kind k );
   /** isAntisymmetric */
   bool isAntisymmetric( Kind k, Kind& dk );
   /** is idempotent arg */
@@ -459,13 +486,13 @@ public:
   Node getTypeValueOffset( TypeNode tn, Node val, int offset, int& status );
   /** get value */
   Node getTypeMaxValue( TypeNode tn );
-  TypeNode getSygusType( Node v );
+  TypeNode getSygusTypeForVar( Node v );
   Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre );
   Node sygusToBuiltin( Node n, TypeNode tn );
   Node builtinToSygusConst( Node c, TypeNode tn, int rcons_depth = 0 );
   Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
   Node getNormalized( TypeNode t, Node prog, bool do_pre_norm = false, bool do_post_norm = true );
-  int getTermSize( Node n );
+  int getSygusTermSize( Node n );
   /** given a term, construct an equivalent smaller one that respects syntax */
   Node minimizeBuiltinTerm( Node n );
   /** given a term, expand it into more basic components */
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index c55ed27ea..e4d9a2730 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -145,7 +145,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >&
         break;
       }
     }
-    if( varCount<f[0].getNumChildren() ){
+    if( varCount<f[0].getNumChildren() && !options::partialTriggers() ){
       Trace("trigger-debug") << "Don't consider trigger since it does not contain all variables in " << f << std::endl;
       for( unsigned i=0; i<nodes.size(); i++) {
         Trace("trigger-debug") << nodes[i] << " ";
@@ -226,6 +226,12 @@ bool Trigger::isUsable( Node n, Node f ){
       if( isBooleanTermTrigger( n ) ){
         return true;
       }
+      if( options::purifyTriggers() ){
+        Node x = getInversionVariable( n );
+        if( !x.isNull() ){
+          return true;
+        }
+      }
     }
     return false;
   }else{
@@ -247,6 +253,7 @@ bool nodeContainsVar( Node n, Node v ){
 }
 
 Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
+  Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
   if( options::relationalTriggers() ){
     if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){
       Node rtr;
@@ -287,7 +294,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
     }
   }
   bool usable = quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f );
-  Trace("usable") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==f) << " " << isAtomicTrigger( n ) << " " << isUsable( n, f ) << std::endl;
+  Trace("trigger-debug") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==f) << " " << isAtomicTrigger( n ) << " " << isUsable( n, f ) << std::endl;
   if( usable ){
     return n;
   }else{
@@ -512,13 +519,16 @@ Node Trigger::getInversionVariable( Node n ) {
         if( !n[i].isConst() ){
           Trace("var-trigger-debug") << "No : non-linear coefficient " << n << std::endl;
           return Node::null();
-        }else if( n.getType().isInteger() ){
+        }
+        /*
+        else if( n.getType().isInteger() ){
           Rational r = n[i].getConst<Rational>();
           if( r!=Rational(-1) && r!=Rational(1) ){
             Trace("var-trigger-debug") << "No : not integer coefficient " << n << std::endl;
             return Node::null();
           }
         }
+        */
       }
     }
     return ret;
@@ -539,8 +549,13 @@ Node Trigger::getInversion( Node n, Node x ) {
           x = NodeManager::currentNM()->mkNode( MINUS, x, n[i] );
         }else if( n.getKind()==MULT ){
           Assert( n[i].isConst() );
-          Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst<Rational>() );
-          x = NodeManager::currentNM()->mkNode( MULT, x, coeff );
+          if( x.getType().isInteger() ){
+            Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst<Rational>() );
+            x = NodeManager::currentNM()->mkNode( INTS_DIVISION, x, coeff );
+          }else{
+            Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst<Rational>() );
+            x = NodeManager::currentNM()->mkNode( MULT, x, coeff );
+          }
         }
       }else{
         Assert( cindex==-1 );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index e654a689d..54f2a16fe 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -32,10 +32,12 @@
 #include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/local_theory_ext.h"
 #include "theory/quantifiers/relevant_domain.h"
+#include "theory/quantifiers/alpha_equivalence.h"
 #include "theory/uf/options.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/quantifiers/full_model_check.h"
 #include "theory/quantifiers/ambqi_builder.h"
+#include "theory/quantifiers/fun_def_engine.h"
 
 using namespace std;
 using namespace CVC4;
@@ -99,7 +101,7 @@ d_lemmas_produced_c(u){
   }else{
     d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
   }
-  if( !options::finiteModelFind() ){
+  if( options::fullSaturateQuant() ){
     d_rel_dom = new quantifiers::RelevantDomain( this, d_model );
   }else{
     d_rel_dom = NULL;
@@ -163,6 +165,17 @@ d_lemmas_produced_c(u){
   }else{
     d_lte_part_inst = NULL;
   }
+  if( options::quantAlphaEquiv() ){
+    d_alpha_equiv = new quantifiers::AlphaEquivalence( this );
+  }else{
+    d_alpha_equiv = NULL;
+  }
+  //if( options::funDefs() ){
+  //  d_fun_def_engine = new quantifiers::FunDefEngine( this, c );
+  //  d_modules.push_back( d_fun_def_engine );
+  //}else{
+  d_fun_def_engine = NULL;
+  //}
 
   if( needsBuilder ){
     Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
@@ -202,6 +215,7 @@ QuantifiersEngine::~QuantifiersEngine(){
   delete d_sg_gen;
   delete d_ceg_inst;
   delete d_lte_part_inst;
+  delete d_fun_def_engine;
   for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) {
     delete (*i).second;
   }
@@ -298,6 +312,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
         Trace("quant-engine-debug") << "  lemmas waiting = " << d_lemmas_waiting.size() << std::endl;
       }
       Trace("quant-engine-debug") << "  Theory engine finished : " << !d_te->needCheck() << std::endl;
+      Trace("quant-engine-debug") << "  Needs model effort : " << needsModelE << std::endl;
       Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
     }
     if( Trace.isOn("quant-engine-ee") ){
@@ -422,6 +437,38 @@ void QuantifiersEngine::check( Theory::Effort e ){
   }
 }
 
+bool QuantifiersEngine::reduceQuantifier( Node q ) {
+  std::map< Node, bool >::iterator it = d_quants_red.find( q );
+  if( it==d_quants_red.end() ){
+    if( d_alpha_equiv ){
+      Trace("quant-engine-debug") << "Alpha equivalence " << q << "?" << std::endl;
+      //add equivalence with another quantified formula
+      if( !d_alpha_equiv->registerQuantifier( q ) ){
+        Trace("quant-engine-debug") << "...alpha equivalence success." << std::endl;
+        ++(d_statistics.d_red_alpha_equiv);
+        d_quants_red[q] = true;
+        return true;
+      }
+    }
+    if( d_lte_part_inst && !q.getAttribute(LtePartialInstAttribute()) ){
+      //will partially instantiate
+      Trace("quant-engine-debug") << "LTE: Partially instantiate " << q << "?" << std::endl;
+      if( d_lte_part_inst->addQuantifier( q ) ){
+        Trace("quant-engine-debug") << "...LTE partially instantiate success." << std::endl;
+        //delayed reduction : assert to model
+        d_model->assertQuantifier( q, true );
+        ++(d_statistics.d_red_lte_partial_inst);
+        d_quants_red[q] = true;
+        return true;
+      }
+    }
+    d_quants_red[q] = false;
+    return false;
+  }else{
+    return it->second;
+  }
+}
+
 bool QuantifiersEngine::registerQuantifier( Node f ){
   std::map< Node, bool >::iterator it = d_quants.find( f );
   if( it==d_quants.end() ){
@@ -431,15 +478,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){
     Assert( f.getKind()==FORALL );
 
     //check whether we should apply a reduction
-    bool reduced = false;
-    if( d_lte_part_inst && !f.getAttribute(LtePartialInstAttribute()) ){
-      Trace("lte-partial-inst") << "LTE: Partially instantiate " << f << "?" << std::endl;
-      if( d_lte_part_inst->addQuantifier( f ) ){
-        reduced = true;
-      }
-    }
-    if( reduced ){
-      d_model->assertQuantifier( f, true );
+    if( reduceQuantifier( f ) ){
       d_quants[f] = false;
       return false;
     }else{
@@ -482,30 +521,31 @@ void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
 
 void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
   if( !pol ){
-    //do skolemization
-    if( d_skolemized.find( f )==d_skolemized.end() ){
-      Node body = d_term_db->getSkolemizedBody( f );
-      NodeBuilder<> nb(kind::OR);
-      nb << f << body.notNode();
-      Node lem = nb;
-      if( Trace.isOn("quantifiers-sk") ){
-        Node slem = Rewriter::rewrite( lem );
-        Trace("quantifiers-sk") << "Skolemize lemma : " << slem << std::endl;
+    //if not reduced
+    if( !reduceQuantifier( f ) ){
+      //do skolemization
+      if( d_skolemized.find( f )==d_skolemized.end() ){
+        Node body = d_term_db->getSkolemizedBody( f );
+        NodeBuilder<> nb(kind::OR);
+        nb << f << body.notNode();
+        Node lem = nb;
+        if( Trace.isOn("quantifiers-sk") ){
+          Node slem = Rewriter::rewrite( lem );
+          Trace("quantifiers-sk") << "Skolemize lemma : " << slem << std::endl;
+        }
+        getOutputChannel().lemma( lem, false, true );
+        d_skolemized[f] = true;
       }
-      getOutputChannel().lemma( lem, false, true );
-      d_skolemized[f] = true;
     }
-  }
-  //assert to modules TODO : handle !pol
-  if( pol ){
-    //register the quantifier
-    bool nreduced = registerQuantifier( f );
-    //assert it to each module
-    if( nreduced ){
+  }else{
+    //assert to modules TODO : also for !pol?
+    //register the quantifier, assert it to each module
+    if( registerQuantifier( f ) ){
       d_model->assertQuantifier( f );
       for( int i=0; i<(int)d_modules.size(); i++ ){
         d_modules[i]->assertNode( f );
       }
+      addTermToDatabase( d_term_db->getInstConstantBody( f ), true );
     }
   }
 }
@@ -714,6 +754,7 @@ Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){
 }
 
 Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& terms ) {
+  d_term_db->makeInstantiationConstantsFor( f );
   return getInstantiation( f, d_term_db->d_inst_constants[f], terms );
 }
 
@@ -783,12 +824,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo
     //make it representative, this is helpful for recognizing duplication
     if( mkRep ){
       //pick the best possible representative for instantiation, based on past use and simplicity of term
-      Node ti = d_eq_query->getInternalRepresentative( terms[i], f, i );
-      //check if it is a subtype (can be violated in mixed int/real) FIXME : do this check inside getInternalRepresentative
-      if( ti.getType().isSubtypeOf( f[0][i].getType() ) ){
-        terms[i] = ti;
-        Trace("inst-add-debug2") << " (" << terms[i] << ")";
-      }
+      terms[i] = d_eq_query->getInternalRepresentative( terms[i], f, i );
     }
   }
   Trace("inst-add-debug") << std::endl;
@@ -980,7 +1016,9 @@ QuantifiersEngine::Statistics::Statistics():
   d_triggers("QuantifiersEngine::Triggers", 0),
   d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
   d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
-  d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0)
+  d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
+  d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
+  d_red_lte_partial_inst("QuantifiersEngine::Reductions_Lte_Partial_Inst", 0)
 {
   StatisticsRegistry::registerStat(&d_num_quant);
   StatisticsRegistry::registerStat(&d_instantiation_rounds);
@@ -992,6 +1030,8 @@ QuantifiersEngine::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_simple_triggers);
   StatisticsRegistry::registerStat(&d_multi_triggers);
   StatisticsRegistry::registerStat(&d_multi_trigger_instantiations);
+  StatisticsRegistry::registerStat(&d_red_alpha_equiv);
+  StatisticsRegistry::registerStat(&d_red_lte_partial_inst);
 }
 
 QuantifiersEngine::Statistics::~Statistics(){
@@ -1005,6 +1045,8 @@ QuantifiersEngine::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_simple_triggers);
   StatisticsRegistry::unregisterStat(&d_multi_triggers);
   StatisticsRegistry::unregisterStat(&d_multi_trigger_instantiations);
+  StatisticsRegistry::unregisterStat(&d_red_alpha_equiv);
+  StatisticsRegistry::unregisterStat(&d_red_lte_partial_inst);
 }
 
 eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
@@ -1070,16 +1112,12 @@ bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
     return true;
   }else{
     eq::EqualityEngine* ee = getEngine();
-    if( d_liberal ){
-      return true;//!areDisequal( a, b );
-    }else{
-      if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
-        if( ee->areEqual( a, b ) ){
-          return true;
-        }
+    if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
+      if( ee->areEqual( a, b ) ){
+        return true;
       }
-      return false;
     }
+    return false;
   }
 }
 
@@ -1094,6 +1132,7 @@ bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
 }
 
 Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){
+  Assert( f.isNull() || f.getKind()==FORALL );
   Node r = getRepresentative( a );
   if( !options::internalReps() ){
     return r;
@@ -1108,16 +1147,17 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
             r = getRepresentative( r );
           }else{
             if( r.getType().isSort() ){
-              //TODO : this can happen in rare cases
-              // say x:(Array Int U), select( x, 0 ), x assigned (const @u1).
               Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
+              //should never happen : UF constants should never escape model
+              Assert( false );
             }
           }
         }
       }
     }
-    std::map< Node, Node >::iterator itir = d_int_rep.find( r );
-    if( itir==d_int_rep.end() ){
+    TypeNode v_tn = f.isNull() ? a.getType() : f[0][index].getType();
+    std::map< Node, Node >::iterator itir = d_int_rep[v_tn].find( r );
+    if( itir==d_int_rep[v_tn].end() ){
       //find best selection for representative
       Node r_best;
       //if( options::fmfRelevantDomain() && !f.isNull() ){
@@ -1135,7 +1175,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
       Trace("internal-rep-select")  << " } " << std::endl;
       int r_best_score = -1;
       for( size_t i=0; i<eqc.size(); i++ ){
-        int score = getRepScore( eqc[i], f, index );
+        int score = getRepScore( eqc[i], f, index, v_tn );
         if( score!=-2 ){
           if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
             r_best = eqc[i];
@@ -1144,12 +1184,8 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
         }
       }
       if( r_best.isNull() ){
-        if( !f.isNull() ){
-          Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index );
-          r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
-        }else{
-          r_best = a;
-        }
+        Trace("internal-rep-warn") << "No valid choice for representative in eqc class." << std::endl;
+        r_best = r;
       }
       //now, make sure that no other member of the class is an instance
       std::hash_map<TNode, Node, TNodeHashFunction> cache;
@@ -1159,7 +1195,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
         d_rep_score[ r_best ] = d_reset_count;
       }
       Trace("internal-rep-select") << "...Choose " << r_best << std::endl;
-      d_int_rep[r] = r_best;
+      d_int_rep[v_tn][r] = r_best;
       if( r_best!=a ){
         Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
         Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
@@ -1181,8 +1217,10 @@ void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode,
     }
   }
   Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl;
-  for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
-    Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl;
+  for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
+    for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
+      Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
+    }
   }
   //store representatives for newly created terms
   std::map< Node, Node > temp_rep_map;
@@ -1190,51 +1228,55 @@ void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode,
   bool success;
   do {
     success = false;
-    for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
-      if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){
-        Node ni = it->second;
-        std::vector< Node > cc;
-        cc.push_back( it->second.getOperator() );
-        bool changed = false;
-        for( unsigned j=0; j<ni.getNumChildren(); j++ ){
-          if( ni[j].getType().isSort() ){
-            Node r = getRepresentative( ni[j] );
-            if( d_int_rep.find( r )==d_int_rep.end() ){
-              Assert( temp_rep_map.find( r )!=temp_rep_map.end() );
-              r = temp_rep_map[r];
-            }
-            if( r==ni ){
-              //found sub-term as instance
-              Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl;
-              d_int_rep[it->first] = ni[j];
+    for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
+      for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
+        if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){
+          Node ni = it->second;
+          std::vector< Node > cc;
+          cc.push_back( it->second.getOperator() );
+          bool changed = false;
+          for( unsigned j=0; j<ni.getNumChildren(); j++ ){
+            if( ni[j].getType().isSort() ){
+              Node r = getRepresentative( ni[j] );
+              if( itt->second.find( r )==itt->second.end() ){
+                Assert( temp_rep_map.find( r )!=temp_rep_map.end() );
+                r = temp_rep_map[r];
+              }
+              if( r==ni ){
+                //found sub-term as instance
+                Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl;
+                itt->second[it->first] = ni[j];
+                changed = false;
+                success = true;
+                break;
+              }else{
+                Node ir = itt->second[r];
+                cc.push_back( ir );
+                if( ni[j]!=ir ){
+                  changed = true;
+                }
+              }
+            }else{
               changed = false;
-              success = true;
               break;
-            }else{
-              Node ir = d_int_rep[r];
-              cc.push_back( ir );
-              if( ni[j]!=ir ){
-                changed = true;
-              }
             }
-          }else{
-            changed = false;
-            break;
           }
-        }
-        if( changed ){
-          Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc );
-          Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl;
-          success = true;
-          d_int_rep[it->first] = n;
-          temp_rep_map[n] = it->first;
+          if( changed ){
+            Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc );
+            Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl;
+            success = true;
+            itt->second[it->first] = n;
+            temp_rep_map[n] = it->first;
+          }
         }
       }
     }
   }while( success );
   Trace("internal-rep-flatten") << "---After flattening : " << std::endl;
-  for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
-    Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl;
+  for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
+    for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
+      Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
+    }
   }
 }
 
@@ -1277,6 +1319,7 @@ Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Nod
   }
 }
 
+/*
 int getDepth( Node n ){
   if( n.getNumChildren()==0 ){
     return 0;
@@ -1291,10 +1334,13 @@ int getDepth( Node n ){
     return maxDepth;
   }
 }
+*/
 
-//smaller the score, the better
-int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){
-  if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){
+//-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
+int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, TypeNode v_tn ){
+  if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){  //reject
+    return -2;
+  }else if( !n.getType().isSubtypeOf( v_tn ) ){  //reject if incorrect type
     return -2;
   }else if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){
     return -1;
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index d5887f907..54f63bfe0 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -92,6 +92,8 @@ namespace quantifiers {
   class ConjectureGenerator;
   class CegInstantiation;
   class LtePartialInst;
+  class AlphaEquivalence;
+  class FunDefEngine;
 }/* CVC4::theory::quantifiers */
 
 namespace inst {
@@ -119,6 +121,8 @@ private:
   QuantRelevance * d_quant_rel;
   /** relevant domain */
   quantifiers::RelevantDomain* d_rel_dom;
+  /** alpha equivalence */
+  quantifiers::AlphaEquivalence * d_alpha_equiv;
   /** model builder */
   quantifiers::QModelBuilder* d_builder;
   /** phase requirements for each quantifier for each instantiation literal */
@@ -139,6 +143,8 @@ private:
   quantifiers::CegInstantiation * d_ceg_inst;
   /** lte partial instantiation */
   quantifiers::LtePartialInst * d_lte_part_inst;
+  /** function definitions engine */
+  quantifiers::FunDefEngine * d_fun_def_engine;
 public: //effort levels
   enum {
     QEFFORT_CONFLICT,
@@ -150,6 +156,8 @@ public: //effort levels
 private:
   /** list of all quantifiers seen */
   std::map< Node, bool > d_quants;
+  /** quantifiers reduced */
+  std::map< Node, bool > d_quants_red;
   /** list of all lemmas produced */
   //std::map< Node, bool > d_lemmas_produced;
   BoolMap d_lemmas_produced_c;
@@ -186,8 +194,7 @@ public:
   ~QuantifiersEngine();
   /** get theory engine */
   TheoryEngine* getTheoryEngine() { return d_te; }
-  /** get equality query object for the given type. The default is the
-      generic one */
+  /** get equality query */
   EqualityQueryQuantifiersEngine* getEqualityQuery();
   /** get default sat context for quantifiers engine */
   context::Context* getSatContext();
@@ -224,6 +231,8 @@ public:  //modules
   quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; }
   /** local theory ext partial inst */
   quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; }
+  /** function definition engine */
+  quantifiers::FunDefEngine * getFunDefEngine() { return d_fun_def_engine; }
 private:
   /** owner of quantified formulas */
   std::map< Node, QuantifiersModule * > d_owner;
@@ -250,6 +259,8 @@ public:
   /** get next decision request */
   Node getNextDecisionRequest();
 private:
+  /** reduce quantifier */
+  bool reduceQuantifier( Node q );
   /** compute term vector */
   void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
   /** instantiate f with arguments terms */
@@ -322,6 +333,8 @@ public:
     IntStat d_simple_triggers;
     IntStat d_multi_triggers;
     IntStat d_multi_trigger_instantiations;
+    IntStat d_red_alpha_equiv;
+    IntStat d_red_lte_partial_inst;
     Statistics();
     ~Statistics();
   };/* class QuantifiersEngine::Statistics */
@@ -337,20 +350,18 @@ private:
   /** pointer to theory engine */
   QuantifiersEngine* d_qe;
   /** internal representatives */
-  std::map< Node, Node > d_int_rep;
+  std::map< TypeNode, std::map< Node, Node > > d_int_rep;
   /** rep score */
   std::map< Node, int > d_rep_score;
   /** reset count */
   int d_reset_count;
-
-  bool d_liberal;
 private:
   /** node contains */
   Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache );
   /** get score */
-  int getRepScore( Node n, Node f, int index );
+  int getRepScore( Node n, Node f, int index, TypeNode v_tn );
 public:
-  EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ), d_liberal( false ){}
+  EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ){}
   ~EqualityQueryQuantifiersEngine(){}
   /** reset */
   void reset();
@@ -368,8 +379,6 @@ public:
   Node getInternalRepresentative( Node a, Node f, int index );
   /** flatten representatives */
   void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
-
-  void setLiberal( bool l ) { d_liberal = l; }
 }; /* EqualityQueryQuantifiersEngine */
 
 }/* CVC4::theory namespace */
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index eb05564e5..6a64f762e 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -16,6 +16,7 @@
 #include "theory/type_enumerator.h"
 #include "theory/quantifiers/bounded_integers.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/first_order_model.h"
 
 using namespace std;
 using namespace CVC4;
@@ -187,8 +188,14 @@ bool RepSetIterator::initialize(){
     TypeNode tn = d_types[i];
     Trace("rsi") << "Var #" << i << " is type " << tn << "..." << std::endl;
     if( tn.isSort() ){
+      //must ensure uninterpreted type is non-empty.
       if( !d_rep_set->hasType( tn ) ){
-        Node var = NodeManager::currentNM()->mkSkolem( "repSet", tn, "is a variable created by the RepSetIterator" );
+        //FIXME:
+        // terms in rep_set are now constants which mapped to terms through TheoryModel
+        // thus, should introduce a constant and a term.  for now, just a term.
+        
+        //Node c = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 );
+        Node var = d_qe->getModel()->getSomeDomainElement( tn );
         Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
         d_rep_set->add( tn, var );
       }
@@ -216,15 +223,18 @@ bool RepSetIterator::initialize(){
           d_incomplete = true;
         }
       }
-    //enumerate if the sort is reasonably small, not an Array, the upper bound of 1000 is chosen arbitrarily for now
+    //enumerate if the sort is reasonably small
     }else if( d_qe->getTermDatabase()->mayComplete( tn ) ){
       Trace("rsi") << "  do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl;
       d_rep_set->complete( tn );
+      //must have succeeded
+      Assert( d_rep_set->hasType( tn ) );
     }else{
       Trace("rsi") << "  variable cannot be bounded." << std::endl;
       Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl;
       d_incomplete = true;
     }
+    //if we have yet to determine the type of enumeration
     if( d_enum_type.size()<=i ){
       d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS );
       if( d_rep_set->hasType( tn ) ){
diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h
index 551c0b0ee..fa8f108c3 100644
--- a/src/theory/sets/theory_sets_type_enumerator.h
+++ b/src/theory/sets/theory_sets_type_enumerator.h
@@ -62,6 +62,7 @@ public:
   // by the TypeEnumerator framework.
   SetEnumerator(const SetEnumerator& ae) throw() :
     TypeEnumeratorBase<SetEnumerator>(ae.d_nm->mkSetType(ae.d_constituentType)),
+    d_index(ae.d_index),
     d_constituentType(ae.d_constituentType),
     d_nm(ae.d_nm),
     d_indexVec(ae.d_indexVec),
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 52b018234..05d0c896a 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -478,6 +478,14 @@ void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cac
   cache.insert(n);
 }
 
+void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel ) {
+  constantReps[eqc] = const_rep;
+  Trace("model-builder") << "    Assign: Setting constant rep of " << eqc << " to " << const_rep << endl;
+  if( !fullModel ){
+    tm->d_rep_set.d_values_to_terms[const_rep] = eqc;
+  }
+}
+
 
 void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
 {
@@ -551,7 +559,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
     if (!const_rep.isNull()) {
       // Theories should not specify a rep if there is already a constant in the EC
       Assert(rep.isNull() || rep == const_rep);
-      constantReps[eqc] = const_rep;
+      assignConstantRep( tm, constantReps, eqc, const_rep, fullModel );
       typeConstSet.add(eqct.getBaseType(), const_rep);
     }
     else if (!rep.isNull()) {
@@ -615,7 +623,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
                 Node normalized = normalize(tm, n, constantReps, true);
                 if (normalized.isConst()) {
                   typeConstSet.add(tb, normalized);
-                  constantReps[*i2] = normalized;
+                  assignConstantRep( tm, constantReps, *i2, normalized, fullModel );
                   Trace("model-builder") << "    Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl;
                   changed = true;
                   evaluated = true;
@@ -648,7 +656,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
             if (normalized.isConst()) {
               changed = true;
               typeConstSet.add(tb, normalized);
-              constantReps[*i] = normalized;
+              assignConstantRep( tm, constantReps, *i, normalized, fullModel );
               assertedReps.erase(*i);
               i2 = i;
               ++i;
@@ -727,11 +735,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
             n = *te;
           }
           Assert(!n.isNull());
-          constantReps[*i2] = n;
-          Trace("model-builder") << "    Assign: Setting constant rep of " << (*i2) << " to " << n << endl;
-          if( !fullModel ){
-            tm->d_rep_set.d_values_to_terms[n] = (*i2);
-          }
+          assignConstantRep( tm, constantReps, *i2, n, fullModel );
           changed = true;
           noRepSet.erase(i2);
           if (assignOne) {
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index be202fb69..a161f02f4 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -261,7 +261,7 @@ protected:
   Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly);
   bool isAssignable(TNode n);
   void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache);
-
+  void assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel );
 public:
   TheoryEngineModelBuilder(TheoryEngine* te);
   virtual ~TheoryEngineModelBuilder(){}