Improvements to handling of mixed Int/Real quantifiers.

14 files changed, 367 insertions, 238 deletions

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 4619d74e5..0e7b02b53 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -142,7 +142,7 @@ Node CandidateGeneratorQELitEq::getNextCandidate(){
   while( !d_eq.isFinished() ){
     Node n = (*d_eq);
     ++d_eq;
-    if( n.getType().isSubtypeOf( d_match_pattern[0].getType() ) ){
+    if( n.getType().isComparableTo( d_match_pattern[0].getType() ) ){
       //an equivalence class with the same type as the pattern, return reflexive equality
       return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n );
     }
@@ -199,7 +199,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() {
   while( !d_eq.isFinished() ){
     TNode n = (*d_eq);
     ++d_eq;
-    if( n.getType().isSubtypeOf( d_match_pattern_type ) ){
+    if( n.getType().isComparableTo( d_match_pattern_type ) ){
       TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n );
       if( !nh.isNull() ){
         if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index c7bf61eab..5ae8905d1 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -285,13 +285,13 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
 
       //[3] directly look at assertions
       Trace("cbqi-inst-debug") << "[3] try based on assertions." << std::endl;
-      Node vts_sym[2];
-      vts_sym[0] = d_qe->getTermDatabase()->getVtsInfinity( pvtn, false, false );
-      vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta( false, false );
+      d_vts_sym[0] = d_qe->getTermDatabase()->getVtsInfinity( pvtn, false, false );
+      d_vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta( false, false );
       std::vector< Node > mbp_bounds[2];
       std::vector< Node > mbp_coeff[2];
       std::vector< Node > mbp_vts_coeff[2][2];
       std::vector< Node > mbp_lit[2];
+      //std::vector< MbpBounds > mbp_bounds[2];
       unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2;
       for( unsigned r=0; r<rmax; r++ ){
         TheoryId tid = r==0 ? Theory::theoryOf( pv ) : Theory::theoryOf( pv.getType() );
@@ -340,164 +340,102 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
                     //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" );
-                      }
-                      //get the coefficient of infinity and remove it from msum
-                      Node vts_coeff[2];
-                      for( unsigned t=0; t<2; t++ ){
-                        if( !vts_sym[t].isNull() ){
-                          std::map< Node, Node >::iterator itminf = msum.find( vts_sym[t] );
-                          if( itminf!=msum.end() ){
-                            vts_coeff[t] = itminf->second;
-                            if( vts_coeff[t].isNull() ){
-                              vts_coeff[t] = NodeManager::currentNM()->mkConst( Rational( 1 ) );
-                            }
-                            //negate if coefficient on variable is positive
-                            std::map< Node, Node >::iterator itv = msum.find( pv );
-                            if( itv!=msum.end() ){
-                              //multiply by the coefficient we will isolate for
-                              if( itv->second.isNull() ){
-                                vts_coeff[t] = QuantArith::negate(vts_coeff[t]);
-                              }else{
-                                if( !pvtn.isInteger() ){
-                                  vts_coeff[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) / itv->second.getConst<Rational>() ), vts_coeff[t] );
-                                  vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] );
-                                }else if( itv->second.getConst<Rational>().sgn()==1 ){
-                                  vts_coeff[t] = QuantArith::negate(vts_coeff[t]);
-                                }
-                              }
-                            }
-                            Trace("cbqi-inst-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl;
-                            msum.erase( vts_sym[t] );
-                          }
-                        }
-                      }
-
-                      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 );
-                          }
-                        }
-
-                        //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() ){
-                                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{
-                            bool is_upper = ( r==0 );
-                            if( options::cbqiModel() ){
-                              // disequality is a disjunction : only consider the bound in the direction of the model
-                              //first check if there is an infinity...
-                              if( !vts_coeff[0].isNull() ){
-                                //coefficient or val won't make a difference, just compare with zero
-                                Trace("cbqi-inst-debug") << "Disequality : check infinity polarity " << vts_coeff[0] << std::endl;
-                                Assert( vts_coeff[0].isConst() );
-                                is_upper = ( vts_coeff[0].getConst<Rational>().sgn()==1 );
-                              }else{
-                                Node rhs_value = getModelValue( 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 );
-                                }
-                                Trace("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl;
-                                Assert( lhs_value!=rhs_value );
-                                Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value );
-                                cmp = Rewriter::rewrite( cmp );
-                                Assert( cmp.isConst() );
-                                is_upper = ( cmp!=d_true );
-                              }
-                            }
-                            Assert( atom.getKind()==EQUAL && !pol );
+                    Node vts_coeff_inf;
+                    Node vts_coeff_delta;
+                    Node val;
+                    Node veq_c;
+                    //isolate pv in the inequality
+                    int ires = isolate( pv, satom, veq_c, val, vts_coeff_inf, vts_coeff_delta );
+                    if( ires!=0 ){
+                      //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 = is_upper ? -1 : 1;
                               uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
                               uval = Rewriter::rewrite( uval );
                             }else{
                               Assert( pvtn.isReal() );
-                              uires = is_upper ? -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;
-                          //take into account delta
-                          if( d_use_vts_delta && ( uires==2 || uires==-2 ) ){
-                            if( options::cbqiModel() ){
-                              Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) );
-                              if( vts_coeff[1].isNull() ){
-                                vts_coeff[1] = delta_coeff;
-                              }else{
-                                vts_coeff[1] = NodeManager::currentNM()->mkNode( PLUS, vts_coeff[1], delta_coeff );
-                                vts_coeff[1] = Rewriter::rewrite( vts_coeff[1] );
-                              }
+                        }else{
+                          bool is_upper = ( r==0 );
+                          if( options::cbqiModel() ){
+                            // disequality is a disjunction : only consider the bound in the direction of the model
+                            //first check if there is an infinity...
+                            if( !vts_coeff_inf.isNull() ){
+                              //coefficient or val won't make a difference, just compare with zero
+                              Trace("cbqi-inst-debug") << "Disequality : check infinity polarity " << vts_coeff_inf << std::endl;
+                              Assert( vts_coeff_inf.isConst() );
+                              is_upper = ( vts_coeff_inf.getConst<Rational>().sgn()==1 );
                             }else{
-                              Node delta = d_qe->getTermDatabase()->getVtsDelta();
-                              uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta );
-                              uval = Rewriter::rewrite( uval );
+                              Node rhs_value = getModelValue( 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 );
+                              }
+                              Trace("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl;
+                              Assert( lhs_value!=rhs_value );
+                              Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value );
+                              cmp = Rewriter::rewrite( cmp );
+                              Assert( cmp.isConst() );
+                              is_upper = ( cmp!=d_true );
                             }
                           }
