Fixed bug causing QF_LIA/solver_cvc4/incorrect1.smt and QF_LIA/solver_cvc4/incorrect3.smt

diff --git a/src/theory/ite_simplifier.cpp b/src/theory/ite_simplifier.cpp
index c70e9be6a7084aa9bfed6b8a27430b207d3180c6..bf031fc946491e28143d7b127f470b8fa4b8905d 100644 (file)
--- a/src/theory/ite_simplifier.cpp
+++ b/src/theory/ite_simplifier.cpp
@@ -369,10 +369,10 @@ Node ITESimplifier::substitute(TNode e, TNodeMap& substTable, TNodeMap& cache)
   }
 
   Node result = builder;
-  it = substTable.find(result);
-  if (it != iend) {
-    result = substitute(it->second, substTable, cache);
-  }
+  // it = substTable.find(result);
+  // if (it != iend) {
+  //   result = substitute(it->second, substTable, cache);
+  // }
   cache[e] = result;
   return result;
 }