Use ConstantExpr::alloc instead of ref<Expr> directly

 - The "constant optimization" embedded inside ref<Expr> is going away.

 - No functionality change.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72730 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 6 insertions, 6 deletions

diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index e6d88bac..9369dcbc 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -88,12 +88,12 @@ void SeedInfo::patchSeed(const ExecutionState &state,
     const Array *array = it->first;
     unsigned i = it->second;
     ref<Expr> read = ReadExpr::create(UpdateList(array, true, 0),
-                                      ref<Expr>(i, Expr::Int32));
+                                      ConstantExpr::alloc(i, Expr::Int32));
     
     // If not in bindings then this can't be a violation?
     Assignment::bindings_ty::iterator it2 = assignment.bindings.find(array);
     if (it2 != assignment.bindings.end()) {
-      ref<Expr> isSeed = EqExpr::create(read, ref<Expr>(it2->second[i], Expr::Int8));
+      ref<Expr> isSeed = EqExpr::create(read, ConstantExpr::alloc(it2->second[i], Expr::Int8));
       bool res;
       bool success = solver->mustBeFalse(tmp, isSeed, res);
       assert(success && "FIXME: Unhandled solver failure");
@@ -102,7 +102,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
         bool success = solver->getValue(tmp, read, value);
         assert(success && "FIXME: Unhandled solver failure");            
         it2->second[i] = value.getConstantValue();
-        tmp.addConstraint(EqExpr::create(read, ref<Expr>(it2->second[i], Expr::Int8)));
+        tmp.addConstraint(EqExpr::create(read, ConstantExpr::alloc(it2->second[i], Expr::Int8)));
       } else {
         tmp.addConstraint(isSeed);
       }
@@ -122,8 +122,8 @@ void SeedInfo::patchSeed(const ExecutionState &state,
     const Array *array = it->first;
     for (unsigned i=0; i<array->size; ++i) {
       ref<Expr> read = ReadExpr::create(UpdateList(array, true, 0),
-                                        ref<Expr>(i, Expr::Int32));
-      ref<Expr> isSeed = EqExpr::create(read, ref<Expr>(it->second[i], Expr::Int8));
+                                        ConstantExpr::alloc(i, Expr::Int32));
+      ref<Expr> isSeed = EqExpr::create(read, ConstantExpr::alloc(it->second[i], Expr::Int8));
       bool res;
       bool success = solver->mustBeFalse(tmp, isSeed, res);
       assert(success && "FIXME: Unhandled solver failure");
@@ -132,7 +132,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
         bool success = solver->getValue(tmp, read, value);
         assert(success && "FIXME: Unhandled solver failure");            
         it->second[i] = value.getConstantValue();
-        tmp.addConstraint(EqExpr::create(read, ref<Expr>(it->second[i], Expr::Int8)));
+        tmp.addConstraint(EqExpr::create(read, ConstantExpr::alloc(it->second[i], Expr::Int8)));
       } else {
         tmp.addConstraint(isSeed);
       }