diff options
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; |