From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 1 Apr 2015 11:09:49 +0000 (+0200)
Subject: Improvements and bug fixes related to cbqi/cegqi.  Minor fix for fmf with fun-def... 
X-Git-Tag: cvc5-1.0.0~6367
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3ac872f4a3f65bd1b38c1362b8ca9d351ed89333;p=cvc5.git

Improvements and bug fixes related to cbqi/cegqi.  Minor fix for fmf with fun-def. Add skolemization options.
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7844cede5..cb18b8464 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -866,7 +866,7 @@ SmtEngine::~SmtEngine() throw() {
 
     PROOF(delete d_proofManager;);
     PROOF(d_proofManager = NULL;);
-    
+
     delete d_stats;
     d_stats = NULL;
     delete d_statisticsRegistry;
@@ -1342,12 +1342,15 @@ void SmtEngine::setDefaults() {
       if( !options::preSkolemQuant.wasSetByUser() ){
         options::preSkolemQuant.set( true );
       }
+      if( !options::preSkolemQuantNested.wasSetByUser() ){
+        options::preSkolemQuantNested.set( true );
+      }
       if( !options::fmfOneInstPerRound.wasSetByUser() ){
         options::fmfOneInstPerRound.set( true );
       }
     }
   }
-  
+
   //apply counterexample guided instantiation options
   if( options::cegqiSingleInv() ){
     options::ceGuidedInst.set( true );
@@ -1376,10 +1379,17 @@ void SmtEngine::setDefaults() {
     }
   }
 
-  //implied options...
+  //cbqi options
   if( options::recurseCbqi() || options::cbqi2() ){
     options::cbqi.set( true );
   }
+  if( options::cbqi() ){
+    if( !options::quantConflictFind.wasSetByUser() ){
+      options::quantConflictFind.set( false );
+    }
+  }
+
+  //implied options...
   if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){
     options::quantConflictFind.set( true );
   }
@@ -3430,10 +3440,10 @@ void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput)
 
   Trace("smt") << "SmtEnginePrivate::addFormula(" << n << "), inUnsatCore = " << inUnsatCore << ", inInput = " << inInput << endl;
   // Give it to proof manager
