From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 25 Jul 2015 14:40:54 +0000 (+0200)
Subject: Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/post... 
X-Git-Tag: cvc5-1.0.0~6267^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c0079b3110a81f2ff993b7f86782266380dd102e;p=cvc5.git

Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/post conditions.  Dump synth by default in sygus, update regressions.  Set better defaults for induction. Fix bug in related to IFF and EQUAL in sygus grammar.
---

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 653eaca8f..b9e951f7b 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -213,9 +213,13 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   }
 
   // if doing sygus, turn on CEGQI by default
-  if(opts[options::inputLanguage] == language::input::LANG_SYGUS &&
-     !opts.wasSetByUser(options::ceGuidedInst)) {
-    opts.set(options::ceGuidedInst, true);
+  if(opts[options::inputLanguage] == language::input::LANG_SYGUS ){
+    if( !opts.wasSetByUser(options::ceGuidedInst)) {
+      opts.set(options::ceGuidedInst, true);
+    }
+    if( !opts.wasSetByUser(options::dumpSynth)) {
+      opts.set(options::dumpSynth, true);
+    }
   }
 
   // Determine which messages to show based on smtcomp_mode and verbosity
@@ -572,7 +576,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     // make sure out and err streams are flushed too
     *opts[options::out] << flush;
     *opts[options::err] << flush;
- 
+
 #ifdef CVC4_DEBUG
     if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) {
       _exit(returnValue);
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index b8c4793d4..9ee6d24b4 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -517,7 +517,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
   startIndex = -1;
   Debug("parser-sygus") << "Construct default grammar for " << fun << " " << range << std::endl;
   std::map< CVC4::Type, CVC4::Type > sygus_to_builtin;
-  
+
   std::vector< Type > types;
   for( unsigned i=0; i<sygus_vars.size(); i++ ){
     Type t = sygus_vars[i].getType();
@@ -525,13 +525,13 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin
       types.push_back( t );
     }
   }
-  
+
   //name of boolean sort
   std::stringstream ssb;
   ssb << fun << "_Bool";
   std::string dbname = ssb.str();
   Type unres_bt = mkUnresolvedType(ssb.str());
-  
+
   std::vector< Type > unres_types;
   for( unsigned i=0; i<types.size(); i++ ){
     std::stringstream ss;
@@ -700,7 +700,7 @@ void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& o
 
 //  This method adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1)
 //  This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
-void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,                               
+void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
                               std::vector< CVC4::Datatype >& datatypes,
                               std::vector< CVC4::Type>& sorts,
                               std::vector< std::vector<CVC4::Expr> >& ops,
@@ -708,14 +708,37 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
                               std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
                               std::vector< bool >& allow_const,
                               std::vector< std::vector< std::string > >& unresolved_gterm_sym,
-                              std::vector<CVC4::Expr>& sygus_vars, 
-                              std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, 
+                              std::vector<CVC4::Expr>& sygus_vars,
+                              std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr,
                               CVC4::Type& ret, bool isNested ){
   if( sgt.d_gterm_type==SygusGTerm::gterm_op || sgt.d_gterm_type==SygusGTerm::gterm_let ){
     Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index << std::endl;
-    //convert to UMINUS if one child of -
+    Kind oldKind;
+    Kind newKind = kind::UNDEFINED_KIND;
+    //convert to UMINUS if one child of MINUS
     if( sgt.d_children.size()==1 && sgt.d_expr==getExprManager()->operatorOf(kind::MINUS) ){
-      sgt.d_expr = getExprManager()->operatorOf(kind::UMINUS);
+      oldKind = kind::MINUS;
+      newKind = kind::UMINUS;
+    }
+    //convert to IFF if boolean EQUAL
+    if( sgt.d_expr==getExprManager()->operatorOf(kind::EQUAL) ){
+      Type ctn = sgt.d_children[0].d_type;
+      std::map< CVC4::Type, CVC4::Type >::iterator it = sygus_to_builtin.find( ctn );
+      if( it != sygus_to_builtin.end() && it->second.isBoolean() ){
+        oldKind = kind::EQUAL;
+        newKind = kind::IFF;
+      }
+    }
+    if( newKind!=kind::UNDEFINED_KIND ){
+      Expr newExpr = getExprManager()->operatorOf(newKind);
+      Debug("parser-sygus") << "Replace " << sgt.d_expr << " with " << newExpr << std::endl;
+      sgt.d_expr = newExpr;
+      std::string oldName = kind::kindToString(oldKind);
+      std::string newName = kind::kindToString(newKind);
+      size_t pos = 0;
+      if((pos = sgt.d_name.find(oldName, pos)) != std::string::npos){
+        sgt.d_name.replace(pos, oldName.length(), newName);
+      }
     }
     ops[index].push_back( sgt.d_expr );
     cnames[index].push_back( sgt.d_name );
@@ -730,16 +753,16 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
       int sub_dt_index = datatypes.size()-1;
       //process child
       Type sub_ret;
-      processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, 
+      processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
                          sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret, true );
       //process the nested gterm (either pop the last datatype, or flatten the argument)
-      Type tt = processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, 
+      Type tt = processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
                                          sygus_to_builtin, sygus_to_builtin_expr, sub_ret );
       cargs[index].back().push_back(tt);
     }
     //if let, must create operator
     if( sgt.d_gterm_type==SygusGTerm::gterm_let ){
-      processSygusLetConstructor( sgt.d_let_vars, index, datatypes, sorts, ops, cnames, cargs, 
+      processSygusLetConstructor( sgt.d_let_vars, index, datatypes, sorts, ops, cnames, cargs,
                                   sygus_vars, sygus_to_builtin, sygus_to_builtin_expr );
     }
   }else if( sgt.d_gterm_type==SygusGTerm::gterm_constant ){
@@ -790,7 +813,7 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
       unresolved_gterm_sym[index].push_back(sgt.d_name);
     }
   }else if( sgt.d_gterm_type==SygusGTerm::gterm_ignore ){
-    
+
   }
 }
 
