From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 21 Aug 2015 08:07:12 +0000 (+0200)
Subject: Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi.  Enable... 
X-Git-Tag: cvc5-1.0.0~6252^2~12
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fb746fdd4e60e7d166b0fa1e5788bea925d22ee7;p=cvc5.git

Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi.  Enable redundant ITE branch elimination in quantifiers rewriter.
---

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 9d49f3d72..bf0168c64 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -74,10 +74,15 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
     Node pv = d_vars[i];
     TypeNode pvtn = pv.getType();
     Trace("cbqi-inst-debug") << "[Find instantiation for " << pv << "]" << std::endl;
+    Node pv_value;
+    if( options::cbqiModel() ){
+      pv_value = d_qe->getModel()->getValue( pv );
+      Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
+    }
 
     //if in effort=2, we must choose at least one model value
     if( (i+1)<d_vars.size() || effort!=2 ){
-      
+
       //[1] easy case : pv is in the equivalence class as another term not containing pv
       Trace("cbqi-inst-debug") << "[1] try based on equivalence class." << std::endl;
       std::map< Node, Node >::iterator itr = d_curr_rep.find( pv );
@@ -169,38 +174,37 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                     }
                     Node eq = eq_lhs.eqNode( eq_rhs );
                     eq = Rewriter::rewrite( eq );
-                    //cannot contain infinity
-                    if( !d_qe->getTermDatabase()->containsVtsInfinity( eq ) ){
-                      Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl;
-                      std::map< Node, Node > msum;
-                      if( QuantArith::getMonomialSumLit( eq, msum ) ){
-                        if( Trace.isOn("cbqi-inst-debug") ){
-                          Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl;
-                          QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" );
-                          Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl;
-                        }
-                        Node veq;
-                        if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){
-                          Trace("cbqi-inst-debug") << "...isolated equality " << veq << "." << std::endl;
-                          Node veq_c;
-                          if( veq[0]!=pv ){
-                            Node veq_v;
-                            if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){
-                              Assert( veq_v==pv );
-                            }
-                          }
-                          Node val = veq[1];
-                          //eliminate coefficient if real
-                          if( !pvtn.isInteger() && !veq_c.isNull() ){
-                            val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) );
-                            val = Rewriter::rewrite( val );
-                            veq_c = Node::null();
+                    //cannot contain infinity?
+                    //if( !d_qe->getTermDatabase()->containsVtsInfinity( eq ) ){
+                    Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl;
+                    std::map< Node, Node > msum;
+                    if( QuantArith::getMonomialSumLit( eq, msum ) ){
+                      if( Trace.isOn("cbqi-inst-debug") ){
+                        Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl;
+                        QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" );
+                        Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl;
+                      }
+                      Node veq;
+                      if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){
+                        Trace("cbqi-inst-debug") << "...isolated equality " << veq << "." << std::endl;
+                        Node veq_c;
+                        if( veq[0]!=pv ){
+                          Node veq_v;
+                          if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){
+                            Assert( veq_v==pv );
                           }
-                          if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
-                            subs_proc[val][veq_c] = true;
-                            if( addInstantiationInc( val, pv, veq_c, subs, vars, coeff, has_coeff, theta, i, effort ) ){
-                              return true;
-                            }
+                        }
+                        Node val = veq[1];
+                        //eliminate coefficient if real
+                        if( !pvtn.isInteger() && !veq_c.isNull() ){
+                          val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) );
+                          val = Rewriter::rewrite( val );
+                          veq_c = Node::null();
+                        }
+                        if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
+                          subs_proc[val][veq_c] = true;
+                          if( addInstantiationInc( val, pv, veq_c, subs, vars, coeff, has_coeff, theta, i, effort ) ){
+                            return true;
                           }
                         }
                       }
@@ -264,97 +268,111 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
                 //if it contains pv, not infinity
                 if( !atom_lhs.isNull() && d_prog_var[atom_lhs].find( pv )!=d_prog_var[atom_lhs].end() ){
                   Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs );
-                  //cannot contain infinity
-                  if( !d_qe->getTermDatabase()->containsVtsInfinity( atom_lhs ) ){
-                    Trace("cbqi-inst-debug") << "..[3] From assertion : " << atom << ", pol = " << pol << std::endl;
-                    Trace("cbqi-inst-debug") << "         substituted : " << satom << ", pol = " << pol << std::endl;
-                    std::map< Node, Node > msum;
-                    if( QuantArith::getMonomialSumLit( satom, msum ) ){
-                      if( Trace.isOn("cbqi-inst-debug") ){
-                        Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl;
-                        QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" );
-                        Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl;
-                      }
-                      Node vatom;
-                      //isolate pv in the inequality
-                      int ires = QuantArith::isolate( pv, msum, vatom, atom.getKind(), true );
-                      if( ires!=0 ){
-                        Trace("cbqi-inst-debug") << "...isolated atom " << vatom << "." << std::endl;
-                        Node val = vatom[ ires==1 ? 1 : 0 ];
-                        Node pvm = vatom[ ires==1 ? 0 : 1 ];
-                        //get monomial
-                        Node veq_c;
-                        if( pvm!=pv ){
-                          Node veq_v;
-                          if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){
-                            Assert( veq_v==pv );
-                          }
-                        }
-                        //eliminate coefficient if real
-                        if( !pvtn.isInteger() && !veq_c.isNull() ){
-                          val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) );
-                          val = Rewriter::rewrite( val );
-                          veq_c = Node::null();
+                  //cannot contain infinity?
+                  //if( !d_qe->getTermDatabase()->containsVtsInfinity( atom_lhs ) ){
+                  Trace("cbqi-inst-debug") << "..[3] From assertion : " << atom << ", pol = " << pol << std::endl;
+                  Trace("cbqi-inst-debug") << "         substituted : " << satom << ", pol = " << pol << std::endl;
+                  std::map< Node, Node > msum;
+                  if( QuantArith::getMonomialSumLit( satom, msum ) ){
+                    if( Trace.isOn("cbqi-inst-debug") ){
+                      Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl;
+                      QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" );
+                      Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl;
+                    }
+                    Node vatom;
+                    //isolate pv in the inequality
+                    int ires = QuantArith::isolate( pv, msum, vatom, atom.getKind(), true );
+                    if( ires!=0 ){
+                      Trace("cbqi-inst-debug") << "...isolated atom " << vatom << "." << std::endl;
+                      Node val = vatom[ ires==1 ? 1 : 0 ];
+                      Node pvm = vatom[ ires==1 ? 0 : 1 ];
+                      //get monomial
+                      Node veq_c;
+                      if( pvm!=pv ){
+                        Node veq_v;
+                        if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){
+                          Assert( veq_v==pv );
                         }
+                      }
+                      //eliminate coefficient if real
+                      if( !pvtn.isInteger() && !veq_c.isNull() ){
+                        val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) );
+                        val = Rewriter::rewrite( val );
+                        veq_c = Node::null();
+                      }
 