-  PROOF( 
+  PROOF(
     if( inInput ){
       // n is an input assertion
-      ProofManager::currentPM()->addAssertion(n.toExpr(), inUnsatCore); 
+      ProofManager::currentPM()->addAssertion(n.toExpr(), inUnsatCore);
     }else{
       // n is the result of an unknown preprocessing step, add it to dependency map to null
       ProofManager::currentPM()->addDependence(n, Node::null());
@@ -3634,7 +3644,7 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeChec
   SmtScope smts(this);
   finalOptionsAreSet();
   doPendingPops();
-  
+
   Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl;
 
   // Substitute out any abstract values in ex
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 0fef2aa42..7d1c06b8e 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -31,11 +31,13 @@ using namespace CVC4::theory::quantifiers;
 using namespace std;
 
 namespace CVC4 {
-  
+
 CegInstantiator::CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out ) : d_qe( qe ), d_out( out ){
-  
-}  
-  
+  d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
+  d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
+  d_true = NodeManager::currentNM()->mkConst( true );
+}
+
 void CegInstantiator::computeProgVars( Node n ){
   if( d_prog_var.find( n )==d_prog_var.end() ){
     d_prog_var[n].clear();
@@ -51,14 +53,20 @@ void CegInstantiator::computeProgVars( Node n ){
         d_inelig[n] = true;
         return;
       }
+      if( d_has_delta.find( n[i] )!=d_has_delta.end() ){
+        d_has_delta[n] = true;
+      }
       for( std::map< Node, bool >::iterator it = d_prog_var[n[i]].begin(); it != d_prog_var[n[i]].end(); ++it ){
         d_prog_var[n][it->first] = true;
       }
     }
+    if( n==d_n_delta ){
+      d_has_delta[n] = true;
+    }
   }
 }
 
-bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, 
+bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars,
                                         std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
                                         unsigned i, unsigned effort ){
   if( i==d_vars.size() ){
@@ -69,7 +77,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
     //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]];
     Node pv = d_vars[i];
     TypeNode pvtn = pv.getType();
-    
+
     if( (i+1)<d_vars.size() || effort!=2 ){
       //[1] easy case : pv is in the equivalence class as another term not containing pv
       if( ee->hasTerm( pv ) ){
@@ -78,7 +86,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
         while( !eqc_i.isFinished() ){
           Node n = *eqc_i;
           if( n!=pv ){
-            Trace("cegqi-si-inst-debug") << i << "...try based on equal term " << n << std::endl;
+            Trace("cegqi-si-inst-debug") << "[1] " << i << "...try based on equal term " << n << std::endl;
             //compute d_subs_fv, which program variables are contained in n
             computeProgVars( n );
             //must be an eligible term
@@ -97,6 +105,12 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                 ns = n;
                 proc = true;
               }
+              if( d_has_delta.find( ns )!=d_has_delta.end() ){
+                //also must set delta to zero
+                ns = ns.substitute( (TNode)d_n_delta, (TNode)d_zero );
+                ns = Rewriter::rewrite( ns );
+                computeProgVars( ns );
+              }
               if( proc ){
                 //try the substitution
                 subs_proc[0][ns][pv_coeff] = true;
@@ -109,7 +123,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
           ++eqc_i;
         }
       }
-      
+
       //[2] : we can solve an equality for pv
       ///iterate over equivalence classes to find cases where we can solve for the variable
       if( pvtn.isInteger() || pvtn.isReal() ){
@@ -142,7 +156,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                   for( unsigned j=0; j<lhs.size(); j++ ){
                     //if this term or the another has pv in it, try to solve for it
                     if( hasVar || lhs_v[j] ){
-                      Trace("cegqi-si-inst-debug") << i << "...try based on equality " << lhs[j] << " " << ns << std::endl;
+                      Trace("cegqi-si-inst-debug") << "[2] " << i << "...try based on equality " << lhs[j] << " " << ns << std::endl;
                       Node eq_lhs = lhs[j];
                       Node eq_rhs = ns;
                       //make the same coefficient
@@ -163,6 +177,9 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                       Trace("cegqi-si-inst-debug") << "...equality is " << eq << std::endl;
                       std::map< Node, Node > msum;
                       if( QuantArith::getMonomialSumLit( eq, msum ) ){
+                        if( !d_n_delta.isNull() ){
+                          msum.erase( d_n_delta );
+                        }
                         if( Trace.isOn("cegqi-si-inst-debug") ){
                           Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl;
                           QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" );
@@ -199,7 +216,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
           ++eqcs_i;
         }
       }
-      
+
       //[3] directly look at assertions
       TheoryId tid = Theory::theoryOf( pv );
       Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid );
@@ -211,34 +228,42 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
           bool pol = lit.getKind()!=NOT;
           if( tid==THEORY_ARITH ){
             if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol ) ){
-              Assert( atom[1].isConst() );
-              computeProgVars( atom[0] );
+              Assert( atom.getKind()!=GEQ || atom[1].isConst() );
+              Node atom_lhs;
+              Node atom_rhs;
+              if( atom.getKind()==GEQ ){
+                atom_lhs = atom[0];
+                atom_rhs = atom[1];
+              }else{
+                atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] );
+                atom_lhs = Rewriter::rewrite( atom_lhs );
+                atom_rhs = d_zero;
+              }
+
+              computeProgVars( atom_lhs );
               //must be an eligible term
-              if( d_inelig.find( atom[0] )==d_inelig.end() ){
+              if( d_inelig.find( atom_lhs )==d_inelig.end() ){
                 //apply substitution to LHS of atom
-                Node atom_lhs;
-                Node atom_rhs;
-                if( !d_prog_var[atom[0]].empty() ){
+                if( !d_prog_var[atom_lhs].empty() ){
                   Node atom_lhs_coeff;
-                  atom_lhs = applySubstitution( atom[0], subs, vars, coeff, has_coeff, atom_lhs_coeff );
+                  atom_lhs = applySubstitution( atom_lhs, subs, vars, coeff, has_coeff, atom_lhs_coeff );
                   if( !atom_lhs.isNull() ){
                     computeProgVars( atom_lhs );
-                    atom_rhs = atom[1];
                     if( !atom_lhs_coeff.isNull() ){
                       atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) );
                     }
                   }
-                }else{
-                  atom_lhs = atom[0];
-                  atom_rhs = atom[1];
                 }
                 //if it contains pv
                 if( !atom_lhs.isNull() && d_prog_var[atom_lhs].find( pv )!=d_prog_var[atom_lhs].end() ){
                   Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs );
-                  Trace("cegqi-si-inst-debug") << "From assertion : " << atom << ", pol = " << pol << std::endl;
-                  Trace("cegqi-si-inst-debug") << "   substituted : " << satom << ", pol = " << pol << std::endl;
+                  Trace("cegqi-si-inst-debug") << "[3] From assertion : " << atom << ", pol = " << pol << std::endl;
+                  Trace("cegqi-si-inst-debug") << "       substituted : " << satom << ", pol = " << pol << std::endl;
                   std::map< Node, Node > msum;
                   if( QuantArith::getMonomialSumLit( satom, msum ) ){
+                    if( !d_n_delta.isNull() ){
+                      msum.erase( d_n_delta );
+                    }
                     if( Trace.isOn("cegqi-si-inst-debug") ){
                       Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl;
                       QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" );
@@ -295,6 +320,8 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                           if( addInstantiationInc( uval, pv, veq_c, uires, subs, vars, coeff, has_coeff, subs_typ, i, effort ) ){
                             return true;
                           }
+                        }else{
+                          Trace("cegqi-si-inst-debug") << "...already processed." << std::endl;
                         }
                       }
                     }
@@ -306,12 +333,12 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
         }
       }
     }
-    
-    //[4] resort to using value in model     
+
+    //[4] resort to using value in model
     if( effort>0 ){
       Node mv = d_qe->getModel()->getValue( pv );
       Node pv_coeff_m;
-      Trace("cegqi-si-inst-debug") << i << "...try model value " << mv << std::endl;
+      Trace("cegqi-si-inst-debug") << i << "[4] ...try model value " << mv << std::endl;
       return addInstantiationInc( mv, pv, pv_coeff_m, 9, subs, vars, coeff, has_coeff, subs_typ, i, 1 );
     }else{
       return false;
@@ -320,9 +347,9 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
 }
 
 
-bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, 
+bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars,
                                            std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
-                                           unsigned i, unsigned effort ) {         
+                                           unsigned i, unsigned effort ) {
   //must ensure variables have been computed for n
   computeProgVars( n );
   //substitute into previous substitutions, when applicable
@@ -336,7 +363,7 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int s
     a_coeff.push_back( pv_coeff );
     a_has_coeff.push_back( pv );
   }