@@ -828,7 +851,7 @@ bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes,
   unresolved_gterm_sym.pop_back();
   return true;
 }
-  
+
 Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes,
                                     std::vector< CVC4::Type>& sorts,
                                     std::vector< std::vector<CVC4::Expr> >& ops,
@@ -836,7 +859,7 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
                                     std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
                                     std::vector< bool >& allow_const,
                                     std::vector< std::vector< std::string > >& unresolved_gterm_sym,
-                                    std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, 
+                                    std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
                                     std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ) {
   Type t = sub_ret;
   Debug("parser-sygus") << "Argument is ";
@@ -907,13 +930,13 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
 }
 
 void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
-                                       int index, 
+                                       int index,
                                        std::vector< CVC4::Datatype >& datatypes,
                                        std::vector< CVC4::Type>& sorts,
                                        std::vector< std::vector<CVC4::Expr> >& ops,
                                        std::vector< std::vector<std::string> >& cnames,
                                        std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
-                                       std::vector<CVC4::Expr>& sygus_vars, 
+                                       std::vector<CVC4::Expr>& sygus_vars,
                                        std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
                                        std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr ) {
   std::vector< CVC4::Expr > let_define_args;
@@ -953,30 +976,30 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
         Debug("parser-sygus") << "    cons 0, selector " << j << " : " << cargs[i][0][j] << " " << bt << std::endl;
       }
     }
-  } 
+  }
   */
   //last argument is the return, pop
   cargs[index][dindex].pop_back();
-  collectSygusLetArgs( let_body, cargs[index][dindex], let_define_args );  
-  
+  collectSygusLetArgs( let_body, cargs[index][dindex], let_define_args );
+
   Debug("parser-sygus") << "Make define-fun with " << cargs[index][dindex].size() << " arguments..." << std::endl;
   std::vector<CVC4::Type> fsorts;
   for( unsigned i=0; i<cargs[index][dindex].size(); i++ ){
     Debug("parser-sygus") << "  " << i << " : " << let_define_args[i] << " " << let_define_args[i].getType() << " " << cargs[index][dindex][i] << std::endl;
     fsorts.push_back(let_define_args[i].getType());
   }
-  
+
   Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType());
   std::stringstream ss;
   ss << datatypes[index].getName() << "_let";
   Expr let_func = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
   preemptCommand( new DefineFunctionCommand(ss.str(), let_func, let_define_args, let_body) );
-  
+
   ops[index].pop_back();
   ops[index].push_back( let_func );
   cnames[index].pop_back();
   cnames[index].push_back(ss.str());