-                        //disequalities are both strict upper and lower bounds
-                        unsigned rmax = atom.getKind()==GEQ ? 1 : 2;
-                        for( unsigned r=0; r<rmax; r++ ){
-                          int uires = ires;
-                          Node uval = val;
-                          if( atom.getKind()==GEQ ){
-                            //push negation downwards
-                            if( !pol ){
-                              uires = -ires;
-                              if( pvtn.isInteger() ){
-                                uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
-                                uval = Rewriter::rewrite( uval );
-                              }else{
-                                Assert( pvtn.isReal() );
-                                //now is strict inequality
-                                uires = uires*2;
-                              }
-                            }
-                          }else{
-                            Assert( atom.getKind()==EQUAL && !pol );
+                      //disequalities are either strict upper or lower bounds
+                      unsigned rmax = ( atom.getKind()==GEQ && options::cbqiModel() ) ? 1 : 2;
+                      for( unsigned r=0; r<rmax; r++ ){
+                        int uires = ires;
+                        Node uval = val;
+                        if( atom.getKind()==GEQ ){
+                          //push negation downwards
+                          if( !pol ){
+                            uires = -ires;
                             if( pvtn.isInteger() ){
-                              uires = r==0 ? -1 : 1;
                               uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
                               uval = Rewriter::rewrite( uval );
                             }else{
                               Assert( pvtn.isReal() );
-                              uires = r==0 ? -2 : 2;
+                              //now is strict inequality
+                              uires = uires*2;
                             }
                           }
-                          Trace("cbqi-bound-inf") << "From " << lit << ", got : ";
-                          if( !veq_c.isNull() ){
-                            Trace("cbqi-bound-inf") << veq_c << " * ";
-                          }
-                          Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl;
+                        }else{
+                          unsigned use_r = r;
                           if( options::cbqiModel() ){
-                            //just store bounds, will choose based on tighest bound
-                            unsigned index = uires>0 ? 0 : 1;
-                            mbp_bounds[index].push_back( uval );
-                            mbp_coeff[index].push_back( veq_c );
-                            mbp_strict[index].push_back( uires==2 || uires==-2 );
-                            mbp_lit[index].push_back( lit );
+                            // disequality is a disjunction : only consider the bound in the direction of the model
+                            Node rhs_value = d_qe->getModel()->getValue( val );
+                            Node lhs_value = pv_value;
+                            if( !veq_c.isNull() ){
+                              lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c );
+                              lhs_value = Rewriter::rewrite( lhs_value );
+                            }
+                            Assert( lhs_value!=rhs_value );
+                            Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value );
+                            cmp = Rewriter::rewrite( cmp );
+                            Assert( cmp.isConst() );
+                            use_r = cmp==d_true ? 1 : 0;
+                          }
+                          Assert( atom.getKind()==EQUAL && !pol );
+                          if( pvtn.isInteger() ){
+                            uires = use_r==0 ? -1 : 1;
+                            uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
+                            uval = Rewriter::rewrite( uval );
                           }else{
-                            //take into account delta
-                            if( uires==2 || uires==-2 ){
-                              if( d_use_vts_delta ){
-                                Node delta = d_qe->getTermDatabase()->getVtsDelta();
-                                uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta );
-                                uval = Rewriter::rewrite( uval );
-                              }
+                            Assert( pvtn.isReal() );
+                            uires = use_r==0 ? -2 : 2;
+                          }
+                        }
+                        Trace("cbqi-bound-inf") << "From " << lit << ", got : ";
+                        if( !veq_c.isNull() ){
+                          Trace("cbqi-bound-inf") << veq_c << " * ";
+                        }
+                        Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl;
+                        if( options::cbqiModel() ){
+                          //just store bounds, will choose based on tighest bound
+                          unsigned index = uires>0 ? 0 : 1;
+                          mbp_bounds[index].push_back( uval );
+                          mbp_coeff[index].push_back( veq_c );
+                          mbp_strict[index].push_back( uires==2 || uires==-2 );
+                          mbp_lit[index].push_back( lit );
+                        }else{
+                          //take into account delta
+                          if( uires==2 || uires==-2 ){
+                            if( d_use_vts_delta ){
+                              Node delta = d_qe->getTermDatabase()->getVtsDelta();
+                              uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta );
+                              uval = Rewriter::rewrite( uval );
                             }
-                            if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
-                              subs_proc[uval][veq_c] = true;
-                              if( addInstantiationInc( uval, pv, veq_c, subs, vars, coeff, has_coeff, theta, i, effort ) ){
-                                return true;
-                              }
-                            }else{
-                              Trace("cbqi-inst-debug") << "...already processed." << std::endl;
+                          }
+                          if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
+                            subs_proc[uval][veq_c] = true;
+                            if( addInstantiationInc( uval, pv, veq_c, subs, vars, coeff, has_coeff, theta, i, effort ) ){
+                              return true;
                             }
+                          }else{
+                            Trace("cbqi-inst-debug") << "...already processed." << std::endl;
                           }
                         }
                       }
@@ -371,13 +389,11 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
           bool upper_first = false;
           unsigned best_used[2];
           std::vector< Node > t_values[2];