+                          Assert( atom.getKind()==EQUAL && !pol );
+                          if( pvtn.isInteger() ){
+                            uires = is_upper ? -1 : 1;
+                            uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) );
+                            uval = Rewriter::rewrite( uval );
+                          }else{
+                            Assert( pvtn.isReal() );
+                            uires = is_upper ? -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;
+                        //take into account delta
+                        if( d_use_vts_delta && ( uires==2 || uires==-2 ) ){
                           if( options::cbqiModel() ){
-                            //just store bounds, will choose based on tighest bound
-                            if( pvtn.isInteger() && !veq_c.isNull() && !veq_c.getType().isInteger() ){
-                              Trace("cbqi-bound2") << "Non-integer coefficient : " << veq_c << " for " << pv << std::endl;
-                              Assert( veq_c.isConst() );
-                              //multiply everything by denominator of coefficient
-                              Rational r = veq_c.getConst<Rational>();
-                              Node den = NodeManager::currentNM()->mkConst( Rational(r.getDenominator()) );
-                              uval = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, den, uval ) );
-                              veq_c = NodeManager::currentNM()->mkConst( Rational(r.getNumerator()) );
-                              for( unsigned t=0; t<2; t++ ){
-                                if( !vts_coeff[t].isNull() ){
-                                  vts_coeff[t] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, den, vts_coeff[t] ) );
-                                }
-                              }
-                            }
-                            unsigned index = uires>0 ? 0 : 1;
-                            mbp_bounds[index].push_back( uval );
-                            mbp_coeff[index].push_back( veq_c );
-                            for( unsigned t=0; t<2; t++ ){
-                              mbp_vts_coeff[index][t].push_back( vts_coeff[t] );
+                            Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) );
+                            if( vts_coeff_delta.isNull() ){
+                              vts_coeff_delta = delta_coeff;
+                            }else{
+                              vts_coeff_delta = NodeManager::currentNM()->mkNode( PLUS, vts_coeff_delta, delta_coeff );
+                              vts_coeff_delta = Rewriter::rewrite( vts_coeff_delta );
                             }
-                            mbp_lit[index].push_back( lit );
                           }else{
-                            //try this bound
-                            if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
-                              subs_proc[uval][veq_c] = true;
-                              if( addInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
-                                return true;
-                              }
+                            Node delta = d_qe->getTermDatabase()->getVtsDelta();
+                            uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta );
+                            uval = Rewriter::rewrite( uval );
+                          }
+                        }
+                        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 );
+                          for( unsigned t=0; t<2; t++ ){
+                            mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta );
+                          }
+                          mbp_lit[index].push_back( lit );
+                        }else{
+                          //try this bound
+                          if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
+                            subs_proc[uval][veq_c] = true;
+                            if( addInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                              return true;
                             }
                           }
                         }
