diff options
Diffstat (limited to 'lib/Core/SeedInfo.cpp')
| -rw-r--r-- | lib/Core/SeedInfo.cpp | 12 |
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); } |