-  
+
   bool success = true;
   std::map< int, Node > prev_subs;
   std::map< int, Node > prev_coeff;
@@ -413,7 +440,7 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int s
   }
 }
 
-bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, 
+bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars,
                                              std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, unsigned j ) {
   if( j==has_coeff.size() ){
     return addInstantiation( subs, vars, subs_typ );
@@ -446,13 +473,12 @@ bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vec
           if( !veq_c.isNull() ){
             subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c );
             if( subs_typ[index]>=1 && subs_typ[index]<=2 ){
-              subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], 
-                NodeManager::currentNM()->mkNode( ITE, 
-                  NodeManager::currentNM()->mkNode( EQUAL, 
-                    NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), 
-                    NodeManager::currentNM()->mkConst( Rational( 0 ) ) ),
-                  NodeManager::currentNM()->mkConst( Rational( 0 ) ),
-                  NodeManager::currentNM()->mkConst( Rational( 1 ) ) )
+              subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index],
+                NodeManager::currentNM()->mkNode( ITE,
+                  NodeManager::currentNM()->mkNode( EQUAL,
+                    NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ),
+                    d_zero ),
+                  d_zero, d_one )
               );
             }
           }
@@ -463,10 +489,10 @@ bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vec
             //equalities are both upper and lower bounds
             /*
             if( subs_typ[index]==0 && !veq_c.isNull() ){
-              subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], 
-                NodeManager::currentNM()->mkNode( ITE, 
-                  NodeManager::currentNM()->mkNode( EQUAL, 
-                    NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), 
+              subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index],
+                NodeManager::currentNM()->mkNode( ITE,
+                  NodeManager::currentNM()->mkNode( EQUAL,
+                    NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ),
                     NodeManager::currentNM()->mkConst( Rational( 0 ) ) ),
                   NodeManager::currentNM()->mkConst( Rational( 0 ) ),
                   NodeManager::currentNM()->mkConst( Rational( 1 ) ) )
@@ -503,7 +529,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
       prev[i] = subs[i];
       if( d_n_delta.isNull() ){
         d_n_delta = NodeManager::currentNM()->mkSkolem( "delta", vars[i].getType(), "delta for cegqi" );
-        Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) );
+        Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, d_zero );
         d_qe->getOutputChannel().lemma( delta_lem );
       }
       subs[i] = NodeManager::currentNM()->mkNode( subs_typ[i]==2 ? PLUS : MINUS, subs[i], d_n_delta );
@@ -521,7 +547,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
 }
 
 
-Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, 
+Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars,
                                                 std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff ) {
   Assert( d_prog_var.find( n )!=d_prog_var.end() );
   Assert( n==Rewriter::rewrite( n ) );
@@ -603,7 +629,77 @@ Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std:
   }
 }
 
+//check if delta has a lower bound L
+// if so, add lemma L>0 => L>d
+void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) {
+  if( !d_n_delta.isNull() ){
+    Theory* theory = d_qe->getTheoryEngine()->theoryOf( THEORY_ARITH );
+    if( theory && d_qe->getTheoryEngine()->isTheoryEnabled( THEORY_ARITH ) ){
+      context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
+      for (unsigned j = 0; it != it_end; ++ it, ++j) {
+        Node lit = (*it).assertion;
+        Node atom = lit.getKind()==NOT ? lit[0] : lit;
+        bool pol = lit.getKind()!=NOT;
+        if( atom.getKind()==GEQ || ( pol && atom.getKind()==EQUAL ) ){
+          Assert( atom.getKind()!=GEQ || atom[1].isConst() );
+          Node atom_lhs;
+          Node atom_rhs;
+          if( atom.getKind()==GEQ ){
+            atom_lhs = atom[0];
+            atom_rhs = atom[1];
+          }else{
+            atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] );
+            atom_lhs = Rewriter::rewrite( atom_lhs );
+            atom_rhs = d_zero;
+          }
+          computeProgVars( atom_lhs );
+          //must be an eligible term with delta
+          if( d_inelig.find( atom_lhs )==d_inelig.end() && d_has_delta.find( atom_lhs )!=d_has_delta.end() ){
+            Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs );
+            Trace("cegqi-delta") << "Delta assertion : " << atom << ", pol = " << pol << std::endl;
+            std::map< Node, Node > msum;
+            if( QuantArith::getMonomialSumLit( satom, msum ) ){
+              Node vatom;
+              //isolate delta in the inequality
+              int ires = QuantArith::isolate( d_n_delta, msum, vatom, atom.getKind(), true );
+              if( ((ires==1)==pol) || ( ires!=0 && lit.getKind()==EQUAL ) ){
+                Node val = vatom[ ires==1 ? 1 : 0 ];
+                Node pvm = vatom[ ires==1 ? 0 : 1 ];
+                //get monomial
+                if( pvm!=d_n_delta ){
+                  Node veq_c;
+                  Node veq_v;
+                  if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){
+                    Assert( veq_v==d_n_delta );
+                    val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) );
+                    val = Rewriter::rewrite( val );
+                  }else{
+                    val = Node::null();
+                  }
+                }
+                if( !val.isNull()  ){
+                  Node lem1 = NodeManager::currentNM()->mkNode( GT, val, d_zero );
+                  lem1 = Rewriter::rewrite( lem1 );
+                  if( !lem1.isConst() || lem1==d_true ){
+                    Node lem2 = NodeManager::currentNM()->mkNode( GT, val, d_n_delta );
+                    Node lem = lem1==d_true ? lem2 : NodeManager::currentNM()->mkNode( OR, lem1.negate(), lem2 );
+                    lems.push_back( lem );
+                    Trace("cegqi-delta") << "...lemma : " << lem << std::endl;
+                  }
+                }
+              }else{
+                Trace("cegqi-delta") << "...wrong polarity." << std::endl;
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+}
+
 void CegInstantiator::check() {
+
   for( unsigned r=0; r<2; r++ ){
     std::vector< Node > subs;
     std::vector< Node > vars;
@@ -617,18 +713,21 @@ void CegInstantiator::check() {
   }
   Trace("cegqi-engine") << "  WARNING : unable to find CEGQI single invocation instantiation." << std::endl;
 }
-  
-  
+
+
 bool CegqiOutputSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) {
   return d_out->addInstantiation( subs, subs_typ );
 }
-  
+
 bool CegqiOutputSingleInv::isEligibleForInstantiation( Node n ) {
   return d_out->isEligibleForInstantiation( n );
-}  
-  
-  
-  
+}
+
+bool CegqiOutputSingleInv::addLemma( Node n ) {
+  return d_out->addLemma( n );
+}
+
+
 CegConjectureSingleInv::CegConjectureSingleInv( CegConjecture * p ) : d_parent( p ){
   d_sol = NULL;
   d_c_inst_match_trie = NULL;
@@ -651,12 +750,12 @@ Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) {
     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() );
-    
+
     return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst );
   }else{
     return Node::null();
@@ -1056,14 +1155,24 @@ bool CegConjectureSingleInv::isEligibleForInstantiation( Node n ) {
   return n.getKind()!=SKOLEM || std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )!=d_single_inv_arg_sk.end();
 }
 
+bool CegConjectureSingleInv::addLemma( Node n ) {
+  d_curr_lemmas.push_back( n );
+  return true;
+}
+
 void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
   if( !d_single_inv.isNull() ) {
     Assert( d_cinst!=NULL );
     d_curr_lemmas.clear();
-    //call check for instantiator
-    d_cinst->check();
-    //add lemmas
-    lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() );
+    //check if there are delta lemmas
+    d_cinst->getDeltaLemmas( d_curr_lemmas );
+    //if not, do ce-guided instantiation
+    if( d_curr_lemmas.empty() ){
+      //call check for instantiator
+      d_cinst->check();
+      //add lemmas
+      lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() );
+    }
   }
 }
 
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index 9e65b0c24..b5ebe3d7c 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -33,38 +33,47 @@ class CegqiOutput
 public:
   virtual bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) = 0;
   virtual bool isEligibleForInstantiation( Node n ) = 0;
+  virtual bool addLemma( Node lem ) = 0;
 };
 
 class CegInstantiator
 {
 private:
+  Node d_zero;
+  Node d_one;
+  Node d_true;
   QuantifiersEngine * d_qe;
   CegqiOutput * d_out;
   //program variable contains cache
   std::map< Node, std::map< Node, bool > > d_prog_var;
   std::map< Node, bool > d_inelig;
+  std::map< Node, bool > d_has_delta;
 private:
-  Node d_n_delta;
   //for adding instantiations during check
   void computeProgVars( Node n );
   // effort=0 : do not use model value, 1: use model value, 2: one must use model value
-  bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, 
+  bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars,
                          std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
                          unsigned i, unsigned effort );
-  bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, 
+  bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars,
                             std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
                             unsigned i, unsigned effort );
-  bool addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, 
+  bool addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars,
                               std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ,
                               unsigned j );
   bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ );
-  Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, 
-                          std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff = true ); 
+  Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars,
+                          std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff = true );
 public:
   CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out );
   //the CE variables
   std::vector< Node > d_vars;
+  //delta
+  Node d_n_delta;
+  //check : add instantiations based on valuation of d_vars
   void check();
+  // get delta lemmas : on-demand force minimality of d_n_delta
+  void getDeltaLemmas( std::vector< Node >& lems );
 };
 
 
@@ -77,6 +86,7 @@ public:
   CegConjectureSingleInv * d_out;
   bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
   bool isEligibleForInstantiation( Node n );
+  bool addLemma( Node lem );
 };
 
 
@@ -129,6 +139,8 @@ private:
   bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
   //is eligible for instantiation
   bool isEligibleForInstantiation( Node n );
+  // add lemma
+  bool addLemma( Node lem );
 public:
   CegConjectureSingleInv( CegConjecture * p );
   // original conjecture
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index cb772a31f..0bc365ec7 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -38,19 +38,19 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
         Node n = assertions[i][1][0];
         Assert( n.getKind()==APPLY_UF );
         Node f = n.getOperator();
-        
+
         //check if already defined, if so, throw error
         if( d_sorts.find( f )!=d_sorts.end() ){
           Message() << "Cannot define function " << f << " more than once." << std::endl;
           exit( 0 );
         }
-        
+
         //create a sort S that represents the inputs of the function
         std::stringstream ss;
         ss << "I_" << f;
         TypeNode iType = NodeManager::currentNM()->mkSort( ss.str() );
         d_sorts[f] = iType;
-        
+
         //create functions f1...fn mapping from this sort to concrete elements
         for( unsigned j=0; j<n.getNumChildren(); j++ ){
           TypeNode typ = NodeManager::currentNM()->mkFunctionType( iType, n[j].getType() );
@@ -58,7 +58,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
           ss << f << "_arg_" << j;
           d_input_arg_inj[f].push_back( NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during fun def fmf" ) );
         }
-        
+
         //construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn]
         std::vector< Node > children;
         Node bv = NodeManager::currentNM()->mkBoundVar("?i", iType );
@@ -70,7 +70,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
           subs.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], bv ) );
         }
         Node bd = assertions[i][1].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-        
+
         Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << std::endl;
         Trace("fmf-fun-def") << "  to " << std::endl;
         assertions[i] = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
@@ -81,8 +81,9 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
   }
   //second pass : rewrite assertions
   for( unsigned i=0; i<assertions.size(); i++ ){
-    bool is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end();
+    int is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end() ? 1 : 0;
     std::vector< Node > constraints;
+    Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i] << ", is_fd = " << is_fd << std::endl;
     Node n = simplify( assertions[i], true, true, constraints, is_fd );
     Assert( constraints.empty() );
     if( n!=assertions[i] ){
@@ -95,7 +96,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
   }
 }
 
-Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, bool is_fun_def ) {
+Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, int is_fun_def ) {
   Trace("fmf-fun-def-debug") << "Simplify " << n << " " << pol << " " << hasPol << " " << is_fun_def << std::endl;
   if( n.getKind()==FORALL ){
     Node c = simplify( n[1], pol, hasPol, constraints, is_fun_def );
@@ -104,51 +105,51 @@ Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& co
     }else{
       return n;
     }
-  }else if( n.getType().isBoolean() && n.getKind()!=APPLY_UF ){
-    std::vector< Node > children;
-    bool childChanged = false;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      Node c = n[i];
-      //do not process LHS of definition
-      if( !is_fun_def || i!=0 ){
-        bool newHasPol;
-        bool newPol;
-        QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
-        //get child constraints
-        std::vector< Node > cconstraints;
-        c = simplify( n[i], newPol, newHasPol, cconstraints );
-        constraints.insert( constraints.end(), cconstraints.begin(), cconstraints.end() );
+  }else{
+    Node nn = n;
+    bool isBool = n.getType().isBoolean();
+    if( isBool && n.getKind()!=APPLY_UF && is_fun_def!=2 ){
+      std::vector< Node > children;
+      bool childChanged = false;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        Node c = n[i];
+        //do not process LHS of definition
+        if( is_fun_def!=1 || i!=0 ){
+          bool newHasPol;
+          bool newPol;
+          QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
+          //get child constraints
+          std::vector< Node > cconstraints;
+          c = simplify( n[i], newPol, newHasPol, cconstraints, is_fun_def==1 ? 2 : 0 );
+          constraints.insert( constraints.end(), cconstraints.begin(), cconstraints.end() );
+        }
+        children.push_back( c );
+        childChanged = c!=n[i] || childChanged;
       }
-      children.push_back( c );
-      childChanged = c!=n[i] || childChanged;
-    }
-    if( !constraints.empty() || childChanged ){
-      std::vector< Node > c;
       if( childChanged ){
-        c.push_back( NodeManager::currentNM()->mkNode( n.getKind(), children ) );
-      }else{
-        c.push_back( n );
+        nn = n;
       }
-      if( hasPol ){
-        //conjoin with current
-        for( unsigned i=0; i<constraints.size(); i++ ){
-          if( pol ){
-            c.push_back( constraints[i] );
-          }else{
-            c.push_back( constraints[i].negate() );
-          }
+    }else{
+      //simplify term
+      simplifyTerm( n, constraints );
+    }
+    if( !constraints.empty() && isBool && hasPol ){
+      std::vector< Node > c;
+      c.push_back( nn );
+      //conjoin with current
+      for( unsigned i=0; i<constraints.size(); i++ ){
+        if( pol ){
+          c.push_back( constraints[i] );
+        }else{
+          c.push_back( constraints[i].negate() );
         }
-        constraints.clear();
-      }else{
-        //must add at higher level
       }
+      constraints.clear();
       return c.size()==1 ? c[0] : NodeManager::currentNM()->mkNode( pol ? AND : OR, c );
+    }else{
+      return nn;
     }
-  }else{
-    //simplify term
-    simplifyTerm( n, constraints );
   }
-  return n;
 }
 
 void FunDefFmf::simplifyTerm( Node n, std::vector< Node >& constraints ) {
diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h
index 40364eeb7..63aa1bf94 100644
--- a/src/theory/quantifiers/fun_def_process.h
+++ b/src/theory/quantifiers/fun_def_process.h
@@ -36,7 +36,7 @@ private:
   //defined functions to injections input -> argument elements
   std::map< Node, std::vector< Node > > d_input_arg_inj;
   //simplify
-  Node simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, bool is_fun_def = false );
+  Node simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, int is_fun_def = 0 );
   //simplify term
   void simplifyTerm( Node n, std::vector< Node >& constraints );
 public:
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 6de6e1d03..f97c4040b 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -357,13 +357,17 @@ bool CegqiOutputInstStrategy::isEligibleForInstantiation( Node n ) {
   return d_out->isEligibleForInstantiation( n );
 }
 
+bool CegqiOutputInstStrategy::addLemma( Node lem ) {
+  return d_out->addLemma( lem );
+}
+
 
 InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategy( qe ) {
   d_out = new CegqiOutputInstStrategy( this );
 }
 
 void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) {
-  
+  d_check_delta_lemma = true;
 }
 
 int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
@@ -374,6 +378,12 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
     std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( f );
     if( it==d_cinst.end() ){
       cinst = new CegInstantiator( d_quantEngine, d_out );
+      if( d_n_delta.isNull() ){
+        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 );
+      }
+      cinst->d_n_delta = d_n_delta;
       for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
         cinst->d_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) );
       }
@@ -381,24 +391,59 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
     }else{
       cinst = it->second;
     }
+    if( d_check_delta_lemma ){
+      Trace("inst-alg") << "-> Get delta lemmas for cegqi..." << std::endl; 
+      d_check_delta_lemma = false;
+      std::vector< Node > dlemmas;
+      cinst->getDeltaLemmas( dlemmas );
+      Trace("inst-alg") << "...got " << dlemmas.size() << " delta lemmas." << std::endl; 
+      if( !dlemmas.empty() ){
+        bool addedLemma = false;
+        for( unsigned i=0; i<dlemmas.size(); i++ ){
+          if( addLemma( dlemmas[i] ) ){
+            addedLemma = true;
+          }
+        }
+        if( addedLemma ){
+          return STATUS_UNKNOWN;
+        }
+      }
+    }
+    Trace("inst-alg") << "-> Run cegqi for " << f << std::endl;
     d_curr_quant = f;
     cinst->check();
     d_curr_quant = Node::null();
-    
-    return STATUS_UNKNOWN;
-  }else{
-    // To fix warning
-    Unreachable();
   }
+  return STATUS_UNKNOWN;
 }
 
 bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) {
   Assert( !d_curr_quant.isNull() );
+  /*
+  std::stringstream siss;
+  if( Trace.isOn("inst-cegqi") || Trace.isOn("inst-cegqi-debug") ){
+    for( unsigned j=0; j<d_single_inv_sk.size(); j++ ){
+      Node v = d_single_inv_map_to_prog[d_single_inv[0][j]];
+      siss << "    * " << v;
+      siss << " (" << d_single_inv_sk[j] << ")";
+      siss << " -> " << ( subs_typ[j]==9 ? "M:" : "") << subs[j] << std::endl;
+    }
+  }  
+  */
   return d_quantEngine->addInstantiation( d_curr_quant, subs, false );
 }
 