@@ -622,7 +560,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
                 best_used[rr] = (unsigned)best;
                 Node val = mbp_bounds[rr][best];
                 val = getModelBasedProjectionValue( pv, val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta,
-                                                    mbp_vts_coeff[rr][0][best], vts_sym[0], mbp_vts_coeff[rr][1][best], vts_sym[1] );
+                                                    mbp_vts_coeff[rr][0][best], mbp_vts_coeff[rr][1][best] );
                 if( !val.isNull() ){
                   if( subs_proc[val].find( mbp_coeff[rr][best] )==subs_proc[val].end() ){
                     subs_proc[val][mbp_coeff[rr][best]] = true;
@@ -638,7 +576,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
           if( !use_inf && mbp_bounds[0].empty() && mbp_bounds[1].empty() ){
             Node val = d_zero;
             Node c; //null (one) coefficient
-            val = getModelBasedProjectionValue( pv, val, true, c, pv_value, d_zero, theta, Node::null(), vts_sym[0], Node::null(), vts_sym[1] );
+            val = getModelBasedProjectionValue( pv, val, true, c, pv_value, d_zero, theta, Node::null(), Node::null() );
             if( !val.isNull() ){
               if( subs_proc[val].find( c )==subs_proc[val].end() ){
                 subs_proc[val][c] = true;
@@ -658,7 +596,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve
             for( unsigned j=0; j<mbp_bounds[rr].size(); j++ ){
               if( j!=best_used[rr] ){
                 Node val = getModelBasedProjectionValue( pv, mbp_bounds[rr][j], rr==0, mbp_coeff[rr][j], pv_value, t_values[rr][j], theta,
-                                                         mbp_vts_coeff[rr][0][j], vts_sym[0], mbp_vts_coeff[rr][1][j], vts_sym[1] );
+                                                         mbp_vts_coeff[rr][0][j], mbp_vts_coeff[rr][1][j] );
                 if( !val.isNull() ){
                   if( subs_proc[val].find( mbp_coeff[rr][j] )==subs_proc[val].end() ){
                     subs_proc[val][mbp_coeff[rr][j]] = true;
@@ -904,6 +842,14 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector<
       subs.push_back( n );
     }
   }
+  if( !d_var_order_index.empty() ){
+    std::vector< Node > subs_orig;
+    subs_orig.insert( subs_orig.end(), subs.begin(), subs.end() );
+    subs.clear();
+    for( unsigned i=0; i<subs_orig.size(); i++ ){
+      subs.push_back( subs_orig[d_var_order_index[i]] );
+    }
+  }
   bool ret = d_out->addInstantiation( subs );
 #ifdef MBP_STRICT_ASSERTIONS
   Assert( ret );
@@ -1029,12 +975,13 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
   }
 }
 
-Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta,
-                                                    Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta ) {
+Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) {
+  /*
   if( e.getType().isInteger() && !t.getType().isInteger() ){
     //TODO : round up/down this bound?
     return Node::null();
   }
+  */
   Node val = t;
   Trace("cbqi-bound2") << "Value : " << val << std::endl;
   //add rho value
@@ -1056,6 +1003,10 @@ Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower
   }
   if( !new_theta.isNull() && e.getType().isInteger() ){
     Node rho;
+    //if( !mt.getType().isInteger() ){
+      //round up/down
+      //mt = NodeManager::currentNM()->mkNode( 
+    //}
     if( isLower ){
       rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt );
     }else{
@@ -1073,16 +1024,16 @@ Node CegInstantiator::getModelBasedProjectionValue( Node e, Node t, bool isLower
     Trace("cbqi-bound2") << "(after rho) : " << val << std::endl;
   }
   if( !inf_coeff.isNull() ){
-    Assert( !vts_inf.isNull() );
-    val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, vts_inf ) );
+    Assert( !d_vts_sym[0].isNull() );
+    val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, d_vts_sym[0] ) );
     val = Rewriter::rewrite( val );
   }
   if( !delta_coeff.isNull() ){
     //create delta here if necessary
-    if( vts_delta.isNull() ){
-      vts_delta = d_qe->getTermDatabase()->getVtsDelta();
+    if( d_vts_sym[1].isNull() ){
+      d_vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta();
     }
-    val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, vts_delta ) );
+    val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, d_vts_sym[1] ) );
     val = Rewriter::rewrite( val );
   }
   return val;
@@ -1399,9 +1350,47 @@ void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited )
   }
 }
 
+struct sortCegVarOrder {
+  bool operator() (Node i, Node j) {
+    TypeNode it = i.getType();
+    TypeNode jt = j.getType();
+    return ( it!=jt && jt.isSubtypeOf( it ) ) || ( it==jt && i<j );
+  }
+};
+
+
 void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
   Assert( d_vars.empty() );
   d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() );
+
+  //determine variable order: must do Reals before Ints
+  if( !d_vars.empty() ){
+    TypeNode tn0 = d_vars[0].getType();
+    bool doSort = false;
+    std::map< Node, unsigned > voo;
+    for( unsigned i=0; i<d_vars.size(); i++ ){
+      voo[d_vars[i]] = i;
+      d_var_order_index.push_back( 0 );
+      if( d_vars[i].getType()!=tn0 ){
+        doSort = true;
+      }
+    }
+    if( doSort ){
+      Trace("cbqi-debug") << "Sort variables based on ordering." << std::endl;
+      sortCegVarOrder scvo;
+      std::sort( d_vars.begin(), d_vars.end(), scvo );
+      Trace("cbqi-debug") << "Consider variables in this order : " << std::endl;
+      for( unsigned i=0; i<d_vars.size(); i++ ){
+        d_var_order_index[voo[d_vars[i]]] = i;
+        Trace("cbqi-debug") << "  " << d_vars[i] << " : " << d_vars[i].getType() << ", index was : " << voo[d_vars[i]] << std::endl;
+      }
+      Trace("cbqi-debug") << std::endl;
+    }else{
+      d_var_order_index.clear();
+    }
+  }
+  
+  //remove ITEs 
   IteSkolemMap iteSkolemMap;
   d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap);
   Assert( d_aux_vars.empty() );
