From 68becff3ce3bdf27510c2868c3db67bd44eb137a Mon Sep 17 00:00:00 2001
From: "Hoang M. Le" <hle@informatik.uni-bremen.de>
Date: Wed, 26 Oct 2016 13:45:58 +0200
Subject: move the query creation part into runAndGetCex() (to be consistent
 with runAndGetCexForked())

---
 lib/Solver/MetaSMTSolver.cpp | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

(limited to 'lib/Solver')

diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index 19f11617..022056fe 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -173,15 +173,6 @@ bool MetaSMTSolverImpl<SolverContext>::computeInitialValues(
   TimerStatIncrementer t(stats::queryTime);
   assert(_builder);
 
-  if (!_useForked) {
-    for (ConstraintManager::const_iterator it = query.constraints.begin(),
-                                           ie = query.constraints.end();
-         it != ie; ++it) {
-      // assertion(_meta_solver, _builder->construct(*it));
-      assumption(_meta_solver, _builder->construct(*it));
-    }
-  }
-
   ++stats::queries;
   ++stats::queryCounterexamples;
 
@@ -212,6 +203,12 @@ SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCex(
     const Query &query, const std::vector<const Array *> &objects,
     std::vector<std::vector<unsigned char> > &values, bool &hasSolution) {
 
+  // assume the constraints of the query
+  for (ConstraintManager::const_iterator it = query.constraints.begin(),
+                                           ie = query.constraints.end();
+       it != ie; ++it) {
+    assumption(_meta_solver, _builder->construct(*it));
+  }
   // assume the negation of the query
   assumption(_meta_solver, _builder->construct(Expr::createIsZero(query.expr)));
   hasSolution = solve(_meta_solver);
-- 
cgit 1.4.1