+bool InstStrategyCegqi::addLemma( Node lem ) {
+  return d_quantEngine->addLemma( lem );
+}
+
 bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
-  return true;
+  if( n.getKind()==INST_CONSTANT ){
+    //only legal if current quantified formula contains n
+    return TermDb::containsTerm( d_curr_quant, n );
+  }else{
+    return true;
+  }
 } 
 
 
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index e139d0b6f..9435fc97c 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -92,13 +92,16 @@ public:
   InstStrategyCegqi * d_out;
   bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
   bool isEligibleForInstantiation( Node n );
+  bool addLemma( Node lem );
 };
 
 class InstStrategyCegqi : public InstStrategy {
 private:
   CegqiOutputInstStrategy * d_out;
   std::map< Node, CegInstantiator * > d_cinst;
+  Node d_n_delta;
   Node d_curr_quant;
+  bool d_check_delta_lemma;
   /** process functions */
   void processResetInstantiationRound( Theory::Effort effort );
   int process( Node f, Theory::Effort effort, int e );
@@ -108,6 +111,7 @@ public:
   
   bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
   bool isEligibleForInstantiation( Node n );  
+  bool addLemma( Node lem );
   /** identify */
   std::string identify() const { return std::string("Cegqi"); }
 };
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 9c3035c85..cb01fd373 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -143,9 +143,9 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
           //check each instantiation strategy
           for( size_t i=0; i<d_instStrategies.size(); ++i ){
             InstStrategy* is = d_instStrategies[i];
-            Debug("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
+            Trace("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
             int quantStatus = is->process( f, effort, e_use );
-            Debug("inst-engine-debug") << " -> status is " << quantStatus << std::endl;
+            Trace("inst-engine-debug") << " -> status is " << quantStatus << std::endl;
             if( quantStatus==InstStrategy::STATUS_UNFINISHED ){
               finished = false;
             }
@@ -185,11 +185,14 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
                           << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl;
     for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
+      Debug("quantifiers") << "Process " << n << "..." << std::endl;
       //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
       if( !d_quantEngine->hasOwnership( n, this ) ){
         d_quant_active[n] = false;
+        Debug("quantifiers") << "  Quantifier has owner." << std::endl;
       }else if( !d_quantEngine->getModel()->isQuantifierActive( n ) ){
         d_quant_active[n] = false;
+        Debug("quantifiers") << "  Quantifier is not active (from model)." << std::endl;
       //it is not active if we have found the skolemized negation is unsat
       }else if( options::cbqi() && hasAddedCbqiLemma( n ) ){
         Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( n );
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 62790432d..a529e37d0 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -44,6 +44,10 @@ option clauseSplit --clause-split bool :default false
 #   forall x. P( x ) => f( S( x ) ) = x
 option preSkolemQuant --pre-skolem-quant bool :read-write :default false
  apply skolemization eagerly to bodies of quantified formulas
+option preSkolemQuantNested --pre-skolem-quant-nested bool :read-write :default true
+ apply skolemization to nested quantified formulass
+option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true
+ apply skolemization to quantified formulas aggressively
 # Whether to perform agressive miniscoping
 option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
  perform aggressive miniscoping for quantifiers
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index a78fa8d7b..991043157 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -285,7 +285,7 @@ Node QuantifiersRewriter::computeNNF( Node body ){
     }else{
       std::vector< Node > children;
       Kind k = body[0].getKind();
-      
+
       if( body[0].getKind()==OR || body[0].getKind()==AND ){
         k = body[0].getKind()==AND ? OR : AND;
         for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
@@ -1210,7 +1210,7 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
     return nn.negate();
   }else if( n.getKind()==kind::FORALL ){
     if( polarity ){
-      if( options::preSkolemQuant() ){
+      if( options::preSkolemQuant() && ( options::preSkolemQuantNested() || fvs.empty() ) ){
         vector< Node > children;
         children.push_back( n[0] );
         //add children to current scope
@@ -1245,20 +1245,22 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
     if( containsQuantifiers( n ) ){
       if( n.getType().isBoolean() ){
         if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){
-          Node nn;
-          //must remove structure
-          if( n.getKind()==kind::ITE ){
-            nn = NodeManager::currentNM()->mkNode( kind::AND,
-                   NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
-                   NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
-          }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
-            nn = NodeManager::currentNM()->mkNode( kind::AND,
-                   NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
-                   NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
-          }else if( n.getKind()==kind::IMPLIES ){
-            nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
+          if( options::preSkolemQuantAgg() ){
+            Node nn;
+            //must remove structure
+            if( n.getKind()==kind::ITE ){
+              nn = NodeManager::currentNM()->mkNode( kind::AND,
+                    NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
+                    NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
+            }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
+              nn = NodeManager::currentNM()->mkNode( kind::AND,
+                    NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
+                    NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
+            }else if( n.getKind()==kind::IMPLIES ){
+              nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
+            }
+            return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs );
           }
-          return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs );
         }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
           vector< Node > children;
           for( int i=0; i<(int)n.getNumChildren(); i++ ){
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 888cdbce0..ba75af873 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -417,7 +417,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){
     Trace("quant") << " : " << f << std::endl;
     ++(d_statistics.d_num_quant);
     Assert( f.getKind()==FORALL );
-    
+
     //check whether we should apply a reduction
     bool reduced = false;
     if( d_lte_part_inst && !f.getAttribute(LtePartialInstAttribute()) ){
@@ -567,7 +567,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
       Trace("inst") << std::endl;
       Assert( terms[i].getType().isSubtypeOf( f[0][i].getType() ) );
     }
-    if( options::cbqi() ){
+    if( options::cbqi() && !options::cbqi2() ){
       for( int i=0; i<(int)terms.size(); i++ ){
         if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){
           Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl;
@@ -589,7 +589,6 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
       }
       setInstantiationLevelAttr( body, f[1], maxInstLevel+1 );
     }
-    Trace("inst-debug") << "*** Lemma is " << lem << std::endl;
     ++(d_statistics.d_instantiations);
     return true;
   }else{
@@ -673,13 +672,17 @@ Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std
     Trace("partial-inst") << "Partial instantiation : " << f << std::endl;
     Trace("partial-inst") << "                      : " << body << std::endl;
   }else{
-    //do optimized version
-    Node icb = d_term_db->getInstConstantBody( f );
-    body = getSubstitute( icb, terms );
-    if( Debug.isOn("check-inst") ){
-      Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
-      if( body!=body2 ){
-        Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl;
+    if( options::cbqi() ){
+      body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+    }else{
+      //do optimized version
+      Node icb = d_term_db->getInstConstantBody( f );
+      body = getSubstitute( icb, terms );
+      if( Debug.isOn("check-inst") ){
+        Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+        if( body!=body2 ){
+          Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl;
+        }
       }
     }
   }
@@ -722,16 +725,16 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b
 
 bool QuantifiersEngine::addLemma( Node lem, bool doCache ){
   if( doCache ){
-    Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl;
     lem = Rewriter::rewrite(lem);
+    Trace("inst-add-debug2") << "Adding lemma : " << lem << std::endl;
     if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
       //d_curr_out->lemma( lem, false, true );
       d_lemmas_produced_c[ lem ] = true;
       d_lemmas_waiting.push_back( lem );
-      Debug("inst-engine-debug") << "Added lemma : " << lem << std::endl;
+      Trace("inst-add-debug2") << "Added lemma : " << lem << std::endl;
       return true;
     }else{
-      Debug("inst-engine-debug") << "Duplicate." << std::endl;
+      Trace("inst-add-debug2") << "Duplicate." << std::endl;
       return false;
     }
   }else{
@@ -943,7 +946,7 @@ void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
     out << "Internal error : module for synth solution not found." << std::endl;
   }
 }
-  
+
 QuantifiersEngine::Statistics::Statistics():
   d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
   d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),