@@ -1435,3 +1424,103 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
     collectCeAtoms( lems[i], visited );
   }
 }
+
+//this isolates the monomial sum into solved form (pv k t), ensures t is Int if pv is Int, and t does not contain vts symbols
+int CegInstantiator::isolate( Node pv, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta ) {
+  int ires = 0;
+  Trace("cbqi-inst-debug") << "isolate for " << pv << " in " << atom << std::endl;
+  std::map< Node, Node > msum;
+  if( QuantArith::getMonomialSumLit( atom, msum ) ){
+    Trace("cbqi-inst-debug") << "got monomial sum: " << std::endl;
+    if( Trace.isOn("cbqi-inst-debug") ){
+      QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" );
+    }
+    TypeNode pvtn = pv.getType();
+    //remove vts symbols from polynomial
+    Node vts_coeff[2];
+    for( unsigned t=0; t<2; t++ ){
+      if( !d_vts_sym[t].isNull() ){
+        std::map< Node, Node >::iterator itminf = msum.find( d_vts_sym[t] );
+        if( itminf!=msum.end() ){
+          vts_coeff[t] = itminf->second;
+          if( vts_coeff[t].isNull() ){
+            vts_coeff[t] = NodeManager::currentNM()->mkConst( Rational( 1 ) );
+          }
+          //negate if coefficient on variable is positive
+          std::map< Node, Node >::iterator itv = msum.find( pv );
+          if( itv!=msum.end() ){
+            //multiply by the coefficient we will isolate for
+            if( itv->second.isNull() ){
+              vts_coeff[t] = QuantArith::negate(vts_coeff[t]);
+            }else{
+              if( !pvtn.isInteger() ){
+                vts_coeff[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) / itv->second.getConst<Rational>() ), vts_coeff[t] );
+                vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] );
+              }else if( itv->second.getConst<Rational>().sgn()==1 ){
+                vts_coeff[t] = QuantArith::negate(vts_coeff[t]);
+              }
+            }
+          }
+          Trace("cbqi-inst-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl;
+          msum.erase( d_vts_sym[t] );
+        }
+      }
+    }
+    
+    ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() );
+    if( ires!=0 ){
+      Node realPart;
+      Trace("cbqi-inst-debug") << "Isolate : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl;
+      if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){
+        //redo, split integer/non-integer parts
+        bool useCoeff = false;
+        Integer coeff = d_one.getConst<Rational>().getNumerator();
+        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+          if( it->first.isNull() || it->first.getType().isInteger() ){
+            if( !it->second.isNull() ){
+              coeff = coeff.lcm( it->second.getConst<Rational>().getDenominator() );
+              useCoeff = true;
+            }
+          }
+        }
+        //multiply everything by this coefficient
+        Node rcoeff = NodeManager::currentNM()->mkConst( Rational( coeff ) );
+        std::vector< Node > real_part;
+        for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+          if( useCoeff ){
+            if( it->second.isNull() ){
+              msum[it->first] = rcoeff;
+            }else{
+              msum[it->first] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, it->second, rcoeff ) );
+            }
+          }
+          if( !it->first.isNull() && !it->first.getType().isInteger() ){
+            real_part.push_back( msum[it->first].isNull() ? it->first : NodeManager::currentNM()->mkNode( MULT, msum[it->first], it->first ) );
+          }
+        }
+        for( unsigned t=0; t<2; t++ ){
+          if( !vts_coeff[t].isNull() ){
+            vts_coeff[t] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[t] ) );
+          }
+        }
+        realPart = real_part.empty() ? d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) );
+        Assert( d_out->isEligibleForInstantiation( realPart ) );
+        //re-isolate
+        ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() );
+        Trace("cbqi-inst-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl;
+        Trace("cbqi-inst-debug") << "                 real part : " << realPart << std::endl;
+        if( ires!=0 ){
+          val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires==-1 ? PLUS : MINUS, 
+                                    NodeManager::currentNM()->mkNode( ires==-1 ? MINUS : PLUS, val, realPart ),
+                                    NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) );
+          Trace("cbqi-inst-debug") << "result : " << val << std::endl;
+          Assert( val.getType().isInteger() );
+        }
+      }
+    }
+    vts_coeff_inf = vts_coeff[0];
+    vts_coeff_delta = vts_coeff[1];
+  }
+    
+  return ires;
+}
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h
index 38bb12e5b..9504bd407 100644
--- a/src/theory/quantifiers/ceg_instantiator.h
+++ b/src/theory/quantifiers/ceg_instantiator.h
@@ -48,6 +48,7 @@ private:
   Node d_true;
   bool d_use_vts_delta;
   bool d_use_vts_inf;
+  Node d_vts_sym[2];
   //program variable contains cache
   std::map< Node, std::map< Node, bool > > d_prog_var;
   std::map< Node, bool > d_inelig;
@@ -61,6 +62,8 @@ private:
   std::map< Node, std::map< Node, Node > > d_aux_eq;
   //the CE variables
   std::vector< Node > d_vars;
