about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/FastCexSolver.cpp4
-rw-r--r--lib/Solver/Solver.cpp6
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;