Added some BV rewrites, fixed bugs in array theory, made ite simp work with BV

1 files changed, 8 insertions, 11 deletions

diff --git a/src/theory/ite_simplifier.cpp b/src/theory/ite_simplifier.cpp
index 50881af82..7d2b6e333 100644
--- a/src/theory/ite_simplifier.cpp
+++ b/src/theory/ite_simplifier.cpp
@@ -144,19 +144,16 @@ Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVa
 
 Node ITESimplifier::getSimpVar(TypeNode t)
 {
-  if (t.isInteger()) {
-    if (d_simpVarInt.isNull()) {
-      d_simpVarInt = NodeManager::currentNM()->mkVar(t);
-    }
-    return d_simpVarInt;
+  std::hash_map<TypeNode, Node, TypeNode::HashFunction>::iterator it;
+  it = d_simpVars.find(t);
+  if (it != d_simpVars.end()) {
+    return (*it).second;
   }
-  if (t.isReal()) {
-    if (d_simpVarReal.isNull()) {
-      d_simpVarReal = NodeManager::currentNM()->mkVar(t);
-    }
-    return d_simpVarReal;
+  else {
+    Node var = NodeManager::currentNM()->mkVar(t);
+    d_simpVars[t] = var;
+    return var;
   }
-  return Node();
 }