+  //index of variables reported in instantiation
+  std::vector< unsigned > d_var_order_index;
   //atoms of the CE lemma
   bool d_is_nested_quant;
   std::vector< Node > d_ce_atoms;
@@ -95,6 +98,15 @@ private:
       }
     }
   };
+  /*
+  class MbpBound {
+  public:
+    Node d_bound;
+    Node d_coeff;
+    Node d_vts_coeff[2];
+    Node d_lit;
+  };
+  */
   // effort=0 : do not use model value, 1: use model value, 2: one must use model value
   bool addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
                          std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
@@ -112,12 +124,13 @@ private:
   }
   Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff,
                           std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true );
-  Node getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta,
-                                     Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta );
+  Node getModelBasedProjectionValue( Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff );
   void processAssertions();
   void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r );
   //get model value
   Node getModelValue( Node n );
+private:
+  int isolate( Node v, Node atom, Node & veq_c, Node & val, Node& vts_coeff_inf, Node& vts_coeff_delta );
 public:
   CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true );
   //check : add instantiations based on valuation of d_vars
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index f7dc709d9..47e838f1c 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -341,7 +341,8 @@ bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine*
     t = d_cg->getNextCandidate();
     Trace("matching-debug2") << "Matching candidate : " << t << std::endl;
     //if t not null, try to fit it into match m
-    if( !t.isNull() && t.getType().isSubtypeOf( d_match_pattern_type ) ){
+    if( !t.isNull() ){
+      Assert( t.getType().isComparableTo( d_match_pattern_type ) );
       success = getMatch( f, t, m, qe );
     }
   }while( !success && !t.isNull() );
@@ -431,7 +432,7 @@ VarMatchGeneratorBooleanTerm::VarMatchGeneratorBooleanTerm( Node var, Node comp
   d_var_num[0] = var.getAttribute(InstVarNumAttribute());
 }
 
