From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 7 Mar 2014 15:24:04 +0000 (-0500)
Subject: Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodies;... 
X-Git-Tag: cvc5-1.0.0~7036
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d01269e2d5a02952fbda74dcd9629acfbf23dfd4;p=cvc5.git

Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodies; fix bug 551, improper ITE removal under quantifiers.
---

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index c88fd187d..34a72e106 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -55,8 +55,13 @@ UnknownTypeException::UnknownTypeException(TNode n) throw() :
 /** Is this node constant? (and has that been computed yet?) */
 struct IsConstTag { };
 struct IsConstComputedTag { };
+struct HasBoundVarTag { };
+struct HasBoundVarComputedTag { };
 typedef expr::Attribute<IsConstTag, bool> IsConstAttr;
 typedef expr::Attribute<IsConstComputedTag, bool> IsConstComputedAttr;
+/** Attribute true for expressions with bound variables in them */
+typedef expr::Attribute<HasBoundVarTag, bool> HasBoundVarAttr;
+typedef expr::Attribute<HasBoundVarComputedTag, bool> HasBoundVarComputedAttr;
 
 template <bool ref_count>
 bool NodeTemplate<ref_count>::isConst() const {
@@ -91,7 +96,29 @@ bool NodeTemplate<ref_count>::isConst() const {
   }
 }
 
+template <bool ref_count>
+bool NodeTemplate<ref_count>::hasBoundVar() {
+  assertTNodeNotExpired();
+  if(! getAttribute(HasBoundVarComputedAttr())) {
+    bool hasBv = false;
+    if(getKind() == kind::BOUND_VARIABLE) {
+      hasBv = true;
+    } else {
+      for(iterator i = begin(); i != end() && !hasBv; ++i) {
+        hasBv = (*i).hasBoundVar();
+      }
+    }
+    setAttribute(HasBoundVarAttr(), hasBv);
+    setAttribute(HasBoundVarComputedAttr(), true);
+    Debug("bva") << *this << " has bva : " << getAttribute(HasBoundVarAttr()) << std::endl;
+    return hasBv;
+  }
+  return getAttribute(HasBoundVarAttr());
+}
+
 template bool NodeTemplate<true>::isConst() const;
 template bool NodeTemplate<false>::isConst() const;
+template bool NodeTemplate<true>::hasBoundVar();
+template bool NodeTemplate<false>::hasBoundVar();
 
 }/* CVC4 namespace */
diff --git a/src/expr/node.h b/src/expr/node.h
index 9ada7879c..ba139748e 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -423,6 +423,13 @@ public:
   // bool containsDecision(); // is "atomic"
   // bool properlyContainsDecision(); // maybe not atomic but all children are
 
+  /**
+   * Returns true iff this node contains a bound variable.  This bound
+   * variable may or may not be free.
+   * @return true iff this node contains a bound variable.
+   */
+  bool hasBoundVar();
+
   /**
    * Convert this Node into an Expr using the currently-in-scope
    * manager.  Essentially this is like an "operator Expr()" but we
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1bbc99f09..16528e404 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3999,6 +3999,10 @@ void SmtEngine::checkModel(bool hardFailure) {
       continue;
     }
 
+    // Replace the already-known ITEs (this is important for ground ITEs under quantifiers).
+    n = d_private->d_iteRemover.replace(n);
+    Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n << endl;
+
     // As a last-ditch effort, ask model to simplify it.
     // Presently, this is only an issue for quantifiers, which can have a value
     // but don't show up in our substitution map above.
diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp
index 1b4e096f2..a4af4f26f 100644
--- a/src/theory/ite_utilities.cpp
+++ b/src/theory/ite_utilities.cpp
@@ -28,6 +28,7 @@ namespace CVC4 {
 namespace theory {
 
 namespace ite {
+
 inline static bool isTermITE(TNode e) {
   return (e.getKind() == kind::ITE && !e.getType().isBoolean());
 }
@@ -77,9 +78,7 @@ struct CTIVStackElement {
 
 } /* CVC4::theory::ite */
 
-
-
-ITEUtilities::ITEUtilities(ContainsTermITEVistor* containsVisitor)
+ITEUtilities::ITEUtilities(ContainsTermITEVisitor* containsVisitor)
   : d_containsVisitor(containsVisitor)
   , d_compressor(NULL)
   , d_simplifier(NULL)