-          Node pv_value = d_qe->getModel()->getValue( pv );
-          Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
           //try optimal bounds
           for( unsigned r=0; r<2; r++ ){
             int rr = upper_first ? (1-r) : r;
             if( mbp_bounds[rr].empty() ){
-              if( d_use_vts_inf ){
+              if( d_use_vts_inf && ( pvtn.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() ) ){
                 Trace("cbqi-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << pvtn << ")" << std::endl;
                 //no bounds, we do +- infinity
                 Node val = d_qe->getTermDatabase()->getVtsInfinity( pvtn );
@@ -459,7 +475,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
       int new_effort = pvtn.isBoolean() ? effort : 1;
 #ifdef MBP_STRICT_ASSERTIONS
       //we only resort to values in the case of booleans
-      Assert( !options::cbqiUseInf() || pvtn.isBoolean() );
+      Assert( !options::cbqiUseInfInt() || !options::cbqiUseInfReal() || pvtn.isBoolean() );
 #endif
       if( addInstantiationInc( mv, pv, pv_coeff_m, subs, vars, coeff, has_coeff, theta, i, new_effort ) ){
         return true;
@@ -474,10 +490,10 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
 bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, std::vector< Node >& subs, std::vector< Node >& vars,
                                            std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort ) {
   if( Trace.isOn("cbqi-inst") ){
-    for( unsigned i=0; i<subs.size(); i++ ){
+    for( unsigned j=0; j<subs.size(); j++ ){
       Trace("cbqi-inst") << " ";
     }
-    Trace("cbqi-inst") << "i: ";
+    Trace("cbqi-inst") << subs.size() << ": ";
     if( !pv_coeff.isNull() ){
       Trace("cbqi-inst") << pv_coeff << " * ";
     }
@@ -540,11 +556,6 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, std::
     if( !pv_coeff.isNull() ){
       has_coeff.push_back( pv );
     }
-    Trace("cbqi-inst-debug") << i << ": ";
-    if( !pv_coeff.isNull() ){
-      Trace("cbqi-inst-debug") << pv_coeff << "*";
-    }
-    Trace("cbqi-inst-debug") << pv << " -> " << n << std::endl;
     Node new_theta = theta;
     if( !pv_coeff.isNull() ){
       if( new_theta.isNull() ){
@@ -829,13 +840,13 @@ void CegInstantiator::processAssertions() {
   d_curr_eqc.clear();
   d_curr_rep.clear();
   d_curr_arith_eqc.clear();
-  
+
   eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
   //to eliminate identified illegal terms
   std::map< Node, Node > aux_uf;
   std::map< Node, Node > aux_subs;
   std::map< Node, bool > aux_subs_inelig;
-  
+
   //for each variable
   bool has_arith_var = false;
   for( unsigned i=0; i<d_vars.size(); i++ ){
@@ -856,6 +867,16 @@ void CegInstantiator::processAssertions() {
             Node lit = (*it).assertion;
             d_curr_asserts[tid].push_back( lit );
             Trace("cbqi-proc-debug") << "...add : " << lit << std::endl;
+            if( lit.getKind()==EQUAL ){
+              std::map< Node, std::map< Node, Node > >::iterator itae = d_aux_eq.find( lit );
+              if( itae!=d_aux_eq.end() ){
+                for( std::map< Node, Node >::iterator itae2 = itae->second.begin(); itae2 != itae->second.end(); ++itae2 ){
+                  aux_subs[ itae2->first ] = itae2->second;
+                  Trace("cbqi-proc") << "......add substitution : " << itae2->first << " -> " << itae2->second << std::endl;
+                }
+              }
+            } 
+            /*
             if( lit.getKind()==EQUAL ){
               //check if it is an auxiliary variable (for instance, from ITE removal).  If so, solve for it.
               for( unsigned k=0; k<2; k++ ){
@@ -881,6 +902,7 @@ void CegInstantiator::processAssertions() {
                 }
               }
             }
+            */
           }
         }
       }
@@ -910,7 +932,7 @@ void CegInstantiator::processAssertions() {
     while( !eqcs_i.isFinished() ){
       Node r = *eqcs_i;
       TypeNode rtn = r.getType();
-      if( rtn.isInteger() || rtn.isReal() ){  
+      if( rtn.isInteger() || rtn.isReal() ){
         Trace("cbqi-proc-debug") << "...arith eqc: " << r << std::endl;
         d_curr_arith_eqc.push_back( r );
         if( d_curr_eqc.find( r )==d_curr_eqc.end() ){
@@ -935,21 +957,21 @@ void CegInstantiator::processAssertions() {
     if( it!=aux_subs.end() ){
       addToAuxVarSubstitution( subs_lhs, subs_rhs, l, it->second );
     }else{
+      Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << l << "!!!" << std::endl;
 #ifdef MBP_STRICT_ASSERTIONS
       Assert( false );
 #endif
-      Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << l << "!!!" << std::endl;
     }
-  }  
+  }
+
 
-  
   //apply substitutions to everything, if necessary
   if( !subs_lhs.empty() ){
     Trace("cbqi-proc") << "Applying substitution : " << std::endl;
     for( unsigned i=0; i<subs_lhs.size(); i++ ){
       Trace("cbqi-proc") << "  " << subs_lhs[i] << " -> " << subs_rhs[i] << std::endl;
     }
-    
+
     for( std::map< TheoryId, std::vector< Node > >::iterator it = d_curr_asserts.begin(); it != d_curr_asserts.end(); ++it ){
       for( unsigned i=0; i<it->second.size(); i++ ){
         Node lit = it->second[i];
@@ -979,6 +1001,7 @@ void CegInstantiator::processAssertions() {
       if( d_inelig.find( n )==d_inelig.end() ){
         //must contain at least one variable
         if( !d_prog_var[n].empty() ){
+          Trace("cbqi-proc") << "...literal[" << it->first << "] : " << n << std::endl;
           akeep.push_back( n );
         }else{
           Trace("cbqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains no relevant variables." << std::endl;
@@ -990,7 +1013,7 @@ void CegInstantiator::processAssertions() {
     it->second.clear();
     it->second.insert( it->second.end(), akeep.begin(), akeep.end() );
   }
-  
+
   //remove duplicate terms from eqc
   for( std::map< Node, std::vector< Node > >::iterator it = d_curr_eqc.begin(); it != d_curr_eqc.end(); ++it ){
     std::vector< Node > new_eqc;
@@ -1006,7 +1029,7 @@ void CegInstantiator::processAssertions() {
 
 void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ) {
   r = r.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
-  
+
   std::vector< Node > cl;
   cl.push_back( l );
   std::vector< Node > cr;
@@ -1016,7 +1039,7 @@ void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, st
     nr = Rewriter::rewrite( nr );
     subs_rhs[i] = nr;
   }
-  
+
   subs_lhs.push_back( l );
   subs_rhs.push_back( r );
 }
@@ -1369,21 +1392,7 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
   if( e<1 ){
     return STATUS_UNFINISHED;
   }else if( e==1 ){
-    CegInstantiator * cinst;
-    std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( f );
-    if( it==d_cinst.end() ){
-      cinst = new CegInstantiator( d_quantEngine, d_out, true, options::cbqiUseInf() );
-      for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
-        cinst->d_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) );
-      }
-      std::map< Node, std::vector< Node > >::iterator itav = d_aux_variables.find( f );
-      if( itav!=d_aux_variables.end() ){
-        cinst->d_aux_vars.insert( cinst->d_aux_vars.begin(), itav->second.begin(), itav->second.end() );
-      }
-      d_cinst[f] = cinst;
-    }else{
-      cinst = it->second;
-    }
+    CegInstantiator * cinst = getInstantiator( f );
     Trace("inst-alg") << "-> Run cegqi for " << f << std::endl;
     d_curr_quant = f;
     bool addedLemma = cinst->check();
@@ -1434,14 +1443,17 @@ bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
   }
 }
 
-void InstStrategyCegqi::setAuxiliaryVariables( Node q, std::vector< Node >& vars ) {
+CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
   std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( q );
-  if( it!=d_cinst.end() ){
-    Assert( it->second->d_aux_vars.empty() );
-    it->second->d_aux_vars.insert( it->second->d_aux_vars.end(), vars.begin(), vars.end() );
+  if( it==d_cinst.end() ){
+    CegInstantiator * cinst = new CegInstantiator( d_quantEngine, d_out, true, true );
+    for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( q ); i++ ){
+      cinst->d_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ) );
+    }
+    d_cinst[q] = cinst;
+    return cinst;
   }else{
-    Assert( d_aux_variables.find( q )==d_aux_variables.end() );
-    d_aux_variables[q].insert( d_aux_variables[q].end(), vars.begin(), vars.end() );
+   return it->second;
   }
 }
 
@@ -1453,5 +1465,3 @@ void InstStrategyCegqi::setAuxiliaryVariables( Node q, std::vector< Node >& vars
 
 
 
-
-
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 64303e1f3..f7cb290b2 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -88,6 +88,8 @@ public:
   std::vector< Node > d_vars;
   //auxiliary variables
   std::vector< Node > d_aux_vars;
+  //literals to equalities for aux vars
+  std::map< Node, std::map< Node, Node > > d_aux_eq;
   //check : add instantiations based on valuation of d_vars
   bool check();
 };
@@ -153,7 +155,6 @@ class InstStrategyCegqi : public InstStrategy {
 private:
   CegqiOutputInstStrategy * d_out;
   std::map< Node, CegInstantiator * > d_cinst;
-  std::map< Node, std::vector< Node > > d_aux_variables;
   Node d_small_const;
   Node d_curr_quant;
   bool d_check_vts_lemma_lc;
@@ -170,8 +171,8 @@ public:
   /** identify */
   std::string identify() const { return std::string("Cegqi"); }
   
-  //set auxiliary variables
-  void setAuxiliaryVariables( Node q, std::vector< Node >& vars );
+  //get instantiator for quantifier
+  CegInstantiator * getInstantiator( Node q );
 };
 
 }
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index b12c822ef..3dad74044 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -108,18 +108,37 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
           std::vector< Node > lems;
           lems.push_back( lem );
           d_quantEngine->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap);
-          std::vector< Node > aux_vars;
-          for( unsigned i=0; i<lems.size(); i++ ){
-            Trace("cbqi-debug") << "Counterexample lemma (processed) " << i << " : " << lems[i] << std::endl;
-            d_quantEngine->addLemma( lems[i], false );
-          }
-          for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) {
-            Trace("cbqi-debug") << "  Auxiliary var (from ITE) : " << i->first << std::endl;
-            aux_vars.push_back( i->first );
-          }
-          //record the auxiliary variables in the inst strategy
+          CegInstantiator * cinst = NULL;
           if( d_i_cegqi ){
-            d_i_cegqi->setAuxiliaryVariables( f, aux_vars );
+            cinst = d_i_cegqi->getInstantiator( f );
+            Assert( cinst->d_aux_vars.empty() );
+            for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) {
+              Trace("cbqi-debug") << "  Auxiliary var (from ITE) : " << i->first << std::endl;
+              cinst->d_aux_vars.push_back( i->first );
+            }
+          }
+          for( unsigned i=0; i<lems.size(); i++ ){
+            Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite)  " << i << " : " << lems[i] << std::endl;
+            if( !cinst ){
+              d_quantEngine->addLemma( lems[i], false );
+            }else{
+              Node rlem = lems[i];
+              rlem = Rewriter::rewrite( rlem );
+              Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl;
+              d_quantEngine->addLemma( rlem, false );
+              //record the literals that imply auxiliary variables to be equal to terms
+              if( lems[i].getKind()==ITE && rlem.getKind()==ITE ){
+                if( lems[i][1].getKind()==EQUAL && lems[i][2].getKind()==EQUAL && lems[i][1][0]==lems[i][2][0] ){
+                  if( std::find( cinst->d_aux_vars.begin(), cinst->d_aux_vars.end(), lems[i][1][0] )!=cinst->d_aux_vars.end() ){
+                    Node v = lems[i][1][0];
+                    for( unsigned r=1; r<=2; r++ ){
+                      cinst->d_aux_eq[rlem[r]][v] = lems[i][r][1];
+                      Trace("cbqi-debug") << "  " << rlem[r] << " implies " << v << " = " << lems[i][r][1] << std::endl;
+                    }
+                  }
+                }
+              }
+            }
           }
           
           addedLemma = true;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index b573ebd67..66de51f39 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -17,7 +17,8 @@ option miniscopeQuant --miniscope-quant bool :default true :read-write
 # ( forall x. P( x ) ) V Q
 option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write
  disable miniscope quantifiers for ground subformulas
-# Whether to prenex (nested universal) quantifiers
+option clauseSplit --clause-split bool :default true
+ apply clause splitting to quantified formulas
 option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToPrenexQuantMode :handler-include "theory/quantifiers/options_handlers.h"
  prenex mode for quantified formulas
 # Whether to variable-eliminate quantifiers.
@@ -37,11 +38,8 @@ option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default fal
 # Whether to CNF quantifier bodies
 # option cnfQuant --cnf-quant bool :default false
 #  apply CNF conversion to quantified formulas
-# Whether to NNF quantifier bodies
 option nnfQuant --nnf-quant bool :default true
  apply NNF conversion to quantified formulas
-option clauseSplit --clause-split bool :default true
- apply clause splitting to quantified formulas
 # Whether to pre-skolemize quantifier bodies.
 # For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
 #   forall x. P( x ) => f( S( x ) ) = x
@@ -51,10 +49,8 @@ option preSkolemQuantNested --pre-skolem-quant-nested bool :read-write :default
  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
-# Whether to CNF quantifier bodies
 option elimTautQuant --elim-taut-quant bool :default true
  eliminate tautological disjuncts of quantified formulas
  
@@ -246,8 +242,11 @@ option cbqiSat --cbqi-sat bool :read-write :default true
  answer sat when quantifiers are asserted with counterexample-based quantifier instantiation
 option cbqiModel --cbqi-model bool :read-write :default true
  guide instantiations by model values for counterexample-based quantifier instantiation
-option cbqiUseInf --cbqi-use-inf bool :read-write :default false
- use infinity for vts in counterexample-based quantifier instantiation
+option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false
+ use integer infinity for vts in counterexample-based quantifier instantiation
+option cbqiUseInfReal --cbqi-use-inf-real bool :read-write :default false
+ use real infinity for vts in counterexample-based quantifier instantiation
+ 
  
 ### local theory extensions options 
 
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 2c65b62b3..938245871 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -313,15 +313,20 @@ void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int
 }
 
 void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) {
-  newHasPol = hasPol;
-  newPol = pol;
-  if( n.getKind()==NOT || ( n.getKind()==IMPLIES && child==0 ) ){
+  if( n.getKind()==AND || n.getKind()==OR ){
+    newHasPol = hasPol;
+    newPol = pol;
+  }else if( n.getKind()==IMPLIES ){
+    newHasPol = hasPol;
+    newPol = child==0 ? !pol : pol;
+  }else if( n.getKind()==NOT ){
+    newHasPol = hasPol;
     newPol = !pol;
-  }else if( n.getKind()==IFF || n.getKind()==XOR ){
-    newHasPol = false;
   }else if( n.getKind()==ITE ){
-    if( child==0 ){
-      newHasPol = false;
-    }
+    newHasPol = (child!=0) && hasPol;
+    newPol = pol;
+  }else{
+    newHasPol = false;
+    newPol = pol;
   }
 }
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index d6cbe386c..c32aeeb78 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -415,89 +415,105 @@ void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node
   }
 }
 
-Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol ) {
-  if( body.getType().isBoolean() ){
-    if( body.getKind()==EQUAL && options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE ){
-      for( size_t i=0; i<2; i++ ){
-        if( body[i].getKind()==ITE ){
-          Node no = i==0 ? body[1] : body[0];
-          if( no.getKind()!=ITE ){
-            bool doRewrite = options::iteLiftQuant()==ITE_LIFT_QUANT_MODE_ALL;
-            std::vector< Node > children;
-            children.push_back( body[i][0] );
-            for( size_t j=1; j<=2; j++ ){
-              //check if it rewrites to a constant
-              Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] );
-              nn = Rewriter::rewrite( nn );
-              children.push_back( nn );
-              if( nn.isConst() ){
-                doRewrite = true;
-              }
-            }
-            if( doRewrite ){
-              return NodeManager::currentNM()->mkNode( ITE, children );
+Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond ) {
+  if( body.getKind()==EQUAL && options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE ){
+    for( size_t i=0; i<2; i++ ){
+      if( body[i].getKind()==ITE ){
+        Node no = i==0 ? body[1] : body[0];
+        if( no.getKind()!=ITE ){
+          bool doRewrite = options::iteLiftQuant()==ITE_LIFT_QUANT_MODE_ALL;
+          std::vector< Node > children;
+          children.push_back( body[i][0] );
+          for( size_t j=1; j<=2; j++ ){
+            //check if it rewrites to a constant
+            Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] );
+            nn = Rewriter::rewrite( nn );
+            children.push_back( nn );
+            if( nn.isConst() ){
+              doRewrite = true;
             }
           }
+          if( doRewrite ){
+            return NodeManager::currentNM()->mkNode( ITE, children );
+          }
         }
       }
-    }else if( body.getKind()==ITE && hasPol ){
-      if( options::iteCondVarSplitQuant() ){
-        Trace("quantifiers-rewrite-ite-debug") << "Conditional var eq split " << body << std::endl;
-        for( unsigned r=0; r<2; r++ ){
-          //check if there is a variable elimination
-          Node b = r==0 ? body[0] : body[0].negate();
-          QuantPhaseReq qpr( b );
-          std::vector< Node > vars;
-          std::vector< Node > subs;
-          Trace("quantifiers-rewrite-ite-debug") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl;
-          for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
-            Trace("quantifiers-rewrite-ite-debug") << "phase req " << it->first << " -> " << it->second << std::endl;
-            if( it->second ){
-              if( it->first.getKind()==EQUAL ){
-                for( unsigned i=0; i<2; i++ ){
-                  if( it->first[i].getKind()==BOUND_VARIABLE ){
-                    unsigned j = i==0 ? 1 : 0;
-                    if( !hasArg1( it->first[i], it->first[j] ) ){
-                      vars.push_back( it->first[i] );
-                      subs.push_back( it->first[j] );
-                      break;
-                    }
+    }
+  }else if( body.getKind()==ITE ){
+    if( body.getType().isBoolean() && hasPol && options::iteCondVarSplitQuant() ){
+      Trace("quantifiers-rewrite-ite-debug") << "Conditional var eq split " << body << std::endl;
+      for( unsigned r=0; r<2; r++ ){
+        //check if there is a variable elimination
+        Node b = r==0 ? body[0] : body[0].negate();
+        QuantPhaseReq qpr( b );
+        std::vector< Node > vars;
+        std::vector< Node > subs;
+        Trace("quantifiers-rewrite-ite-debug") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl;
+        for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
+          Trace("quantifiers-rewrite-ite-debug") << "phase req " << it->first << " -> " << it->second << std::endl;
+          if( it->second ){
+            if( it->first.getKind()==EQUAL ){
+              for( unsigned i=0; i<2; i++ ){
+                if( it->first[i].getKind()==BOUND_VARIABLE ){
+                  unsigned j = i==0 ? 1 : 0;
+                  if( !hasArg1( it->first[i], it->first[j] ) ){
+                    vars.push_back( it->first[i] );
+                    subs.push_back( it->first[j] );
+                    break;
                   }
                 }
               }
             }
           }
-          if( !vars.empty() ){
-            //bool cpol = (r==1);
-            Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] );
-            //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-            //pos = Rewriter::rewrite( pos );
-            Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] );
-            Trace("quantifiers-rewrite-ite") << "*** Split ITE (conditional variable eq) " << body << " into : " << std::endl;
-            Trace("quantifiers-rewrite-ite") << "   " << pos << std::endl;
-            Trace("quantifiers-rewrite-ite") << "   " << neg << std::endl;
-            return NodeManager::currentNM()->mkNode( AND, pos, neg );
-          }
+        }
+        if( !vars.empty() ){
+          //bool cpol = (r==1);
+          Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] );
+          //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+          //pos = Rewriter::rewrite( pos );
+          Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] );
+          Trace("quantifiers-rewrite-ite") << "*** Split ITE (conditional variable eq) " << body << " into : " << std::endl;
+          Trace("quantifiers-rewrite-ite") << "   " << pos << std::endl;
+          Trace("quantifiers-rewrite-ite") << "   " << neg << std::endl;
+          return NodeManager::currentNM()->mkNode( AND, pos, neg );
         }
       }
     }
-    if( body.getKind()!=EQUAL && body.getKind()!=APPLY_UF ){
-      bool changed = false;
-      std::vector< Node > children;
-      for( size_t i=0; i<body.getNumChildren(); i++ ){
-        bool newHasPol;
-        bool newPol;
-        QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
-        Node nn = computeProcessIte( body[i], newHasPol, newPol );
-        children.push_back( nn );
-        changed = changed || nn!=body[i];
-      }
-      if( changed ){
-        return NodeManager::currentNM()->mkNode( body.getKind(), children );
+  }
+  bool changed = false;
+  std::vector< Node > children;
+  for( size_t i=0; i<body.getNumChildren(); i++ ){
+    bool newHasPol;
+    bool newPol;
+    QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
+    if( body.getKind()==ITE && i>0 ){
+      currCond[children[0]] = (i==1);
+    }
+    Node nn = computeProcessIte( body[i], newHasPol, newPol, currCond );
+    if( body.getKind()==ITE && i==0 ){
+      std::map< Node, bool >::iterator itc = currCond.find( nn );
+      if( itc!=currCond.end() ){
+        if( itc->second ){
+          return computeProcessIte( body[1], hasPol, pol, currCond );
+        }else{
+          return computeProcessIte( body[2], hasPol, pol, currCond );
+        }
       }
     }
+    children.push_back( nn );
+    changed = changed || nn!=body[i];
+  }
+  if( body.getKind()==ITE ){
+    currCond.erase( children[0] );
+  }
+  if( changed ){
+    if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
+      children.insert( children.begin(), body.getOperator() );
+    }
+    return NodeManager::currentNM()->mkNode( body.getKind(), children );
+  }else{
+    return body;
   }
-  return body;
 }
 
 Node QuantifiersRewriter::computeProcessIte2( Node body ){
@@ -1140,7 +1156,9 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
   }else if( computeOption==COMPUTE_NNF ){
     return options::nnfQuant();
   }else if( computeOption==COMPUTE_PROCESS_ITE ){
-    return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant();
+    //always eliminate redundant conditions in ITE
+    return true;
+    //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant();
   }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){
     return options::iteDtTesterSplitQuant();
   }else if( computeOption==COMPUTE_PRENEX ){
@@ -1182,7 +1200,8 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp
     }else if( computeOption==COMPUTE_NNF ){
       n = computeNNF( n );
     }else if( computeOption==COMPUTE_PROCESS_ITE ){
-      n = computeProcessIte( n, true, true );
+      std::map< Node, bool > curr_cond;
+      n = computeProcessIte( n, true, true, curr_cond );
     }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){
       n = computeProcessIte2( n );
     }else if( computeOption==COMPUTE_PRENEX ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index d01677171..7db80c84b 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -46,7 +46,7 @@ private:
   static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl );
   static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
   static Node computeNNF( Node body );
-  static Node computeProcessIte( Node body, bool hasPol, bool pol );
+  static Node computeProcessIte( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond );
   static Node computeProcessIte2( Node body );
   static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl );
   static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 13c408d85..d1a268950 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -329,6 +329,10 @@ void QuantifiersEngine::check( Theory::Effort e ){
       Trace("quant-engine-ee") << "Equality engine : " << std::endl;
       debugPrintEqualityEngine( "quant-engine-ee" );
     }
+    if( Trace.isOn("quant-engine-assert") ){
+      Trace("quant-engine-assert") << "Assertions : " << std::endl;
+      getTheoryEngine()->printAssertions("quant-engine-assert");
+    }
 
     //reset relevant information
     d_conflict = false;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 96a99763d..b28a73b9d 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -798,9 +798,6 @@ private:
   /** Visitor for collecting shared terms */
   SharedTermsVisitor d_sharedTermsVisitor;
 
-  /** Prints the assertions to the debug stream */
-  void printAssertions(const char* tag);
-
   /** Dump the assertions to the dump */
   void dumpAssertions(const char* tag);
 
@@ -834,6 +831,10 @@ public:
   RemoveITE* getIteRemover() { return &d_iteRemover; }
 
   SortInference* getSortInference() { return &d_sortInfer; }
+  
+  /** Prints the assertions to the debug stream */
+  void printAssertions(const char* tag);
+
 private:
   std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;
 public:
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index c15074d8c..d913cb76a 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1047,6 +1047,7 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
     //add splitting lemma for cardinality constraint
     Assert( !d_cardinality_term.isNull() );
     Node lem = getCardinalityLiteral( d_aloc_cardinality );
+    Trace("uf-ss-lemma") << "*** Cardinality split on : " << lem << std::endl;
     lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() );
     d_cardinality_lemma[ d_aloc_cardinality ] = lem;
     //add as lemma to output channel
diff --git a/test/regress/regress0/quantifiers/006-cbqi-ite.smt2 b/test/regress/regress0/quantifiers/006-cbqi-ite.smt2
new file mode 100644
index 000000000..bfa3ef22b
--- /dev/null
+++ b/test/regress/regress0/quantifiers/006-cbqi-ite.smt2
@@ -0,0 +1,299 @@
+(set-logic LIA)
+(set-info :status unsat)
+(declare-fun W_S2_V6 () Bool)
+(declare-fun W_S2_V4 () Bool)
+(declare-fun W_S2_V2 () Bool)
+(declare-fun W_S2_V3 () Bool)
+(declare-fun W_S2_V1 () Bool)
+(declare-fun W_S1_V6 () Bool)
+(declare-fun W_S1_V5 () Bool)
+(declare-fun W_S1_V2 () Bool)
+(declare-fun W_S1_V3 () Bool)
+(declare-fun W_S1_V1 () Bool)
+(declare-fun R_S1_V1 () Bool)
+(declare-fun R_S2_V6 () Bool)
+(declare-fun R_S2_V4 () Bool)
+(declare-fun R_S2_V5 () Bool)
+(declare-fun R_S2_V2 () Bool)
+(declare-fun R_S2_V3 () Bool)
+(declare-fun R_S2_V1 () Bool)
+(declare-fun R_E1_V6 () Bool)
+(declare-fun R_E1_V4 () Bool)
+(declare-fun R_E1_V5 () Bool)
+(declare-fun R_E1_V2 () Bool)
+(declare-fun R_E1_V3 () Bool)
+(declare-fun R_E1_V1 () Bool)
+(declare-fun DISJ_W_S2_R_E1 () Bool)
+(declare-fun DISJ_W_S2_R_S2 () Bool)
+(declare-fun R_S1_V6 () Bool)
+(declare-fun R_S1_V4 () Bool)
+(declare-fun R_S1_V5 () Bool)
+(declare-fun R_S1_V2 () Bool)
+(declare-fun R_S1_V3 () Bool)
+(declare-fun DISJ_W_S2_R_S1 () Bool)
+(declare-fun DISJ_W_S1_W_S2 () Bool)
+(declare-fun DISJ_W_S1_R_E1 () Bool)
+(declare-fun DISJ_W_S1_R_S2 () Bool)
+(declare-fun DISJ_W_S1_R_S1 () Bool)
+(declare-fun W_S2_V5 () Bool)
+(declare-fun W_S1_V4 () Bool)
+(assert
+ (let
+ (($x1615
+   (forall
+    ((V1_0 Int) (V3_0 Int) 
+     (V2_0 Int) (V5_0 Int) 
+     (V4_0 Int) (V6_0 Int) 
+     (MW_S1_V1 Bool) (MW_S1_V3 Bool) 
+     (MW_S1_V2 Bool) (MW_S1_V5 Bool) 
+     (MW_S1_V4 Bool) (MW_S1_V6 Bool) 
+     (MW_S2_V1 Bool) (MW_S2_V3 Bool) 
+     (MW_S2_V2 Bool) (MW_S2_V5 Bool) 
+     (MW_S2_V4 Bool) (MW_S2_V6 Bool) 
+     (S1_V1_!158 Int) (S1_V1_!171 Int) 
+     (S2_V5_!167 Int) (S2_V5_!180 Int) 
+     (S1_V3_!159 Int) (S1_V3_!172 Int) 
+     (S1_V2_!160 Int) (S1_V2_!173 Int) 
+     (E1_!157 Int) (E1_!170 Int) 
+     (E1_!183 Int) (S2_V4_!168 Int) 
+     (S2_V4_!181 Int) (S2_V6_!169 Int) 
+     (S2_V6_!182 Int) (S1_V5_!161 Int) 
+     (S1_V5_!174 Int) (S2_V1_!164 Int) 
+     (S2_V1_!177 Int) (S1_V4_!162 Int) 
+     (S1_V4_!175 Int) (S2_V3_!165 Int) 
+     (S2_V3_!178 Int) (S2_V2_!166 Int) 
+     (S2_V2_!179 Int) (S1_V6_!163 Int) 
+     (S1_V6_!176 Int))
+    (let ((?x1431 (ite MW_S1_V6 S1_V6_!176 V6_0)))
+    (let ((?x1432 (ite MW_S2_V6 S2_V6_!182 ?x1431)))
+    (let ((?x1433 (ite MW_S1_V6 S1_V6_!163 V6_0)))
+    (let ((?x1434 (ite MW_S2_V6 S2_V6_!169 ?x1433)))
+    (let (($x1435 (= ?x1434 ?x1432)))
+    (let ((?x1436 (ite MW_S1_V4 S1_V4_!175 V4_0)))
+    (let ((?x1437 (ite MW_S2_V4 S2_V4_!181 ?x1436)))
+    (let ((?x1438 (ite MW_S1_V4 S1_V4_!162 V4_0)))
+    (let ((?x1439 (ite MW_S2_V4 S2_V4_!168 ?x1438)))
+    (let (($x1440 (= ?x1439 ?x1437)))
+    (let ((?x1441 (ite MW_S1_V5 S1_V5_!174 V5_0)))
+    (let ((?x1442 (ite MW_S2_V5 S2_V5_!180 ?x1441)))
+    (let ((?x1444 (ite MW_S1_V5 S1_V5_!161 V5_0)))
+    (let ((?x1445 (ite MW_S2_V5 S2_V5_!167 ?x1444)))
+    (let (($x1446 (= ?x1445 ?x1442)))
+    (let ((?x1447 (ite MW_S1_V2 S1_V2_!173 V2_0)))
+    (let ((?x1448 (ite MW_S2_V2 S2_V2_!179 ?x1447)))
+    (let ((?x1449 (ite MW_S1_V2 S1_V2_!160 V2_0)))
+    (let ((?x1450 (ite MW_S2_V2 S2_V2_!166 ?x1449)))
+    (let (($x1451 (= ?x1450 ?x1448)))
+    (let ((?x1467 (ite MW_S1_V3 S1_V3_!159 V3_0)))
+    (let ((?x1468 (+ 1 ?x1467)))
+    (let ((?x1458 (ite MW_S2_V3 S2_V3_!165 ?x1468)))
+    (let
+    (($x1459
+      (= ?x1458
+      (+ (ite MW_S2_V3 S2_V3_!178 (ite MW_S1_V3 S1_V3_!172 V3_0)) ?x1448
+      (* (- 1) E1_!183)))))
+    (let ((?x1460 (ite MW_S1_V1 S1_V1_!171 E1_!170)))
+    (let ((?x1487 (ite MW_S2_V1 S2_V1_!177 ?x1460)))
+    (let ((?x1453 (ite MW_S1_V1 S1_V1_!158 E1_!157)))
+    (let ((?x1489 (ite MW_S2_V1 S2_V1_!164 ?x1453)))
+    (let (($x1289 (= ?x1489 ?x1487)))
+    (let ((?x1455 (+ (- 1) ?x1448)))
+    (let (($x1376 (>= ?x1487 ?x1455)))
+    (let (($x1377 (<= V2_0 E1_!170)))
+    (let (($x1379 (not $x1377)))
+    (let ((?x1380 (+ (- 1) ?x1450)))
+    (let (($x1381 (>= ?x1489 ?x1380)))
+    (let (($x1479 (<= V2_0 E1_!157)))
+    (let (($x1456 (not $x1479)))
+    (let (($x1499 (and $x1456 $x1381 $x1379 $x1376)))
+    (let (($x1500 (not $x1499)))
+    (let (($x1502 (not MW_S2_V6)))
+    (let (($x1503 (or $x1502 W_S2_V6)))
+    (let (($x1504 (not MW_S2_V4)))
+    (let (($x1505 (or $x1504 W_S2_V4)))
+    (let (($x1508 (not MW_S2_V2)))
+    (let (($x1509 (or $x1508 W_S2_V2)))
+    (let (($x1510 (not MW_S2_V3)))
+    (let (($x1511 (or $x1510 W_S2_V3)))
+    (let (($x1512 (not MW_S2_V1)))
+    (let (($x1513 (or $x1512 W_S2_V1)))
+    (let (($x1514 (not MW_S1_V6)))
+    (let (($x1515 (or $x1514 W_S1_V6)))
+    (let (($x1518 (not MW_S1_V5)))
+    (let (($x1519 (or $x1518 W_S1_V5)))
+    (let (($x1520 (not MW_S1_V2)))
+    (let (($x1521 (or $x1520 W_S1_V2)))
+    (let (($x1522 (not MW_S1_V3)))
+    (let (($x1523 (or $x1522 W_S1_V3)))
+    (let (($x1524 (not MW_S1_V1)))
+    (let (($x1525 (or $x1524 W_S1_V1)))
+    (let (($x1527 (= S1_V6_!176 S1_V6_!163)))
+    (let (($x1528 (= E1_!170 E1_!157)))
+    (let (($x228 (not R_S1_V1)))
+    (let (($x1529 (or $x228 $x1528)))
+    (let (($x1530 (not $x1529)))
+    (let (($x1531 (or $x1530 $x1527)))
+    (let (($x1532 (= S2_V2_!179 S2_V2_!166)))
+    (let (($x1533 (= ?x1431 ?x1433)))
+    (let (($x253 (not R_S2_V6)))
+    (let (($x1534 (or $x253 $x1533)))
+    (let (($x1535 (= ?x1436 ?x1438)))
+    (let (($x251 (not R_S2_V4)))
+    (let (($x1536 (or $x251 $x1535)))
+    (let (($x1537 (= ?x1441 ?x1444)))
+    (let (($x249 (not R_S2_V5)))
+    (let (($x1538 (or $x249 $x1537)))
+    (let (($x1539 (= ?x1447 ?x1449)))
+    (let (($x247 (not R_S2_V2)))
+    (let (($x1540 (or $x247 $x1539)))
+    (let ((?x1462 (ite MW_S1_V3 S1_V3_!172 V3_0)))
+    (let (($x1541 (= ?x1462 ?x1468)))
+    (let (($x245 (not R_S2_V3)))
+    (let (($x1542 (or $x245 $x1541)))
+    (let (($x1543 (= ?x1460 ?x1453)))
+    (let (($x243 (not R_S2_V1)))
+    (let (($x1544 (or $x243 $x1543)))
+    (let (($x1545 (and $x1544 $x1542 $x1540 $x1538 $x1536 $x1534)))
+    (let (($x1546 (not $x1545)))
+    (let (($x1547 (or $x1546 $x1532)))
+    (let (($x1548 (= S2_V3_!165 S2_V3_!178)))
+    (let (($x1549 (= ?x1433 ?x1431)))
+    (let (($x1550 (or $x253 $x1549)))
+    (let (($x1551 (= ?x1438 ?x1436)))
+    (let (($x1552 (or $x251 $x1551)))
+    (let (($x1553 (= ?x1444 ?x1441)))
+    (let (($x1554 (or $x249 $x1553)))
+    (let (($x1555 (= ?x1449 ?x1447)))
+    (let (($x1556 (or $x247 $x1555)))
+    (let ((?x1557 (+ (- 1) ?x1462)))
+    (let (($x1558 (= ?x1467 ?x1557)))
+    (let (($x1559 (or $x245 $x1558)))
+    (let (($x1560 (= ?x1453 ?x1460)))
+    (let (($x1561 (or $x243 $x1560)))
+    (let (($x1562 (and $x1561 $x1559 $x1556 $x1554 $x1552 $x1550)))
+    (let (($x1563 (not $x1562)))
+    (let (($x1564 (or $x1563 $x1548)))
+    (let (($x1565 (= S1_V4_!175 S1_V4_!162)))
+    (let (($x1566 (or $x1530 $x1565)))
+    (let (($x1567 (= S2_V1_!177 S2_V1_!164)))
+    (let (($x1568 (or $x1546 $x1567)))
+    (let (($x1569 (= S1_V5_!174 S1_V5_!161)))
+    (let (($x1570 (or $x1530 $x1569)))
+    (let (($x1571 (= S2_V6_!182 S2_V6_!169)))
+    (let (($x1572 (or $x1546 $x1571)))
+    (let (($x1573 (= S2_V4_!168 S2_V4_!181)))
+    (let (($x1574 (or $x1563 $x1573)))
+    (let (($x1575 (= E1_!170 E1_!183)))
+    (let (($x1576 (= V6_0 ?x1432)))
+    (let (($x177 (not R_E1_V6)))
+    (let (($x1577 (or $x177 $x1576)))
+    (let (($x1578 (= V4_0 ?x1437)))
+    (let (($x175 (not R_E1_V4)))
+    (let (($x1579 (or $x175 $x1578)))
+    (let (($x1580 (= V5_0 ?x1442)))
+    (let (($x173 (not R_E1_V5)))
+    (let (($x1581 (or $x173 $x1580)))
+    (let (($x1582 (= V2_0 ?x1448)))
+    (let (($x171 (not R_E1_V2)))
+    (let (($x1583 (or $x171 $x1582)))
+    (let ((?x1463 (ite MW_S2_V3 S2_V3_!178 ?x1462)))
+    (let (($x1584 (= V3_0 ?x1463)))
+    (let (($x169 (not R_E1_V3)))
+    (let (($x1585 (or $x169 $x1584)))
+    (let ((?x1586 (+ 1 ?x1487)))
+    (let (($x1587 (= V1_0 ?x1586)))
+    (let (($x167 (not R_E1_V1)))
+    (let (($x1588 (or $x167 $x1587)))
+    (let (($x1589 (and $x1588 $x1585 $x1583 $x1581 $x1579 $x1577)))
+    (let (($x1590 (not $x1589)))
+    (let (($x1591 (or $x1590 $x1575)))
+    (let (($x1592 (= E1_!157 E1_!183)))
+    (let (($x1593 (or $x1590 $x1592)))
+    (let (($x1594 (= E1_!157 E1_!170)))
+    (let (($x1595 (= S1_V2_!173 S1_V2_!160)))
+    (let (($x1596 (or $x1530 $x1595)))
+    (let (($x1597 (= S1_V3_!159 S1_V3_!172)))
+    (let (($x1598 (or $x228 $x1594)))
+    (let (($x1599 (not $x1598)))
+    (let (($x1600 (or $x1599 $x1597)))
+    (let (($x1601 (= S2_V5_!180 S2_V5_!167)))
+    (let (($x1602 (or $x1546 $x1601)))
+    (let (($x1603 (= S1_V1_!158 S1_V1_!171)))
+    (let (($x1604 (or $x1599 $x1603)))
+    (let
+    (($x1612
+      (and $x1604 $x1602 $x1600 $x1596 $x1594 $x1593 $x1591 $x1574 $x1572
+      $x1570 $x1568 $x1566 $x1564 $x1547 $x1531 $x1525 $x1523 $x1521 $x1519
+      $x1515 $x1513 $x1511 $x1509 $x1505 $x1503)))
+    (let (($x1613 (not $x1612)))
+    (or $x1613 $x1500 (and $x1289 $x1459 $x1451 $x1446 $x1440 $x1435)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+ (let (($x103 (and W_S2_V6 R_E1_V6)))
+ (let (($x102 (and W_S2_V4 R_E1_V4)))
+ (let (($x100 (and W_S2_V2 R_E1_V2)))
+ (let (($x99 (and W_S2_V3 R_E1_V3)))
+ (let (($x98 (and W_S2_V1 R_E1_V1)))
+ (let (($x128 (or $x98 $x99 $x100 R_E1_V5 $x102 $x103)))
+ (let (($x129 (not $x128)))
+ (let (($x130 (= DISJ_W_S2_R_E1 $x129)))
+ (let (($x93 (and W_S2_V6 R_S2_V6)))
+ (let (($x92 (and W_S2_V4 R_S2_V4)))
+ (let (($x90 (and W_S2_V2 R_S2_V2)))
+ (let (($x89 (and W_S2_V3 R_S2_V3)))
+ (let (($x88 (and W_S2_V1 R_S2_V1)))
+ (let (($x125 (or $x88 $x89 $x90 R_S2_V5 $x92 $x93)))
+ (let (($x126 (not $x125)))
+ (let (($x127 (= DISJ_W_S2_R_S2 $x126)))
+ (let (($x83 (and W_S2_V6 R_S1_V6)))
+ (let (($x82 (and W_S2_V4 R_S1_V4)))
+ (let (($x80 (and W_S2_V2 R_S1_V2)))
+ (let (($x79 (and W_S2_V3 R_S1_V3)))
+ (let (($x78 (and W_S2_V1 R_S1_V1)))
+ (let (($x122 (or $x78 $x79 $x80 R_S1_V5 $x82 $x83)))
+ (let (($x123 (not $x122)))
+ (let (($x124 (= DISJ_W_S2_R_S1 $x123)))
+ (let (($x73 (and W_S1_V6 W_S2_V6)))
+ (let (($x68 (and W_S1_V2 W_S2_V2)))
+ (let (($x66 (and W_S1_V3 W_S2_V3)))
+ (let (($x64 (and W_S1_V1 W_S2_V1)))
+ (let (($x119 (or $x64 $x66 $x68 W_S1_V5 W_S2_V4 $x73)))
+ (let (($x120 (not $x119)))
+ (let (($x121 (= DISJ_W_S1_W_S2 $x120)))
+ (let (($x58 (and W_S1_V6 R_E1_V6)))
+ (let (($x54 (and W_S1_V5 R_E1_V5)))
+ (let (($x52 (and W_S1_V2 R_E1_V2)))
+ (let (($x50 (and W_S1_V3 R_E1_V3)))
+ (let (($x48 (and W_S1_V1 R_E1_V1)))
+ (let (($x116 (or $x48 $x50 $x52 $x54 R_E1_V4 $x58)))
+ (let (($x117 (not $x116)))
+ (let (($x118 (= DISJ_W_S1_R_E1 $x117)))
+ (let (($x42 (and W_S1_V6 R_S2_V6)))
+ (let (($x38 (and W_S1_V5 R_S2_V5)))
+ (let (($x36 (and W_S1_V2 R_S2_V2)))
+ (let (($x34 (and W_S1_V3 R_S2_V3)))
+ (let (($x32 (and W_S1_V1 R_S2_V1)))
+ (let (($x113 (or $x32 $x34 $x36 $x38 R_S2_V4 $x42)))
+ (let (($x114 (not $x113)))
+ (let (($x115 (= DISJ_W_S1_R_S2 $x114)))
+ (let (($x26 (and W_S1_V6 R_S1_V6)))
+ (let (($x21 (and W_S1_V5 R_S1_V5)))
+ (let (($x18 (and W_S1_V2 R_S1_V2)))
+ (let (($x15 (and W_S1_V3 R_S1_V3)))
+ (let (($x12 (and W_S1_V1 R_S1_V1)))
+ (let (($x110 (or $x12 $x15 $x18 $x21 R_S1_V4 $x26)))
+ (let (($x111 (not $x110)))
+ (let (($x112 (= DISJ_W_S1_R_S1 $x111)))
+ (and W_S1_V4 W_S2_V5 $x112 $x115 $x118 $x121 $x124 $x127 $x130 $x1615))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(assert
+ (let (($x1192 (not W_S2_V2)))
+ (let (($x1189 (not W_S2_V3)))
+ (let (($x1186 (not W_S2_V1)))
+ (let (($x1091 (not W_S1_V2)))
+ (let (($x1078 (not W_S1_V1)))
+ (let (($x245 (not R_S2_V3)))
+ (let (($x167 (not R_E1_V1)))
+ (let
+ (($x1647
+   (and $x167 $x245 $x1078 $x1091 $x1186 $x1189 $x1192 DISJ_W_S1_R_E1
+   DISJ_W_S2_R_E1))) (not $x1647))))))))))
+(check-sat)
+
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 092c1548f..60b10666e 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -53,7 +53,8 @@ TESTS =	\
 	nested-delta.smt2 \
 	nested-inf.smt2 \
 	RND-small.smt2 \
-	clock-10.smt2
+	clock-10.smt2 \
+	006-cbqi-ite.smt2