2 files changed, 22 insertions, 0 deletions
diff --git a/include/klee/util/ExprEvaluator.h b/include/klee/util/ExprEvaluator.h
index be98942d..739e51e6 100644
--- a/include/klee/util/ExprEvaluator.h
+++ b/include/klee/util/ExprEvaluator.h
@@ -18,6 +18,7 @@ namespace klee {
   protected:
     Action evalRead(const UpdateList &ul, unsigned index);
     Action visitRead(const ReadExpr &re);
+    Action visitExpr(const Expr &e);
       
     Action protectedDivOperation(const BinaryExpr &e);
     Action visitUDiv(const UDivExpr &e);
diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp
index ca8f1611..eced0e87 100644
--- a/lib/Expr/ExprEvaluator.cpp
+++ b/lib/Expr/ExprEvaluator.cpp
@@ -33,6 +33,27 @@ ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul,
   return Action::changeTo(getInitialValue(*ul.root, index));
 }
 
+ExprVisitor::Action ExprEvaluator::visitExpr(const Expr &e) {
+  // Evaluate all constant expressions here, in case they weren't folded in
+  // construction. Don't do this for reads though, because we want them to go to
+  // the normal rewrite path.
+  unsigned N = e.getNumKids();
+  if (!N || isa<ReadExpr>(e))
+    return Action::doChildren();
+
+  for (unsigned i = 0; i != N; ++i)
+    if (!isa<ConstantExpr>(e.getKid(i)))
+      return Action::doChildren();
+
+  ref<Expr> Kids[3];
+  for (unsigned i = 0; i != N; ++i) {
+    assert(i < 3);
+    Kids[i] = e.getKid(i);
+  }
+
+  return Action::changeTo(e.rebuild(Kids));
+}
+
 ExprVisitor::Action ExprEvaluator::visitRead(const ReadExpr &re) {
   ref<Expr> v = visit(re.index);