From fafc1ea17a3c9955a4c1cfb49d8d39ecc426457e Mon Sep 17 00:00:00 2001
From: "Hoang M. Le" <hle@informatik.uni-bremen.de>
Date: Wed, 26 Oct 2016 13:34:24 +0200
Subject: change signature of runAndGetCex() to match runAndGetCexForked()

---
 lib/Solver/MetaSMTSolver.cpp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index e1261ad2..19f11617 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -78,7 +78,7 @@ public:
                             bool &hasSolution);
 
   SolverImpl::SolverRunStatus
-  runAndGetCex(ref<Expr> query_expr, const std::vector<const Array *> &objects,
+  runAndGetCex(const Query &query, const std::vector<const Array *> &objects,
                std::vector<std::vector<unsigned char> > &values,
                bool &hasSolution);
 
@@ -192,7 +192,7 @@ bool MetaSMTSolverImpl<SolverContext>::computeInitialValues(
     success = ((SOLVER_RUN_STATUS_SUCCESS_SOLVABLE == _runStatusCode) ||
                (SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE == _runStatusCode));
   } else {
-    _runStatusCode = runAndGetCex(query.expr, objects, values, hasSolution);
+    _runStatusCode = runAndGetCex(query, objects, values, hasSolution);
     success = true;
   }
 
@@ -209,11 +209,11 @@ bool MetaSMTSolverImpl<SolverContext>::computeInitialValues(
 
 template <typename SolverContext>
 SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCex(
-    ref<Expr> query_expr, const std::vector<const Array *> &objects,
+    const Query &query, const std::vector<const Array *> &objects,
     std::vector<std::vector<unsigned char> > &values, bool &hasSolution) {
 
   // assume the negation of the query
-  assumption(_meta_solver, _builder->construct(Expr::createIsZero(query_expr)));
+  assumption(_meta_solver, _builder->construct(Expr::createIsZero(query.expr)));
   hasSolution = solve(_meta_solver);
 
   if (hasSolution) {
-- 
cgit 1.4.1