-bool VarMatchGeneratorBooleanTerm::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) {
+bool VarMatchGeneratorBooleanTerm::getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) {
   if( !d_eq_class.isNull() ){
     Node s = NodeManager::currentNM()->mkConst(qe->getEqualityQuery()->areEqual( d_eq_class, d_pattern ));
     d_eq_class = Node::null();
@@ -439,7 +440,7 @@ bool VarMatchGeneratorBooleanTerm::getNextMatch( Node f, InstMatch& m, Quantifie
     if( !m.set( qe, d_var_num[0], s ) ){
       return false;
     }else{
-      if( continueNextMatch( f, m, qe ) ){
+      if( continueNextMatch( q, m, qe ) ){
         return true;
       }
     }
@@ -454,26 +455,24 @@ bool VarMatchGeneratorBooleanTerm::getNextMatch( Node f, InstMatch& m, Quantifie
 VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( Node var, Node subs ) :
   InstMatchGenerator(), d_var( var ), d_subs( subs ), d_rm_prev( false ){
   d_var_num[0] = d_var.getAttribute(InstVarNumAttribute());
+  d_var_type = d_var.getType();
 }
 
-bool VarMatchGeneratorTermSubs::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) {
+bool VarMatchGeneratorTermSubs::getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) {
   if( !d_eq_class.isNull() ){
     Trace("var-trigger-matching") << "Matching " << d_eq_class << " against " << d_var << " in " << d_subs << std::endl;
     Node s = d_subs.substitute( d_var, d_eq_class );
     s = Rewriter::rewrite( s );
     Trace("var-trigger-matching") << "...got " << s << std::endl;
     d_eq_class = Node::null();
-    if( s.getType().isSubtypeOf( d_var.getType() ) ){
-      d_rm_prev = m.get( d_var_num[0] ).isNull();
-      if( !m.set( qe, d_var_num[0], s ) ){
-        return false;
-      }else{
-        if( continueNextMatch( f, m, qe ) ){
-          return true;
-        }
-      }
+    //if( s.getType().isSubtypeOf( d_var_type ) ){
+    d_rm_prev = m.get( d_var_num[0] ).isNull();
+    if( !m.set( qe, d_var_num[0], s ) ){
+      return false;
     }else{
-      Trace("var-trigger-matching") << "Violates type requirement." << std::endl;
+      if( continueNextMatch( q, m, qe ) ){
+        return true;
+      }
     }
   }
   if( d_rm_prev ){
@@ -484,11 +483,11 @@ bool VarMatchGeneratorTermSubs::getNextMatch( Node f, InstMatch& m, QuantifiersE
 }
 
 /** constructors */
-InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe ) :
-d_f( f ){
-  Debug("smart-multi-trigger") << "Making smart multi-trigger for " << f << std::endl;
+InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) :
+d_f( q ){
+  Debug("smart-multi-trigger") << "Making smart multi-trigger for " << q << std::endl;
   std::map< Node, std::vector< Node > > var_contains;
-  qe->getTermDatabase()->getVarContains( f, pats, var_contains );
+  qe->getTermDatabase()->getVarContains( q, pats, var_contains );
   //convert to indicies
   for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){
     Debug("smart-multi-trigger") << "Pattern " << it->first << " contains: ";
@@ -503,7 +502,7 @@ d_f( f ){
   for( int i=0; i<(int)pats.size(); i++ ){
     Node n = pats[i];
     //make the match generator
-    d_children.push_back( InstMatchGenerator::mkInstMatchGenerator(f, n, qe ) );
+    d_children.push_back( InstMatchGenerator::mkInstMatchGenerator(q, n, qe ) );
     //compute unique/shared variables
     std::vector< int > unique_vars;
     std::map< int, bool > shared_vars;
@@ -561,14 +560,14 @@ void InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){
   }
 }
 
-int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
+int InstMatchGeneratorMulti::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){
   int addedLemmas = 0;
   Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl;
   for( int i=0; i<(int)d_children.size(); i++ ){
     Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl;
     std::vector< InstMatch > newMatches;
-    InstMatch m( f );
-    while( d_children[i]->getNextMatch( f, m, qe ) ){
+    InstMatch m( q );
+    while( d_children[i]->getNextMatch( q, m, qe ) ){
       //m.makeRepresentative( qe );
       newMatches.push_back( InstMatch( &m ) );
       m.clear();
@@ -684,15 +683,15 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe,
   }
 }
 
-int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){
+int InstMatchGeneratorMulti::addTerm( Node q, Node t, QuantifiersEngine* qe ){
   Assert( options::eagerInstQuant() );
   int addedLemmas = 0;
   for( int i=0; i<(int)d_children.size(); i++ ){
     Node t_op = qe->getTermDatabase()->getOperator( t );
     if( ((InstMatchGenerator*)d_children[i])->d_match_pattern_op==t_op ){
-      InstMatch m( f );
+      InstMatch m( q );
       //if it produces a match, then process it with the rest
-      if( ((InstMatchGenerator*)d_children[i])->getMatch( f, t, m, qe ) ){
+      if( ((InstMatchGenerator*)d_children[i])->getMatch( q, t, m, qe ) ){
         processNewMatch( qe, m, i, addedLemmas );
       }
     }
@@ -700,10 +699,10 @@ int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){
   return addedLemmas;
 }
 
-InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ) {
+InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat ) : d_f( q ), d_match_pattern( pat ) {
   for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
     if( d_match_pattern[i].getKind()==INST_CONSTANT ){
-      if( !options::cbqi() || quantifiers::TermDb::getInstConstAttr(d_match_pattern[i])==f ){
+      if( !options::cbqi() || quantifiers::TermDb::getInstConstAttr(d_match_pattern[i])==q ){
         d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
       }else{
         d_var_num[i] = -1;
@@ -717,8 +716,8 @@ void InstMatchGeneratorSimple::resetInstantiationRound( QuantifiersEngine* qe )
   d_op = qe->getTermDatabase()->getOperator( d_match_pattern );
 }
 
-int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
-  InstMatch m( f );
+int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){
+  InstMatch m( q );
   m.add( baseMatch );
   int addedLemmas = 0;
 
@@ -749,7 +748,8 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin
           Node t = it->first;
           Node prev = m.get( v );
           //using representatives, just check if equal
-          if( ( prev.isNull() || prev==t ) && t.getType().isSubtypeOf( d_match_pattern_arg_types[argIndex] ) ){
+          Assert( t.getType().isComparableTo( d_match_pattern_arg_types[argIndex] ) );
+          if( prev.isNull() || prev==t ){
             m.setValue( v, t);
             addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
             m.setValue( v, prev);
@@ -766,9 +766,9 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin
   }
 }
 
-int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){
+int InstMatchGeneratorSimple::addTerm( Node q, Node t, QuantifiersEngine* qe ){
   Assert( options::eagerInstQuant() );
-  InstMatch m( f );
+  InstMatch m( q );
   for( int i=0; i<(int)t.getNumChildren(); i++ ){
     if( d_match_pattern[i].getKind()==INST_CONSTANT ){
       m.setValue(d_var_num[i], t[i]);
@@ -776,7 +776,7 @@ int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){
       return 0;
     }
   }
-  return qe->addInstantiation( f, m, false ) ? 1 : 0;
+  return qe->addInstantiation( q, m, false ) ? 1 : 0;
 }
 
 }/* CVC4::theory::inst namespace */
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index aae6d4e73..75adeb2d8 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -39,11 +39,11 @@ public:
   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
   virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0;
   /** get the next match.  must call reset( eqc ) before this function. */
-  virtual bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) = 0;
+  virtual bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) = 0;
   /** add instantiations directly */
-  virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;
+  virtual int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;
   /** add ground term t, called when t is added to term db */
-  virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) { return 0; }
+  virtual int addTerm( Node q, Node t, QuantifiersEngine* qe ) { return 0; }
   /** set active add */
   virtual void setActiveAdd( bool val ) {}
 };/* class IMGenerator */
@@ -72,7 +72,7 @@ protected:
   /** children types 0 : variable, 1 : child term, -1 : ground term */
   std::vector< int > d_children_types;
   /** continue */
-  bool continueNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe );
+  bool continueNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
 public:
   enum {
     //options for producing matches
@@ -85,7 +85,7 @@ public:
       d_match_pattern and t should have the same shape.
       only valid for use where !d_match_pattern.isNull().
   */
-  bool getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe );
+  bool getMatch( Node q, Node t, InstMatch& m, QuantifiersEngine* qe );
 
   /** constructors */
   InstMatchGenerator( Node pat );
@@ -108,11 +108,11 @@ public:
   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
   void reset( Node eqc, QuantifiersEngine* qe );
   /** get the next match.  must call reset( eqc ) before this function. */
-  bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe );
+  bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
   /** add instantiations */
-  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
+  int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
   /** add ground term t */
-  int addTerm( Node f, Node t, QuantifiersEngine* qe );
+  int addTerm( Node q, Node t, QuantifiersEngine* qe );
 
   bool d_active_add;
   void setActiveAdd( bool val );
@@ -133,9 +133,9 @@ public:
   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
   void reset( Node eqc, QuantifiersEngine* qe ){ d_eq_class = eqc; }
   /** get the next match.  must call reset( eqc ) before this function. */
-  bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe );
+  bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
   /** add instantiations directly */
-  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){ return 0; }
+  int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){ return 0; }
 };
 
 //match generator for purified terms (matched term is substituted into d_subs)
@@ -144,6 +144,7 @@ public:
   VarMatchGeneratorTermSubs( Node var, Node subs );
   ~VarMatchGeneratorTermSubs() throw() {}
   TNode d_var;
+  TypeNode d_var_type;
   Node d_subs;
   bool d_rm_prev;
   /** reset instantiation round (call this at beginning of instantiation round) */
@@ -151,9 +152,9 @@ public:
   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
   void reset( Node eqc, QuantifiersEngine* qe ){ d_eq_class = eqc; }
   /** get the next match.  must call reset( eqc ) before this function. */
-  bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe );
+  bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
   /** add instantiations directly */