@@ -144,11 +143,11 @@ void ITEUtilities::clear(){
 }
 
 /*********************                                                        */
-/* ContainsTermITEVistor
+/* ContainsTermITEVisitor
  */
-ContainsTermITEVistor::ContainsTermITEVistor(): d_cache() {}
-ContainsTermITEVistor::~ContainsTermITEVistor(){}
-bool ContainsTermITEVistor::containsTermITE(TNode e){
+ContainsTermITEVisitor::ContainsTermITEVisitor(): d_cache() {}
+ContainsTermITEVisitor::~ContainsTermITEVisitor(){}
+bool ContainsTermITEVisitor::containsTermITE(TNode e){
   /* throughout execution skip through NOT nodes. */
   e = (e.getKind() == kind::NOT) ? e[0] : e;
   if(ite::triviallyContainsNoTermITEs(e)){ return false; }
@@ -197,7 +196,7 @@ bool ContainsTermITEVistor::containsTermITE(TNode e){
   }
   return foundTermIte;
 }
-void ContainsTermITEVistor::garbageCollect() {
+void ContainsTermITEVisitor::garbageCollect() {
   d_cache.clear();
 }
 
@@ -249,7 +248,7 @@ void IncomingArcCounter::clear() {
 /*********************                                                        */
 /* ITECompressor
  */
-ITECompressor::ITECompressor(ContainsTermITEVistor* contains)
+ITECompressor::ITECompressor(ContainsTermITEVisitor* contains)
   : d_contains(contains)
   , d_assertions(NULL)
   , d_incoming(true, true)
@@ -547,7 +546,7 @@ uint32_t TermITEHeightCounter::termITEHeight(TNode e){
 
 
 
-ITESimplifier::ITESimplifier(ContainsTermITEVistor* contains)
+ITESimplifier::ITESimplifier(ContainsTermITEVisitor* contains)
   : d_containsVisitor(contains)
   , d_termITEHeight()
   , d_constantLeaves()
@@ -1608,6 +1607,5 @@ Node ITECareSimplifier::simplifyWithCare(TNode e)
   return substitute(e, substTable, cache);
 }
 
-
 } /* namespace theory */
 } /* namespace CVC4 */
diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h
index d9e6120aa..7f0986ecb 100644
--- a/src/theory/ite_utilities.h
+++ b/src/theory/ite_utilities.h
@@ -31,7 +31,7 @@
 namespace CVC4 {
 namespace theory {
 
-class ContainsTermITEVistor;
+class ContainsTermITEVisitor;
 class IncomingArcCounter;
 class TermITEHeightCounter;
 class ITECompressor;
@@ -40,7 +40,7 @@ class ITECareSimplifier;
 
 class ITEUtilities {
 public:
-  ITEUtilities(ContainsTermITEVistor* containsVisitor);
+  ITEUtilities(ContainsTermITEVisitor* containsVisitor);
   ~ITEUtilities();
 
   Node simpITE(TNode assertion);
@@ -55,7 +55,7 @@ public:
   void clear();
 
 private:
-  ContainsTermITEVistor* d_containsVisitor;
+  ContainsTermITEVisitor* d_containsVisitor;
   ITECompressor* d_compressor;
   ITESimplifier* d_simplifier;
   ITECareSimplifier* d_careSimp;
@@ -64,10 +64,10 @@ private:
 /**
  * A caching visitor that computes whether a node contains a term ite.
  */
-class ContainsTermITEVistor {
+class ContainsTermITEVisitor {
 public:
-  ContainsTermITEVistor();
-  ~ContainsTermITEVistor();
+  ContainsTermITEVisitor();
+  ~ContainsTermITEVisitor();
 
   /** returns true if a node contains a term ite. */
   bool containsTermITE(TNode n);
@@ -140,7 +140,7 @@ private:
  */
 class ITECompressor {
 public:
-  ITECompressor(ContainsTermITEVistor* contains);
+  ITECompressor(ContainsTermITEVisitor* contains);
   ~ITECompressor();
 
   /* returns false if an assertion is discovered to be equal to false. */
@@ -153,7 +153,7 @@ private:
 
   Node d_true; /* Copy of true. */
   Node d_false; /* Copy of false. */
-  ContainsTermITEVistor* d_contains;
+  ContainsTermITEVisitor* d_contains;
   std::vector<Node>* d_assertions;
   IncomingArcCounter d_incoming;
 
@@ -180,7 +180,7 @@ private:
 
 class ITESimplifier {
 public:
-  ITESimplifier(ContainsTermITEVistor* d_containsVisitor);
+  ITESimplifier(ContainsTermITEVisitor* d_containsVisitor);
   ~ITESimplifier();
 
   Node simpITE(TNode assertion);
@@ -192,7 +192,7 @@ private:
   Node d_true;
   Node d_false;
 
-  ContainsTermITEVistor* d_containsVisitor;
+  ContainsTermITEVisitor* d_containsVisitor;
   inline bool containsTermITE(TNode n) {
     return d_containsVisitor->containsTermITE(n);
   }
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 78f989807..e59874429 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -274,7 +274,7 @@ void BoundedIntegers::registerQuantifier( Node f ) {
       for( unsigned i=0; i<d_set[f].size(); i++) {
         Node v = d_set[f][i];
         Node r = d_range[f][v];
-        if( quantifiers::TermDb::hasBoundVarAttr(r) ){
+        if( r.hasBoundVar() ){
           //introduce a new bound
           Node new_range = NodeManager::currentNM()->mkSkolem( "bir_$$", r.getType(), "bound for term" );
           d_nground_range[f][v] = d_range[f][v];
@@ -384,5 +384,5 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node
 }
 
 bool BoundedIntegers::isGroundRange(Node f, Node v) {
-  return isBoundVar(f,v) && !quantifiers::TermDb::hasBoundVarAttr(getLowerBound(f,v)) && !quantifiers::TermDb::hasBoundVarAttr(getUpperBound(f,v));
+  return isBoundVar(f,v) && !getLowerBound(f,v).hasBoundVar() && !getUpperBound(f,v).hasBoundVar();
 }
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 6d333521b..2967c77c8 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -42,8 +42,6 @@ option clauseSplit --clause-split bool :default false
 #   forall x. P( x ) => f( S( x ) ) = x
 option preSkolemQuant --pre-skolem-quant bool :read-write :default false
  apply skolemization eagerly to bodies of quantified formulas
-option iteRemoveQuant --ite-remove-quant bool :default false
- apply ite removal to bodies of quantifiers
 # Whether to perform agressive miniscoping
 option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
  perform aggressive miniscoping for quantifiers
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index ced4e1997..ae5a35a00 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -128,7 +128,7 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant )
     registerNode( n[1], hasPol, pol, true );
   }else{
     if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=NOT ){
-      if( quantifiers::TermDb::hasBoundVarAttr( n ) ){
+      if( n.hasBoundVar() ){
         //literals
         if( n.getKind()==EQUAL ){
           for( unsigned i=0; i<n.getNumChildren(); i++ ){
@@ -162,7 +162,7 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant )
 
 void QuantInfo::flatten( Node n, bool beneathQuant ) {
   Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;
-  if( quantifiers::TermDb::hasBoundVarAttr( n ) ){
+  if( n.hasBoundVar() ){
     if( d_var_num.find( n )==d_var_num.end() ){
       Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;
       d_var_num[n] = d_vars.size();
@@ -647,7 +647,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){
       d_type = typ_invalid;
     }
   }else{
-    if( quantifiers::TermDb::hasBoundVarAttr( n ) ){
+    if( n.hasBoundVar() ){
       d_type_not = false;
       d_n = n;
       if( d_n.getKind()==NOT ){
@@ -693,7 +693,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){
         //literals
         if( d_n.getKind()==EQUAL ){
           for( unsigned i=0; i<2; i++ ){
-            if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){
+            if( d_n[i].hasBoundVar() ){
               if( !qi->isVar( d_n[i] ) ){
                 Trace("qcf-qregister-debug")  << "ERROR : not var " << d_n[i] << std::endl;
               }else if( d_n[i].getKind()==BOUND_VARIABLE && !beneathQuant ){
@@ -844,7 +844,7 @@ void MatchGen::reset_round( QuantConflictFind * p ) {
     }
   }else if( d_type==typ_eq ){
     for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
-      if( !quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){
+      if( !d_n[i].hasBoundVar() ){
         d_ground_eval[i] = p->evaluateTerm( d_n[i] );
       }
     }
@@ -1904,7 +1904,7 @@ void QuantConflictFind::computeRelevantEqr() {
     eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );
     while( !eqc_i.isFinished() ){
       TNode n = (*eqc_i);
-      if( quantifiers::TermDb::hasBoundVarAttr( n ) ){
+      if( n.hasBoundVar() ){
         std::cout << "BAD TERM IN DB : " << n << std::endl;
         exit( 199 );
       }
@@ -1945,7 +1945,7 @@ void QuantConflictFind::computeRelevantEqr() {
         //    std::cout << n.getKind() << " " << n.getOperator() << " " << n << std::endl;
         //  }
         //}
-        if( !quantifiers::TermDb::hasBoundVarAttr( n ) ){    //temporary
+        if( !n.hasBoundVar() ){    //temporary
 
           bool isRedundant;
           std::map< TNode, std::vector< TNode > >::iterator it_na;
@@ -2095,4 +2095,4 @@ QuantConflictFind::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_partial_inst);
 }
 
-}
\ No newline at end of file
+}
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 39ba3e8af..9a912130f 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -348,28 +348,6 @@ bool TermDb::hasInstConstAttr( Node n ) {
   return !getInstConstAttr(n).isNull();
 }
 
-bool TermDb::hasBoundVarAttr( Node n ) {
-  if( !n.getAttribute(HasBoundVarComputedAttribute()) ){
-    bool hasBv = false;
-    if( n.getKind()==BOUND_VARIABLE ){
-      hasBv = true;
-    }else{
-      for (unsigned i=0; i<n.getNumChildren(); i++) {
-        if( hasBoundVarAttr(n[i]) ){
-          hasBv = true;
-          break;
-        }
-      }
-    }
-    HasBoundVarAttribute hbva;
-    n.setAttribute(hbva, hasBv);
-    HasBoundVarComputedAttribute hbvca;
-    n.setAttribute(hbvca, true);
-    Trace("bva") << n << " has bva : " << n.getAttribute(HasBoundVarAttribute()) << std::endl;
-  }
-  return n.getAttribute(HasBoundVarAttribute());
-}
-
 void TermDb::getBoundVars( Node n, std::vector< Node >& bvs) {
   if (n.getKind()==BOUND_VARIABLE ){
     if ( std::find( bvs.begin(), bvs.end(), n)==bvs.end() ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 860f087dd..66b45be2f 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -60,11 +60,6 @@ typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
 struct ModelBasisArgAttributeId {};
 typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
 
-struct HasBoundVarAttributeId {};
-typedef expr::Attribute<HasBoundVarAttributeId, bool> HasBoundVarAttribute;
-struct HasBoundVarComputedAttributeId {};
-typedef expr::Attribute<HasBoundVarComputedAttributeId, bool> HasBoundVarComputedAttribute;
-
 //for rewrite rules
 struct QRewriteRuleAttributeId {};
 typedef expr::Attribute<QRewriteRuleAttributeId, Node> QRewriteRuleAttribute;
@@ -210,8 +205,6 @@ public:
   static bool hasInstConstAttr( Node n );
 //for bound variables
 public:
-  //does n have bound variables?
-  static bool hasBoundVarAttr( Node n );
   //get bound variables in n
   static void getBoundVars( Node n, std::vector< Node >& bvs);
 //for skolem
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index 0dfea4399..1ceedc688 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -18,7 +18,6 @@
 
 #include "util/ite_removal.h"
 #include "expr/command.h"
-#include "theory/quantifiers/options.h"
 #include "theory/ite_utilities.h"
 
 using namespace CVC4;
@@ -29,7 +28,7 @@ namespace CVC4 {
 RemoveITE::RemoveITE(context::UserContext* u)
   : d_iteCache(u)
 {
-  d_containsVisitor = new theory::ContainsTermITEVistor();
+  d_containsVisitor = new theory::ContainsTermITEVisitor();
 }
 
 RemoveITE::~RemoveITE(){
@@ -40,7 +39,7 @@ void RemoveITE::garbageCollect(){
   d_containsVisitor->garbageCollect();
 }
 
-theory::ContainsTermITEVistor*  RemoveITE::getContainsVisitor(){
+theory::ContainsTermITEVisitor* RemoveITE::getContainsVisitor() {
   return d_containsVisitor;
 }
 
@@ -51,22 +50,20 @@ size_t RemoveITE::collectedCacheSizes() const{
 void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
 {
   for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
-    std::vector<Node> quantVar;
     // Do this in two steps to avoid Node problems(?)
     // Appears related to bug 512, splitting this into two lines
     // fixes the bug on clang on Mac OS
-    Node itesRemoved = run(output[i], output, iteSkolemMap, quantVar);
+    Node itesRemoved = run(output[i], output, iteSkolemMap, false);
     output[i] = itesRemoved;
   }
 }
 
-bool RemoveITE::containsTermITE(TNode e){
+bool RemoveITE::containsTermITE(TNode e) const {
   return d_containsVisitor->containsTermITE(e);
 }
 
 Node RemoveITE::run(TNode node, std::vector<Node>& output,
-                    IteSkolemMap& iteSkolemMap,
-                    std::vector<Node>& quantVar) {
+                    IteSkolemMap& iteSkolemMap, bool inQuant) {
   // Current node
   Debug("ite") << "removeITEs(" << node << ")" << endl;
 
@@ -76,35 +73,28 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
   }
 
   // The result may be cached already
+  std::pair<Node, bool> cacheKey(node, inQuant);
   NodeManager *nodeManager = NodeManager::currentNM();
-  ITECache::const_iterator i = d_iteCache.find(node);
+  ITECache::const_iterator i = d_iteCache.find(cacheKey);
   if(i != d_iteCache.end()) {
     Node cached = (*i).second;
     Debug("ite") << "removeITEs: in-cache: " << cached << endl;
     return cached.isNull() ? Node(node) : cached;
   }
 
+  // Remember that we're inside a quantifier
+  if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+    inQuant = true;
+  }
+
   // If an ITE replace it
   if(node.getKind() == kind::ITE) {
     TypeNode nodeType = node.getType();
-    if(!nodeType.isBoolean()) {
+    if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) {
+Debug("ite") << "CAN REMOVE ITE " << node << " BECAUSE " << inQuant << " " << node.hasBoundVar() << endl;
       Node skolem;
       // Make the skolem to represent the ITE
-      if( quantVar.empty() ){
-        skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
-      }else{
-        //if in the scope of free variables, make a skolem operator
-        vector< TypeNode > argTypes;
-        for( size_t i=0; i<quantVar.size(); i++ ){
-          argTypes.push_back( quantVar[i].getType() );
-        }
-        TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, nodeType );
-        Node op = NodeManager::currentNM()->mkSkolem( "termITEop_$$", typ, "a function variable introduced due to term-level ITE removal" );
-        vector< Node > funcArgs;
-        funcArgs.push_back( op );
-        funcArgs.insert( funcArgs.end(), quantVar.begin(), quantVar.end() );
-        skolem = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs );
-      }
+      skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
 
       // The new assertion
       Node newAssertion =
@@ -113,18 +103,10 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
       Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
 
       // Attach the skolem
-      d_iteCache.insert(node, skolem);
+      d_iteCache.insert(cacheKey, skolem);
 
       // Remove ITEs from the new assertion, rewrite it and push it to the output
-      newAssertion = run(newAssertion, output, iteSkolemMap, quantVar);
-
-      if( !quantVar.empty() ){
-        //if in the scope of free variables, it is a quantified assertion
-        vector< Node > children;
-        children.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, quantVar ) );
-        children.push_back( newAssertion );
-        newAssertion = NodeManager::currentNM()->mkNode( kind::FORALL, children );
-      }
+      newAssertion = run(newAssertion, output, iteSkolemMap, inQuant);
 
       iteSkolemMap[skolem] = output.size();
       output.push_back(newAssertion);
@@ -135,42 +117,66 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
   }
 
   // If not an ITE, go deep
-  if( ( node.getKind() != kind::FORALL || options::iteRemoveQuant() ) &&
-      node.getKind() != kind::EXISTS &&
-      node.getKind() != kind::REWRITE_RULE ) {
-    std::vector< Node > newQuantVar;
-    newQuantVar.insert( newQuantVar.end(), quantVar.begin(), quantVar.end() );
-    if( node.getKind()==kind::FORALL ){
-      for( size_t i=0; i<node[0].getNumChildren(); i++ ){
-        newQuantVar.push_back( node[0][i] );
-      }
-    }
-    vector<Node> newChildren;
-    bool somethingChanged = false;
-    if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
-      newChildren.push_back(node.getOperator());
-    }
-    // Remove the ITEs from the children
-    for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
-      Node newChild = run(*it, output, iteSkolemMap, newQuantVar);
-      somethingChanged |= (newChild != *it);
-      newChildren.push_back(newChild);
-    }
+  vector<Node> newChildren;
+  bool somethingChanged = false;
+  if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+    newChildren.push_back(node.getOperator());
+  }
+  // Remove the ITEs from the children
+  for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
+    Node newChild = run(*it, output, iteSkolemMap, inQuant);
+    somethingChanged |= (newChild != *it);
+    newChildren.push_back(newChild);
+  }
 
-    // If changes, we rewrite
-    if(somethingChanged) {
-      Node cached = nodeManager->mkNode(node.getKind(), newChildren);
-      d_iteCache.insert(node, cached);
-      return cached;
-    } else {
-      d_iteCache.insert(node, Node::null());
-      return node;
-    }
+  // If changes, we rewrite
+  if(somethingChanged) {
+    Node cached = nodeManager->mkNode(node.getKind(), newChildren);
+    d_iteCache.insert(cacheKey, cached);
+    return cached;
   } else {
-    d_iteCache.insert(node, Node::null());
+    d_iteCache.insert(cacheKey, Node::null());
     return node;
   }
 }
 
+Node RemoveITE::replace(TNode node, bool inQuant) const {
+  if(node.isVar() || node.isConst() ||
+     (options::biasedITERemoval() && !containsTermITE(node))){
+    return Node(node);
+  }
+
+  // Check the cache
+  NodeManager *nodeManager = NodeManager::currentNM();
+  ITECache::const_iterator i = d_iteCache.find(make_pair(node, inQuant));
+  if(i != d_iteCache.end()) {
+    Node cached = (*i).second;
+    return cached.isNull() ? Node(node) : cached;
+  }
+
+  // Remember that we're inside a quantifier
+  if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+    inQuant = true;
+  }
+
+  vector<Node> newChildren;
+  bool somethingChanged = false;
+  if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+    newChildren.push_back(node.getOperator());
+  }
+  // Replace in children
+  for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
+    Node newChild = replace(*it, inQuant);
+    somethingChanged |= (newChild != *it);
+    newChildren.push_back(newChild);
+  }
+
+  // If changes, we rewrite
+  if(somethingChanged) {
+    return nodeManager->mkNode(node.getKind(), newChildren);
+  } else {
+    return node;
+  }
+}
 
 }/* CVC4 namespace */
diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h
index c2464636e..de5f83f27 100644
--- a/src/util/ite_removal.h
+++ b/src/util/ite_removal.h
@@ -23,17 +23,19 @@
 #include "util/dump.h"
 #include "context/context.h"
 #include "context/cdinsert_hashmap.h"
+#include "util/hash.h"
+#include "util/bool.h"
 
 namespace CVC4 {
 
 namespace theory {
-class ContainsTermITEVistor;
-}
+  class ContainsTermITEVisitor;
+}/* CVC4::theory namespace */
 
 typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
 
 class RemoveITE {
-  typedef context::CDInsertHashMap<Node, Node, NodeHashFunction> ITECache;
+  typedef context::CDInsertHashMap< std::pair<Node, bool>, Node, PairHashFunction<Node, bool, NodeHashFunction, BoolHashFunction> > ITECache;
   ITECache d_iteCache;
 
 
@@ -59,22 +61,28 @@ public:
    * ite created in conjunction with that skolem variable.
    */
   Node run(TNode node, std::vector<Node>& additionalAssertions,
-           IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar);
+           IteSkolemMap& iteSkolemMap, bool inQuant);
 
-  /** Returns true if e contains a term ite.*/
-  bool containsTermITE(TNode e);
+  /**
+   * Substitute under node using pre-existing cache.  Do not remove
+   * any ITEs not seen during previous runs.
+   */
+  Node replace(TNode node, bool inQuant = false) const;
+
+  /** Returns true if e contains a term ite. */
+  bool containsTermITE(TNode e) const;
 
-  /** Returns the collected size of the caches.*/
+  /** Returns the collected size of the caches. */
   size_t collectedCacheSizes() const;
 
-  /** Garbage collects non-context dependent data-structures.*/
+  /** Garbage collects non-context dependent data-structures. */
   void garbageCollect();
 
-  /** Return the RemoveITE's containsVisitor.*/
-  theory::ContainsTermITEVistor* getContainsVisitor();
+  /** Return the RemoveITE's containsVisitor. */
+  theory::ContainsTermITEVisitor* getContainsVisitor();
 
 private:
-  theory::ContainsTermITEVistor* d_containsVisitor;
+  theory::ContainsTermITEVisitor* d_containsVisitor;
 
 };/* class RemoveTTE */
 
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index e2d6664cd..664958e5a 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -154,7 +154,8 @@ BUG_TESTS = \
 	bug522.smt2 \
 	bug528a.smt2 \
 	bug541.smt2 \
-	bug544.smt2
+	bug544.smt2 \
+	bug548a.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/bug548a.smt2 b/test/regress/regress0/bug548a.smt2
new file mode 100644
index 000000000..12658e507
--- /dev/null
+++ b/test/regress/regress0/bug548a.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --rewrite-divk --tlimit 1000
+; EXPECT: unknown
+(set-logic LIA)
+(declare-fun f (Int) Int)
+
+
+; instantiated version : cvc4 answers sat
+;(assert (= (f 1) (div 1 10)))
+;(assert (= (f 11) (div 11 10)))
+
+; cvc4 answers unsat, should be "sat", cvc4 expected to timeout or answer "unknown"
+(assert (forall ((x Int)) (= (f x) (div x 10))))
+
+(assert (= (f 1) 0))
+(assert (= (f 11) 1))
+
+(check-sat)
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 2633949c8..b9a87231f 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -30,7 +30,8 @@ TESTS =	\
 	german73.smt2 \
 	PUZ001+1.smt2 \
 	refcount24.cvc.smt2 \
-	bug0909.smt2
+	bug0909.smt2 \
+	fmf-bound-int.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/fmf/fmf-bound-int.smt2 b/test/regress/regress0/fmf/fmf-bound-int.smt2
new file mode 100644
index 000000000..fb3106bdf
--- /dev/null
+++ b/test/regress/regress0/fmf/fmf-bound-int.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --finite-model-find --fmf-bound-int
+; EXPECT: sat
+(set-logic UFLIA)
+(declare-fun P (Int Int) Bool)
+(declare-fun Q (Int) Bool)
+(assert (forall ((x Int)) (=> (and (<= 0 x) (<= x (ite (P 0 0) 10 20))) (Q x))))
+(check-sat)
diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am
index 32f8a72ba..b7eac2535 100644
--- a/test/regress/regress0/rewriterules/Makefile.am
+++ b/test/regress/regress0/rewriterules/Makefile.am
@@ -25,7 +25,8 @@ TESTS =	\
 	length_trick.smt2 length_trick2.smt2 length_gen_020.smt2 \
 	datatypes.smt2 datatypes_sat.smt2 set_A_new_fast_tableau-base.smt2 \
 	set_A_new_fast_tableau-base_sat.smt2 relation.smt2 simulate_rewriting.smt2 \
-	reachability_back_to_the_future.smt2 native_arrays.smt2 reachability_bbttf_eT_arrays.smt2
+	reachability_back_to_the_future.smt2 native_arrays.smt2
+# reachability_bbttf_eT_arrays.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 705a7eadb..e82076520 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -32,7 +32,6 @@ TESTS =	\
   fmf001.smt2 \
   fmf002.smt2 \
   type001.smt2 \
-  type002.smt2 \
   type003.smt2 \
   model001.smt2 \
   substr001.smt2 \
@@ -51,8 +50,8 @@ TESTS =	\
 
 FAILING_TESTS =
 
-EXTRA_DIST = $(TESTS)
-
+EXTRA_DIST = $(TESTS) \
+  type002.smt2
 
 # and make sure to distribute it
 EXTRA_DIST +=