about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorHoang M. Le <hle@informatik.uni-bremen.de>2016-10-26 13:45:58 +0200
committerHoang M. Le <hle@informatik.uni-bremen.de>2016-10-26 13:45:58 +0200
commit68becff3ce3bdf27510c2868c3db67bd44eb137a (patch)
treecc90013aa4109851d0bebed085f4c99ce94355d0 /lib
parentfafc1ea17a3c9955a4c1cfb49d8d39ecc426457e (diff)
downloadklee-68becff3ce3bdf27510c2868c3db67bd44eb137a.tar.gz
move the query creation part into runAndGetCex() (to be consistent with runAndGetCexForked())
Diffstat (limited to 'lib')
-rw-r--r--lib/Solver/MetaSMTSolver.cpp15
1 files changed, 6 insertions, 9 deletions
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);