-  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) { return 0; }
+  int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ) { return 0; }
 };
 
 /** smart multi-trigger implementation */
@@ -188,7 +189,7 @@ private:
   void calculateMatches( QuantifiersEngine* qe );
 public:
   /** constructors */
-  InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe );
+  InstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe );
   /** destructor */
   ~InstMatchGeneratorMulti() throw() {}
   /** reset instantiation round (call this whenever equivalence classes have changed) */
@@ -196,11 +197,11 @@ public:
   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
   void reset( Node eqc, QuantifiersEngine* qe );
   /** get the next match.  must call reset( eqc ) before this function. (not implemented) */
-  bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; }
+  bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return false; }
   /** add instantiations */
-  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
+  int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
   /** add ground term t */
-  int addTerm( Node f, Node t, QuantifiersEngine* qe );
+  int addTerm( Node q, Node t, QuantifiersEngine* qe );
 };/* class InstMatchGeneratorMulti */
 
 /** smart (single)-trigger implementation */
@@ -220,7 +221,7 @@ private:
   void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat );
 public:
   /** constructors */
-  InstMatchGeneratorSimple( Node f, Node pat );
+  InstMatchGeneratorSimple( Node q, Node pat );
   /** destructor */
   ~InstMatchGeneratorSimple() throw() {}
   /** reset instantiation round (call this whenever equivalence classes have changed) */
@@ -228,11 +229,11 @@ public:
   /** reset, eqc is the equivalence class to search in (any if eqc=null) */
   void reset( Node eqc, QuantifiersEngine* qe ) {}
   /** get the next match.  must call reset( eqc ) before this function. (not implemented) */
-  bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; }
+  bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return false; }
   /** add instantiations */
-  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
+  int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
   /** add ground term t, possibly add instantiations */
-  int addTerm( Node f, Node t, QuantifiersEngine* qe );
+  int addTerm( Node q, Node t, QuantifiersEngine* qe );
 };/* class InstMatchGeneratorSimple */
 
 }
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 9e13ef5eb..a1af1313d 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1524,7 +1524,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
               if( it != d_qn[index]->d_data.end() ) {
                 d_qni.push_back( it );
                 //set the match
-                if( it->first.getType().isSubtypeOf( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first ) ){
+                if( it->first.getType().isComparableTo( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first ) ){
                   Debug("qcf-match-debug") << "       Binding variable" << std::endl;
                   if( d_qn.size()<d_qni_size ){
                     d_qn.push_back( &it->second );
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 026293e02..0b212d696 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -137,6 +137,24 @@ int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind
   return 0;
 }
 
+int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ) {
+  Node vatom;
+  //isolate pv in the inequality
+  int ires = isolate( v, msum, vatom, k, true );
+  if( ires!=0 ){
+    val = vatom[ ires==1 ? 1 : 0 ];
+    Node pvm = vatom[ ires==1 ? 0 : 1 ];
+    //get monomial
+    if( pvm!=v ){
+      Node veq_v;
+      if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){
+        Assert( veq_v==v );
+      }
+    }
+  }
+  return ires;
+}
+
 Node QuantArith::negate( Node t ) {
   Node tt = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) ), t );
   tt = Rewriter::rewrite( tt );
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 2186e03fd..f65163415 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -38,6 +38,7 @@ public:
   static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum );
   //return 1 : solved on LHS, return -1 : solved on RHS, return 0: failed
   static int isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff = false );
+  static int isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k );
   static Node negate( Node t );
   static Node offset( Node t, int i );
   static void debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 2c9430876..bfeacf044 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1481,6 +1481,19 @@ bool TermDb::containsVtsInfinity( Node n, bool isFree ) {
   return containsTerms( n, t );
 }
 