-  
+
   //mark function as let constructor
   d_sygus_let_func_to_vars[let_func].insert( d_sygus_let_func_to_vars[let_func].end(), let_define_args.begin(), let_define_args.end() );
   d_sygus_let_func_to_body[let_func] = let_body;
@@ -997,12 +1020,12 @@ void Smt2::collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusAr
     }
   }else{
     for( unsigned i=0; i<e.getNumChildren(); i++ ){
-      collectSygusLetArgs( e[i], sygusArgs, builtinArgs );      
-    } 
+      collectSygusLetArgs( e[i], sygusArgs, builtinArgs );
+    }
   }
 }
 
-void Smt2::setSygusStartIndex( std::string& fun, int startIndex, 
+void Smt2::setSygusStartIndex( std::string& fun, int startIndex,
                                std::vector< CVC4::Datatype >& datatypes,
                                std::vector< CVC4::Type>& sorts,
                                std::vector< std::vector<CVC4::Expr> >& ops ) {
@@ -1093,7 +1116,7 @@ void Smt2::defineSygusFuns() {
 
 void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
                             std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs,
-                            std::vector<std::string>& unresolved_gterm_sym, 
+                            std::vector<std::string>& unresolved_gterm_sym,
                             std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ) {
   Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl;
   Debug("parser-sygus") << "  add constructors..." << std::endl;
@@ -1149,7 +1172,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
       Debug("parser-sygus") << ": replace " << ops[i] << " " << ops[i].getKind() << " " << sk << std::endl;
       let_body = getExprManager()->mkExpr( sk, children );
       Debug("parser-sygus") << ": new body of function is " << let_body << std::endl;
-      
+
       Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType());
       Debug("parser-sygus") << ": function type is " << ft << std::endl;
       std::stringstream ss;
@@ -1206,7 +1229,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
       }
     }
   }
-  
+
 }
 
 void Smt2::addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs,
diff --git a/src/smt/options b/src/smt/options
index 077acc6e9..7c725e508 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -37,7 +37,7 @@ option dumpProofs --dump-proofs bool :default false :link --proof
  output proofs after every UNSAT/VALID response
 option dumpInstantiations --dump-instantiations bool :default false
  output instantiations of quantified formulas after every UNSAT/VALID response
-option dumpSynth --dump-synth bool :default false
+option dumpSynth --dump-synth bool :read-write :default false
  output solution for synthesis conjectures after every UNSAT/VALID response
 option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  turn on unsat core generation
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 921583ed2..fa145813c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1465,6 +1465,13 @@ void SmtEngine::setDefaults() {
     if( !options::dtForceAssignment.wasSetByUser() ){
       options::dtForceAssignment.set( true );
     }
+    //try to remove ITEs from quantified formulas
+    if( !options::iteDtTesterSplitQuant.wasSetByUser() ){
+      options::iteDtTesterSplitQuant.set( true );
+    }
+    if( !options::iteLiftQuant.wasSetByUser() ){
+      options::iteLiftQuant.set( quantifiers::ITE_LIFT_QUANT_MODE_ALL );
+    }
   }
   if( options::intWfInduction() ){
     if( !options::purifyTriggers.wasSetByUser() ){
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 045407bf0..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 );
@@ -211,7 +219,7 @@ 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;
   }
 }
@@ -229,7 +237,7 @@ Node CegInstantiation::getNextDecisionRequest() {
       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 ) ) {
@@ -251,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++ ){
@@ -263,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 );
@@ -303,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() );
@@ -334,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 );
@@ -497,11 +507,12 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
     //  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() );
@@ -514,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")) ){
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 5f393626c..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;
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index b7bbf8a93..ef2e3005e 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -810,6 +810,7 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
   }
   //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
@@ -826,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];
@@ -840,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() );
@@ -868,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];
@@ -897,7 +910,6 @@ 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;
       Node pbvl;
       if( !pbvs.empty() ){
         pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs );
@@ -906,6 +918,8 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
         //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;
@@ -917,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;
           }
@@ -941,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;
@@ -948,75 +981,163 @@ 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 );
-          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;
+          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;
+                }
               }
             }
+            */
           }
-          */
         }
       }
     }
