diff options
author | Daniel Dunbar <daniel@zuster.org> | 2009-06-02 17:01:00 +0000 |
---|---|---|
committer | Daniel Dunbar <daniel@zuster.org> | 2009-06-02 17:01:00 +0000 |
commit | 4aea9d3d47e7e47630704fdf6628221fa45f6151 (patch) | |
tree | 5e74319cdcc91f362f6d27bd4befcb5c42131d66 /lib/Solver | |
parent | 1016ee0df2a459881d6f9930f7b72929e8bdc8b8 (diff) | |
download | klee-4aea9d3d47e7e47630704fdf6628221fa45f6151.tar.gz |
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
Diffstat (limited to 'lib/Solver')
-rw-r--r-- | lib/Solver/FastCexSolver.cpp | 4 | ||||
-rw-r--r-- | lib/Solver/Solver.cpp | 6 |
2 files changed, 5 insertions, 5 deletions
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index d2bc27c6..b6f676aa 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -358,11 +358,11 @@ protected: if (index >= cod.size) { return ReadExpr::create(UpdateList(&array, true, 0), - ref<Expr>(index, Expr::Int32)); + ConstantExpr::alloc(index, Expr::Int32)); } else { CexValueData &cvd = cod.values[index]; assert(cvd.min() == cvd.max() && "value is not fixed"); - return ref<Expr>(cvd.min(), Expr::Int8); + return ConstantExpr::alloc(cvd.min(), Expr::Int8); } } diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 2a50ae0c..ae378ac1 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -327,8 +327,8 @@ ValidatingSolver::computeInitialValues(const Query& query, unsigned char value = values[i][j]; bindings.push_back(EqExpr::create(ReadExpr::create(UpdateList(array, true, 0), - ref<Expr>(j, Expr::Int32)), - ref<Expr>(value, Expr::Int8))); + ConstantExpr::alloc(j, Expr::Int32)), + ConstantExpr::alloc(value, Expr::Int8))); } } ConstraintManager tmp(bindings); @@ -439,7 +439,7 @@ char *STPSolverImpl::getConstraintLog(const Query &query) { for (std::vector< ref<Expr> >::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) vc_assertFormula(vc, builder->construct(*it)); - assert(query.expr == ref<Expr>(0, Expr::Bool) && + assert(query.expr == ConstantExpr::alloc(0, Expr::Bool) && "Unexpected expression in query!"); char *buffer; |