+Node TermDb::mkNodeType( Node n, TypeNode tn ) {
+  TypeNode ntn = n.getType();
+  Assert( ntn.isComparableTo( tn ) );
+  if( ntn.isSubtypeOf( tn ) ){
+    return n;
+  }else{
+    if( tn.isInteger() ){
+      return NodeManager::currentNM()->mkNode( TO_INTEGER, n );
+    }
+    return Node::null();
+  }
+}
+
 bool TermDb::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) {
   if( n==t ){
     return true;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 1b0b72bf9..3e38897d1 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -377,6 +377,8 @@ public:
   bool containsVtsTerm( std::vector< Node >& n, bool isFree = false );
   /** simple check for contains term */
   bool containsVtsInfinity( Node n, bool isFree = false );
+  /** make type */
+  static Node mkNodeType( Node n, TypeNode tn );
 
 private:
   //helper for contains term
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 5706c789e..de3c503b5 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -62,7 +62,9 @@ d_quantEngine( qe ), d_f( f ){
       ++(qe->d_statistics.d_simple_triggers);
     }
   }else{
-    Trace("multi-trigger") << "Multi-trigger " << (*this) << " for " << f << std::endl;
+    Trace("multi-trigger") << "Multi-trigger ";
+    debugPrint("multi-trigger");
+    Trace("multi-trigger") << " for " << f << std::endl;
     //Notice() << "Multi-trigger for " << f << " : " << std::endl;
     //Notice() << "   " << (*this) << std::endl;
     ++(qe->d_statistics.d_multi_triggers);
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index bd4c19dba..1817ebe56 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -120,16 +120,6 @@ public:
   /** get all variables that E-matching can possibly handle */
   static void getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, std::vector< Node >& t_vars );
 
-  inline void toStream(std::ostream& out) const {
-    /*
-    out << "TRIGGER( ";
-    for( int i=0; i<(int)d_nodes.size(); i++ ){
-      if( i>0 ){ out << ", "; }
-      out << d_nodes[i];
-    }
-    out << " )";
-    */
-  }
   void debugPrint( const char * c ) {
     Trace(c) << "TRIGGER( ";
     for( int i=0; i<(int)d_nodes.size(); i++ ){
@@ -140,12 +130,6 @@ public:
   }
 };
 
-inline std::ostream& operator<<(std::ostream& out, const Trigger & tr) {
-  tr.toStream(out);
-  return out;
-}
-
-
 /** a trie of triggers */
 class TriggerTrie {
 private:
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 9ae3b1d40..41e560557 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -696,7 +696,7 @@ void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< No
   }
 }
 
-bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){
+bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){
   Assert( f.getKind()==FORALL );
   Assert( vars.size()==terms.size() );
   Node body = getInstantiation( f, vars, terms );
@@ -920,12 +920,17 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
   Assert( terms.size()==q[0].getNumChildren() );
   Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl;
   for( unsigned i=0; i<terms.size(); i++ ){
-    Trace("inst-add-debug") << "  " << q[0][i] << " -> " << terms[i] << std::endl;
+    Trace("inst-add-debug") << "  " << q[0][i] << " -> " << terms[i];
     //make it representative, this is helpful for recognizing duplication
     if( mkRep ){
       //pick the best possible representative for instantiation, based on past use and simplicity of term
       terms[i] = d_eq_query->getInternalRepresentative( terms[i], q, i );
+    }else{
+      //ensure the type is correct
+      terms[i] = quantifiers::TermDb::mkNodeType( terms[i], q[0][i].getType() );
     }
+    Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
+    Assert( !terms[i].isNull() );
   }
 
   //check based on instantiation level
@@ -974,7 +979,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
 
   //add the instantiation
   Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
-  bool addedInst = addInstantiation( q, d_term_db->d_vars[q], terms, doVts );
+  bool addedInst = addInstantiationInternal( q, d_term_db->d_vars[q], terms, doVts );
   //report the result
   if( addedInst ){
     Trace("inst-add-debug") << " -> Success." << std::endl;
@@ -1276,7 +1281,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
         if( i>0 ) Trace("internal-rep-select") << ", ";
         Trace("internal-rep-select") << eqc[i];
       }
-      Trace("internal-rep-select")  << " } " << std::endl;
+      Trace("internal-rep-select")  << " }, type = " << v_tn << std::endl;
       int r_best_score = -1;
       for( size_t i=0; i<eqc.size(); i++ ){
         int score = getRepScore( eqc[i], f, index, v_tn );
@@ -1299,6 +1304,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
         d_rep_score[ r_best ] = d_reset_count;
       }
       Trace("internal-rep-select") << "...Choose " << r_best << std::endl;
+      Assert( r_best.getType().isSubtypeOf( v_tn ) );
       d_int_rep[v_tn][r] = r_best;
       if( r_best!=a ){
         Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 3aea9356d..572149885 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -289,7 +289,7 @@ private:
   /** compute term vector */
   void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
   /** instantiate f with arguments terms */
-  bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false );
+  bool addInstantiationInternal( Node f, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false );
   /** set instantiation level attr */
   static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level );
   /** flush lemmas */