@@ -1146,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 ) ){
@@ -1371,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;
@@ -1429,4 +1612,5 @@ bool CegConjectureSingleInv::needsCheck() {
   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 f8e3879ac..f0d00b61c 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -111,6 +111,9 @@ 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 );
@@ -141,7 +144,7 @@ private:
 public:
   //lemmas produced
   std::vector< Node > d_lemmas_produced;
-  std::vector< std::vector< Node > > d_inst; 
+  std::vector< std::vector< Node > > d_inst;
 private:
   std::vector< Node > d_curr_lemmas;
   //add instantiation
@@ -156,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 );
@@ -165,6 +172,8 @@ 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
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 97ad3e8ea..af2d88e94 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -152,6 +152,15 @@ typedef enum {
   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 ab0526471..5cb9062e4 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -32,7 +32,7 @@ option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuan
  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 iteDtTesterSplitQuant --ite-dtt-split-quant bool :default false
+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
@@ -240,6 +240,9 @@ 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
   
+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
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index c518813a0..4d2276621 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -217,6 +217,19 @@ 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") {
@@ -443,6 +456,22 @@ inline IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string
   }
 }
 
+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/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index fa0e211b3..c6115195d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -781,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 ]);
 }
 
@@ -1754,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() );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ccbbd5bd5..54f2a16fe 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -754,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 );
 }
 
diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy
index 5d8cd8752..56a30b210 100644
--- a/test/regress/regress0/sygus/array_search_2.sy
+++ b/test/regress/regress0/sygus/array_search_2.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 (synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
 (declare-var x1 Int)
diff --git a/test/regress/regress0/sygus/array_sum_2_5.sy b/test/regress/regress0/sygus/array_sum_2_5.sy
index 48b5c8a4d..f6c0320e2 100644
--- a/test/regress/regress0/sygus/array_sum_2_5.sy
+++ b/test/regress/regress0/sygus/array_sum_2_5.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 (synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int ( 0 1 2 y1 y2 (+ Start Start)    (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
 (declare-var x1 Int)
diff --git a/test/regress/regress0/sygus/commutative.sy b/test/regress/regress0/sygus/commutative.sy
index 15567b0a8..46dbd2981 100644
--- a/test/regress/regress0/sygus/commutative.sy
+++ b/test/regress/regress0/sygus/commutative.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy
index 0d753bdf1..428cb2adc 100644
--- a/test/regress/regress0/sygus/const-var-test.sy
+++ b/test/regress/regress0/sygus/const-var-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/constant.sy b/test/regress/regress0/sygus/constant.sy
index ddc12a6a9..0059f6947 100644
--- a/test/regress/regress0/sygus/constant.sy
+++ b/test/regress/regress0/sygus/constant.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/dup-op.sy b/test/regress/regress0/sygus/dup-op.sy
index dbf415986..e5448d626 100644
--- a/test/regress/regress0/sygus/dup-op.sy
+++ b/test/regress/regress0/sygus/dup-op.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-cegqi-si
+; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ Con Con) (+ Start Start) x))
diff --git a/test/regress/regress0/sygus/enum-test.sy b/test/regress/regress0/sygus/enum-test.sy
index 52a72c07d..cd129385e 100644
--- a/test/regress/regress0/sygus/enum-test.sy
+++ b/test/regress/regress0/sygus/enum-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 (define-sort D (Enum (a b)))
 (define-fun f ((x D)) Int (ite (= x D::a) 3 7))
diff --git a/test/regress/regress0/sygus/hd-01-d1-prog.sy b/test/regress/regress0/sygus/hd-01-d1-prog.sy
index a58bc2f64..2e6c6ef81 100644
--- a/test/regress/regress0/sygus/hd-01-d1-prog.sy
+++ b/test/regress/regress0/sygus/hd-01-d1-prog.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
 
 (set-logic BV)
 
@@ -8,12 +8,12 @@
 (synth-fun f ((x (BitVec 32))) (BitVec 32)
     ((Start (BitVec 32) ((bvand Start Start)
                          (bvsub Start Start)
-						 (bvor Start Start)
-						 (bvadd Start Start)
-						 (bvxor Start Start)
+             (bvor Start Start)
+             (bvadd Start Start)
+             (bvxor Start Start)
                          x
-						 #x00000000
-						 #xFFFFFFFF
+             #x00000000
+             #xFFFFFFFF
                          #x00000001))))
 
 (declare-var x (BitVec 32))
diff --git a/test/regress/regress0/sygus/icfp_28_10.sy b/test/regress/regress0/sygus/icfp_28_10.sy
index 6e1610337..b07be0e98 100644
--- a/test/regress/regress0/sygus/icfp_28_10.sy
+++ b/test/regress/regress0/sygus/icfp_28_10.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
 
 (set-logic BV)
 
@@ -14,14 +14,14 @@
 
 (Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
                     (shl1 Start)
- 		    (shr1 Start)
-		    (shr4 Start)
-		    (shr16 Start)
-		    (bvand Start Start)
-		    (bvor Start Start)
-		    (bvxor Start Start)
-		    (bvadd Start Start)
-		    (if0 Start Start Start)
+        (shr1 Start)
+        (shr4 Start)
+        (shr16 Start)
+        (bvand Start Start)
+        (bvor Start Start)
+        (bvxor Start Start)
+        (bvadd Start Start)
+        (if0 Start Start Start)
  ))
 )
 )
diff --git a/test/regress/regress0/sygus/inv-example.sy b/test/regress/regress0/sygus/inv-example.sy
index dda8e0ed5..aafbbd987 100644
--- a/test/regress/regress0/sygus/inv-example.sy
+++ b/test/regress/regress0/sygus/inv-example.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 (synth-inv inv-f ((x Int) (y Int) (b Bool)))
 (declare-primed-var x Int)
diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy
index 046d074d9..4bae90b00 100644
--- a/test/regress/regress0/sygus/let-ringer.sy
+++ b/test/regress/regress0/sygus/let-ringer.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 (define-fun g ((x Int)) Int (ite (= x 1) 15 19))
 (synth-fun f ((x Int)) Int
diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy
index daca906a2..71cd27e8f 100644
--- a/test/regress/regress0/sygus/let-simp.sy
+++ b/test/regress/regress0/sygus/let-simp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 (synth-fun f ((x Int) (y Int)) Int
     ((Start Int (x
diff --git a/test/regress/regress0/sygus/max.sy b/test/regress/regress0/sygus/max.sy
index 4fc515353..dec4594d7 100644
--- a/test/regress/regress0/sygus/max.sy
+++ b/test/regress/regress0/sygus/max.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 
 (synth-fun max ((x Int) (y Int)) Int
diff --git a/test/regress/regress0/sygus/multi-fun-polynomial2.sy b/test/regress/regress0/sygus/multi-fun-polynomial2.sy
index 24d49ee4e..6d185ba3f 100644
--- a/test/regress/regress0/sygus/multi-fun-polynomial2.sy
+++ b/test/regress/regress0/sygus/multi-fun-polynomial2.sy
@@ -1,13 +1,13 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
 
 (set-logic LIA)
 
 (synth-fun addExpr1 ((x Int) (y Int)) Int
     ((Start Int (x
                  y
-		 0
-		 1
+     0
+     1
                  (+ Start Start)
                  (- Start Start)
                  ))
@@ -16,8 +16,8 @@
 (synth-fun addExpr2 ((x Int) (y Int)) Int
     ((Start Int (x
                  y
-		 0
-		 1
+     0
+     1
                  (+ Start Start)
                  (- Start Start)
                  ))
diff --git a/test/regress/regress0/sygus/nflat-fwd-3.sy b/test/regress/regress0/sygus/nflat-fwd-3.sy
index bd7c79e3e..9065a1025 100644
--- a/test/regress/regress0/sygus/nflat-fwd-3.sy
+++ b/test/regress/regress0/sygus/nflat-fwd-3.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ (+ Con Con) Con) x))
diff --git a/test/regress/regress0/sygus/nflat-fwd.sy b/test/regress/regress0/sygus/nflat-fwd.sy
index 0f9d46215..d211d475b 100644
--- a/test/regress/regress0/sygus/nflat-fwd.sy
+++ b/test/regress/regress0/sygus/nflat-fwd.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ Con Con) (+ (+ Start Start) Con) x))
diff --git a/test/regress/regress0/sygus/no-flat-simp.sy b/test/regress/regress0/sygus/no-flat-simp.sy
index 81f90e2aa..cb284b180 100755
--- a/test/regress/regress0/sygus/no-flat-simp.sy
+++ b/test/regress/regress0/sygus/no-flat-simp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/no-syntax-test-bool.sy b/test/regress/regress0/sygus/no-syntax-test-bool.sy
index cc3855ad1..4b3fa22e6 100644
--- a/test/regress/regress0/sygus/no-syntax-test-bool.sy
+++ b/test/regress/regress0/sygus/no-syntax-test-bool.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/no-syntax-test-no-si.sy b/test/regress/regress0/sygus/no-syntax-test-no-si.sy
index 21788426c..86b60638b 100644
--- a/test/regress/regress0/sygus/no-syntax-test-no-si.sy
+++ b/test/regress/regress0/sygus/no-syntax-test-no-si.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/no-syntax-test.sy b/test/regress/regress0/sygus/no-syntax-test.sy
index 95f9b7c11..b95f31aa7 100644
--- a/test/regress/regress0/sygus/no-syntax-test.sy
+++ b/test/regress/regress0/sygus/no-syntax-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/parity-AIG-d0.sy b/test/regress/regress0/sygus/parity-AIG-d0.sy
index c4fbd1c17..03d180634 100644
--- a/test/regress/regress0/sygus/parity-AIG-d0.sy
+++ b/test/regress/regress0/sygus/parity-AIG-d0.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic BV)
 
 (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
diff --git a/test/regress/regress0/sygus/tl-type.sy b/test/regress/regress0/sygus/tl-type.sy
index a8da13742..1545f86cd 100644
--- a/test/regress/regress0/sygus/tl-type.sy
+++ b/test/regress/regress0/sygus/tl-type.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-cegqi-si
+; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int (Term (+ Start Start)))
diff --git a/test/regress/regress0/sygus/twolets1.sy b/test/regress/regress0/sygus/twolets1.sy
index 24b0f2c09..7f84ce06c 100644
--- a/test/regress/regress0/sygus/twolets1.sy
+++ b/test/regress/regress0/sygus/twolets1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 
 ;; f1 is x plus 2 ;; f2 is 2x plus 5
@@ -7,27 +7,27 @@
 (define-fun let0 ((x Int) (y Int) (z Int)) Int (+ (+ y x) z))
 
 (synth-fun f1 ((x Int)) Int
-	   (
-	   (Start Int (
-	   	      (let0 Intx CInt CInt)
-	   	      )
- 	   )
- 	   (Intx Int (x))
-	   (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
-
-	   )
+     (
+     (Start Int (
+            (let0 Intx CInt CInt)
+            )
+     )
+     (Intx Int (x))
+     (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+
+     )
 )
 
 (synth-fun f2 ((x Int)) Int
-	   (
-	   (Start Int (x
-	   	      (let0 Intx Start CInt)
-	   	      )
- 	   )
+     (
+     (Start Int (x
+            (let0 Intx Start CInt)
+            )
+     )
      (Intx Int (x))
-	   (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+     (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
 
-	   )
+     )
 )
 
 
diff --git a/test/regress/regress0/sygus/twolets2-orig.sy b/test/regress/regress0/sygus/twolets2-orig.sy
index c1066277e..91bab5ece 100644
--- a/test/regress/regress0/sygus/twolets2-orig.sy
+++ b/test/regress/regress0/sygus/twolets2-orig.sy
@@ -1,25 +1,25 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 (synth-fun f1 ((x Int)) Int
-	   (
-	   (Start Int (
-	   	      (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z))
-	   	      )
- 	   )
-	   (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+     (
+     (Start Int (
+            (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z))
+            )
+     )
+     (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
 
-	   )
+     )
 )
 (synth-fun f2 ((x Int)) Int
-	   (
-	   (Start Int (x
-	   	      (let ((y Int Start) (z Int CInt)) (+ (+ y x) z))
-	   	      )
- 	   )
-	   (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+     (
+     (Start Int (x
+            (let ((y Int Start) (z Int CInt)) (+ (+ y x) z))
+            )
+     )
+     (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
 
-	   )
+     )
 )
 (declare-var x1 Int)
 (declare-var x2 Int)
diff --git a/test/regress/regress0/sygus/uminus_one.sy b/test/regress/regress0/sygus/uminus_one.sy
index b020c0bee..9886f6a7b 100644
--- a/test/regress/regress0/sygus/uminus_one.sy
+++ b/test/regress/regress0/sygus/uminus_one.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
 (set-logic LIA)
 (synth-fun f ((x Int)) Int ((Start Int ((- 1)))))
 (declare-var x Int)
diff --git a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
index dc39efd84..7c9d6c601 100644
--- a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
+++ b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
 
 (set-logic LIA)
 (synth-fun inv ((x Int)) Bool