Use constraint sets and separate metadata for timing solver invocation

Decouple ExecutionState from TimingSolver

Instead of providing an execution state to the timing solver use a set of
constraints and an additional object for metadata.

Fixes:
* correct accounting of metadata to a specific state
* accounting of all solver invocations (e.g. solver-getRange was not
accounted)
* allows to invoke the solver without a state (avoids costly copying of
states/constraints)

12 files changed, 222 insertions, 171 deletions

diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp
index 82913aa7..f3462ca1 100644
--- a/lib/Core/AddressSpace.cpp
+++ b/lib/Core/AddressSpace.cpp
@@ -9,6 +9,7 @@
 
 #include "AddressSpace.h"
 
+#include "ExecutionState.h"
 #include "Memory.h"
 #include "TimingSolver.h"
 
@@ -87,7 +88,7 @@ bool AddressSpace::resolveOne(ExecutionState &state,
     // try cheap search, will succeed for any inbounds pointer
 
     ref<ConstantExpr> cex;
-    if (!solver->getValue(state, address, cex))
+    if (!solver->getValue(state.constraints, address, cex, state.queryMetaData))
       return false;
     uint64_t example = cex->getZExtValue();
     MemoryObject hack(example);
@@ -115,8 +116,9 @@ bool AddressSpace::resolveOne(ExecutionState &state,
       const auto &mo = oi->first;
 
       bool mayBeTrue;
-      if (!solver->mayBeTrue(state, 
-                             mo->getBoundsCheckPointer(address), mayBeTrue))
+      if (!solver->mayBeTrue(state.constraints,
+                             mo->getBoundsCheckPointer(address), mayBeTrue,
+                             state.queryMetaData))
         return false;
       if (mayBeTrue) {
         result.first = oi->first;
@@ -125,9 +127,9 @@ bool AddressSpace::resolveOne(ExecutionState &state,
         return true;
       } else {
         bool mustBeTrue;
-        if (!solver->mustBeTrue(state, 
+        if (!solver->mustBeTrue(state.constraints,
                                 UgeExpr::create(address, mo->getBaseExpr()),
-                                mustBeTrue))
+                                mustBeTrue, state.queryMetaData))
           return false;
         if (mustBeTrue)
           break;
@@ -139,18 +141,18 @@ bool AddressSpace::resolveOne(ExecutionState &state,
       const auto &mo = oi->first;
 
       bool mustBeTrue;
-      if (!solver->mustBeTrue(state, 
+      if (!solver->mustBeTrue(state.constraints,
                               UltExpr::create(address, mo->getBaseExpr()),
-                              mustBeTrue))
+                              mustBeTrue, state.queryMetaData))
         return false;
       if (mustBeTrue) {
         break;
       } else {
         bool mayBeTrue;
 
-        if (!solver->mayBeTrue(state, 
-                               mo->getBoundsCheckPointer(address),
-                               mayBeTrue))
+        if (!solver->mayBeTrue(state.constraints,
+                               mo->getBoundsCheckPointer(address), mayBeTrue,
+                               state.queryMetaData))
           return false;
         if (mayBeTrue) {
           result.first = oi->first;
@@ -176,7 +178,8 @@ int AddressSpace::checkPointerInObject(ExecutionState &state,
   const MemoryObject *mo = op.first;
   ref<Expr> inBounds = mo->getBoundsCheckPointer(p);
   bool mayBeTrue;
-  if (!solver->mayBeTrue(state, inBounds, mayBeTrue)) {
+  if (!solver->mayBeTrue(state.constraints, inBounds, mayBeTrue,
+                         state.queryMetaData)) {
     return 1;
   }
 
@@ -187,7 +190,8 @@ int AddressSpace::checkPointerInObject(ExecutionState &state,
     auto size = rl.size();
     if (size == 1) {
       bool mustBeTrue;
-      if (!solver->mustBeTrue(state, inBounds, mustBeTrue))
+      if (!solver->mustBeTrue(state.constraints, inBounds, mustBeTrue,
+                              state.queryMetaData))
         return 1;
       if (mustBeTrue)
         return 0;
@@ -227,7 +231,7 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
     // just get this by inspection of the expr.
 
     ref<ConstantExpr> cex;
-    if (!solver->getValue(state, p, cex))
+    if (!solver->getValue(state.constraints, p, cex, state.queryMetaData))
       return true;
     uint64_t example = cex->getZExtValue();
     MemoryObject hack(example);
@@ -254,8 +258,9 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
         return incomplete ? true : false;
 
       bool mustBeTrue;
-      if (!solver->mustBeTrue(state, UgeExpr::create(p, mo->getBaseExpr()),
-                              mustBeTrue))
+      if (!solver->mustBeTrue(state.constraints,
+                              UgeExpr::create(p, mo->getBaseExpr()), mustBeTrue,
+                              state.queryMetaData))
         return true;
       if (mustBeTrue)
         break;
@@ -268,8 +273,9 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
         return true;
 
       bool mustBeTrue;
-      if (!solver->mustBeTrue(state, UltExpr::create(p, mo->getBaseExpr()),
-                              mustBeTrue))
+      if (!solver->mustBeTrue(state.constraints,
+                              UltExpr::create(p, mo->getBaseExpr()), mustBeTrue,
+                              state.queryMetaData))
         return true;
       if (mustBeTrue)
         break;
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 0b848f41..5e95ca9b 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -101,7 +101,6 @@ ExecutionState::ExecutionState(const ExecutionState& state):
     depth(state.depth),
     addressSpace(state.addressSpace),
     constraints(state.constraints),
-    queryCost(state.queryCost),
     pathOS(state.pathOS),
     symPathOS(state.symPathOS),
     coveredLines(state.coveredLines),
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index 397b2364..03cad916 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -17,6 +17,7 @@
 #include "klee/Expr/Constraints.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Module/KInstIterator.h"
+#include "klee/Solver/Solver.h"
 #include "klee/System/Time.h"
 
 #include <map>
@@ -96,8 +97,8 @@ public:
 
   /// Statistics and information
 
-  /// @brief Costs for all queries issued for this state, in seconds
-  mutable time::Span queryCost;
+  /// @brief Metadata utilized and collected by solvers for this state
+  mutable SolverQueryMetaData queryMetaData;
 
   /// @brief History of complete path: represents branches taken to
   /// reach/create this state (both concrete and symbolic)
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index ceefc710..041a4e6a 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -915,9 +915,9 @@ void Executor::branch(ExecutionState &state,
       unsigned i;
       for (i=0; i<N; ++i) {
         ref<ConstantExpr> res;
-        bool success = 
-          solver->getValue(state, siit->assignment.evaluate(conditions[i]), 
-                           res);
+        bool success = solver->getValue(
+            state.constraints, siit->assignment.evaluate(conditions[i]), res,
+            state.queryMetaData);
         assert(success && "FIXME: Unhandled solver failure");
         (void) success;
         if (res->isTrue())
@@ -974,8 +974,9 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
         (MaxStaticCPForkPct<1. &&
          cpn && (cpn->statistics.getValue(stats::solverTime) > 
                  stats::solverTime*MaxStaticCPSolvePct))) {
-      ref<ConstantExpr> value; 
-      bool success = solver->getValue(current, condition, value);
+      ref<ConstantExpr> value;
+      bool success = solver->getValue(current.constraints, condition, value,
+                                      current.queryMetaData);
       assert(success && "FIXME: Unhandled solver failure");
       (void) success;
       addConstraint(current, EqExpr::create(value, condition));
@@ -987,7 +988,8 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
   if (isSeeding)
     timeout *= static_cast<unsigned>(it->second.size());
   solver->setTimeout(timeout);
-  bool success = solver->evaluate(current, condition, res);
+  bool success = solver->evaluate(current.constraints, condition, res,
+                                  current.queryMetaData);
   solver->setTimeout(time::Span());
   if (!success) {
     current.pc = current.prevPC;
@@ -1041,8 +1043,9 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
     for (std::vector<SeedInfo>::iterator siit = it->second.begin(), 
            siie = it->second.end(); siit != siie; ++siit) {
       ref<ConstantExpr> res;
-      bool success = 
-        solver->getValue(current, siit->assignment.evaluate(condition), res);
+      bool success = solver->getValue(current.constraints,
+                                      siit->assignment.evaluate(condition), res,
+                                      current.queryMetaData);
       assert(success && "FIXME: Unhandled solver failure");
       (void) success;
       if (res->isTrue()) {
@@ -1102,8 +1105,9 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
       for (std::vector<SeedInfo>::iterator siit = seeds.begin(), 
              siie = seeds.end(); siit != siie; ++siit) {
         ref<ConstantExpr> res;
-        bool success = 
-          solver->getValue(current, siit->assignment.evaluate(condition), res);
+        bool success = solver->getValue(current.constraints,
+                                        siit->assignment.evaluate(condition),
+                                        res, current.queryMetaData);
         assert(success && "FIXME: Unhandled solver failure");
         (void) success;
         if (res->isTrue()) {
@@ -1176,8 +1180,9 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
     for (std::vector<SeedInfo>::iterator siit = it->second.begin(), 
            siie = it->second.end(); siit != siie; ++siit) {
       bool res;
-      bool success = 
-        solver->mustBeFalse(state, siit->assignment.evaluate(condition), res);
+      bool success = solver->mustBeFalse(state.constraints,
+                                         siit->assignment.evaluate(condition),
+                                         res, state.queryMetaData);
       assert(success && "FIXME: Unhandled solver failure");
       (void) success;
       if (res) {
@@ -1233,10 +1238,12 @@ ref<Expr> Executor::toUnique(const ExecutionState &state,
     bool isTrue = false;
     e = optimizer.optimizeExpr(e, true);
     solver->setTimeout(coreSolverTimeout);
-    if (solver->getValue(state, e, value)) {
+    if (solver->getValue(state.constraints, e, value, state.queryMetaData)) {
       ref<Expr> cond = EqExpr::create(e, value);
       cond = optimizer.optimizeExpr(cond, false);
-      if (solver->mustBeTrue(state, cond, isTrue) && isTrue)
+      if (solver->mustBeTrue(state.constraints, cond, isTrue,
+                             state.queryMetaData) &&
+          isTrue)
         result = value;
     }
     solver->setTimeout(time::Span());
@@ -1257,7 +1264,8 @@ Executor::toConstant(ExecutionState &state,
     return CE;
 
   ref<ConstantExpr> value;
-  bool success = solver->getValue(state, e, value);
+  bool success =
+      solver->getValue(state.constraints, e, value, state.queryMetaData);
   assert(success && "FIXME: Unhandled solver failure");
   (void) success;
 
@@ -1286,7 +1294,8 @@ void Executor::executeGetValue(ExecutionState &state,
   if (it==seedMap.end() || isa<ConstantExpr>(e)) {
     ref<ConstantExpr> value;
     e = optimizer.optimizeExpr(e, true);
-    bool success = solver->getValue(state, e, value);
+    bool success =
+        solver->getValue(state.constraints, e, value, state.queryMetaData);
     assert(success && "FIXME: Unhandled solver failure");
     (void) success;
     bindLocal(target, state, value);
@@ -1297,7 +1306,8 @@ void Executor::executeGetValue(ExecutionState &state,
       ref<Expr> cond = siit->assignment.evaluate(e);
       cond = optimizer.optimizeExpr(cond, true);
       ref<ConstantExpr> value;
-      bool success = solver->getValue(state, cond, value);
+      bool success =
+          solver->getValue(state.constraints, cond, value, state.queryMetaData);
       assert(success && "FIXME: Unhandled solver failure");
       (void) success;
       values.insert(value);
@@ -1856,7 +1866,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
 
       // check feasibility
       bool result;
-      bool success __attribute__ ((unused)) = solver->mayBeTrue(state, e, result);
+      bool success __attribute__((unused)) =
+          solver->mayBeTrue(state.constraints, e, result, state.queryMetaData);
       assert(success && "FIXME: Unhandled solver failure");
       if (result) {
         targets.push_back(d);
@@ -1865,7 +1876,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     }
     // check errorCase feasibility
     bool result;
-    bool success __attribute__ ((unused)) = solver->mayBeTrue(state, errorCase, result);
+    bool success __attribute__((unused)) = solver->mayBeTrue(
+        state.constraints, errorCase, result, state.queryMetaData);
     assert(success && "FIXME: Unhandled solver failure");
     if (result) {
       expressions.push_back(errorCase);
@@ -1948,7 +1960,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         // Check if control flow could take this case
         bool result;
         match = optimizer.optimizeExpr(match, false);
-        bool success = solver->mayBeTrue(state, match, result);
+        bool success = solver->mayBeTrue(state.constraints, match, result,
+                                         state.queryMetaData);
         assert(success && "FIXME: Unhandled solver failure");
         (void) success;
         if (result) {
@@ -1976,7 +1989,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       // Check if control could take the default case
       defaultValue = optimizer.optimizeExpr(defaultValue, false);
       bool res;
-      bool success = solver->mayBeTrue(state, defaultValue, res);
+      bool success = solver->mayBeTrue(state.constraints, defaultValue, res,
+                                       state.queryMetaData);
       assert(success && "FIXME: Unhandled solver failure");
       (void) success;
       if (res) {
@@ -2095,7 +2109,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       do {
         v = optimizer.optimizeExpr(v, true);
         ref<ConstantExpr> value;
-        bool success = solver->getValue(*free, v, value);
+        bool success =
+            solver->getValue(free->constraints, v, value, free->queryMetaData);
         assert(success && "FIXME: Unhandled solver failure");
         (void) success;
         StatePair res = fork(*free, EqExpr::create(v, value), true);
@@ -3096,12 +3111,14 @@ std::string Executor::getAddressInfo(ExecutionState &state,
     example = CE->getZExtValue();
   } else {
     ref<ConstantExpr> value;
-    bool success = solver->getValue(state, address, value);
+    bool success = solver->getValue(state.constraints, address, value,
+                                    state.queryMetaData);
     assert(success && "FIXME: Unhandled solver failure");
     (void) success;
     example = value->getZExtValue();
     info << "\texample: " << example << "\n";
-    std::pair< ref<Expr>, ref<Expr> > res = solver->getRange(state, address);
+    std::pair<ref<Expr>, ref<Expr>> res =
+        solver->getRange(state.constraints, address, state.queryMetaData);
     info << "\trange: [" << res.first << ", " << res.second <<"]\n";
   }
   
@@ -3322,7 +3339,8 @@ void Executor::callExternalFunction(ExecutionState &state,
     if (ExternalCalls == ExternalCallPolicy::All) { // don't bother checking uniqueness
       *ai = optimizer.optimizeExpr(*ai, true);
       ref<ConstantExpr> ce;
-      bool success = solver->getValue(state, *ai, ce);
+      bool success =
+          solver->getValue(state.constraints, *ai, ce, state.queryMetaData);
       assert(success && "FIXME: Unhandled solver failure");
       (void) success;
       ce->toMemory(&args[wordIndex]);
@@ -3513,7 +3531,8 @@ void Executor::executeAlloc(ExecutionState &state,
     size = optimizer.optimizeExpr(size, true);
 
     ref<ConstantExpr> example;
-    bool success = solver->getValue(state, size, example);
+    bool success =
+        solver->getValue(state.constraints, size, example, state.queryMetaData);
     assert(success && "FIXME: Unhandled solver failure");
     (void) success;
     
@@ -3522,7 +3541,9 @@ void Executor::executeAlloc(ExecutionState &state,
     while (example->Ugt(ConstantExpr::alloc(128, W))->isTrue()) {
       ref<ConstantExpr> tmp = example->LShr(ConstantExpr::alloc(1, W));
       bool res;
-      bool success = solver->mayBeTrue(state, EqExpr::create(tmp, size), res);
+      bool success =
+          solver->mayBeTrue(state.constraints, EqExpr::create(tmp, size), res,
+                            state.queryMetaData);
       assert(success && "FIXME: Unhandled solver failure");      
       (void) success;
       if (!res)
@@ -3535,13 +3556,14 @@ void Executor::executeAlloc(ExecutionState &state,
     if (fixedSize.second) { 
       // Check for exactly two values
       ref<ConstantExpr> tmp;
-      bool success = solver->getValue(*fixedSize.second, size, tmp);
+      bool success = solver->getValue(fixedSize.second->constraints, size, tmp,
+                                      fixedSize.second->queryMetaData);
       assert(success && "FIXME: Unhandled solver failure");      
       (void) success;
       bool res;
-      success = solver->mustBeTrue(*fixedSize.second, 
-                                   EqExpr::create(tmp, size),
-                                   res);
+      success = solver->mustBeTrue(fixedSize.second->constraints,
+                                   EqExpr::create(tmp, size), res,
+                                   fixedSize.second->queryMetaData);
       assert(success && "FIXME: Unhandled solver failure");      
       (void) success;
       if (res) {
@@ -3681,7 +3703,8 @@ void Executor::executeMemoryOperation(ExecutionState &state,
 
     bool inBounds;
     solver->setTimeout(coreSolverTimeout);
-    bool success = solver->mustBeTrue(state, check, inBounds);
+    bool success = solver->mustBeTrue(state.constraints, check, inBounds,
+                                      state.queryMetaData);
     solver->setTimeout(time::Span());
     if (!success) {
       state.pc = state.prevPC;
@@ -3999,7 +4022,8 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
                                    &res) {
   solver->setTimeout(coreSolverTimeout);
 
-  ExecutionState tmp(state);
+  ConstraintSet extendedConstraints(state.constraints);
+  ConstraintManager cm(extendedConstraints);
 
   // Go through each byte in every test case and attempt to restrict
   // it to the constraints contained in cexPreferences.  (Note:
@@ -4015,8 +4039,9 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
     for (; pi != pie; ++pi) {
       bool mustBeTrue;
       // Attempt to bound byte to constraints held in cexPreferences
-      bool success = solver->mustBeTrue(tmp, Expr::createIsZero(*pi), 
-					mustBeTrue);
+      bool success =
+          solver->mustBeTrue(extendedConstraints, Expr::createIsZero(*pi),
+                             mustBeTrue, state.queryMetaData);
       // If it isn't possible to constrain this particular byte in the desired
       // way (normally this would mean that the byte can't be constrained to
       // be between 0 and 127 without making the entire constraint list UNSAT)
@@ -4024,7 +4049,8 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
       if (!success) break;
       // If the particular constraint operated on in this iteration through
       // the loop isn't implied then add it to the list of constraints.
-      if (!mustBeTrue) tmp.addConstraint(*pi);
+      if (!mustBeTrue)
+        cm.addConstraint(*pi);
     }
     if (pi!=pie) break;
   }
@@ -4033,7 +4059,8 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
   std::vector<const Array*> objects;
   for (unsigned i = 0; i != state.symbolics.size(); ++i)
     objects.push_back(state.symbolics[i].second);
-  bool success = solver->getInitialValues(tmp, objects, values);
+  bool success = solver->getInitialValues(extendedConstraints, objects, values,
+                                          state.queryMetaData);
   solver->setTimeout(time::Span());
   if (!success) {
     klee_warning("unable to compute initial values (invalid constraints?)!");
@@ -4220,7 +4247,7 @@ void Executor::dumpStates() {
 
       *os << "{";
       *os << "'depth' : " << es->depth << ", ";
-      *os << "'queryCost' : " << es->queryCost << ", ";
+      *os << "'queryCost' : " << es->queryMetaData.queryCost << ", ";
       *os << "'coveredNew' : " << es->coveredNew << ", ";
       *os << "'instsSinceCovNew' : " << es->instsSinceCovNew << ", ";
       *os << "'md2u' : " << md2u << ", ";
diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp
deleted file mode 100644
index e69de29b..00000000
--- a/lib/Core/ExecutorTimers.cpp
+++ /dev/null
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index cb40cd81..bf00ee4b 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -10,6 +10,7 @@
 #include "Memory.h"
 
 #include "Context.h"
+#include "ExecutionState.h"
 #include "MemoryManager.h"
 
 #include "klee/ADT/BitArray.h"
@@ -196,7 +197,8 @@ void ObjectState::flushToConcreteStore(TimingSolver *solver,
   for (unsigned i = 0; i < size; i++) {
     if (isByteKnownSymbolic(i)) {
       ref<ConstantExpr> ce;
-      bool success = solver->getValue(state, read8(i), ce);
+      bool success = solver->getValue(state.constraints, read8(i), ce,
+                                      state.queryMetaData);
       if (!success)
         klee_warning("Solver timed out when getting a value for external call, "
                      "byte %p+%u will have random value",
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index 2ab7cd22..e88d5f55 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -26,10 +26,11 @@ namespace llvm {
 
 namespace klee {
 
+class ArrayCache;
 class BitArray;
+class ExecutionState;
 class MemoryManager;
 class Solver;
-class ArrayCache;
 
 class MemoryObject {
   friend class STPBuilder;
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 6b7e9e49..765784c5 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -214,7 +214,9 @@ double WeightedRandomSearcher::getWeight(ExecutionState *es) {
     return inv;
   }
   case QueryCost:
-    return (es->queryCost.toSeconds() < .1) ? 1. : 1./ es->queryCost.toSeconds();
+    return (es->queryMetaData.queryCost.toSeconds() < .1)
+               ? 1.
+               : 1. / es->queryMetaData.queryCost.toSeconds();
   case CoveringNew:
   case MinDistToUncovered: {
     uint64_t md2u = computeMinDistToUncovered(es->pc,
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index d3688313..55f4ed48 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -62,10 +62,9 @@ KTestObject *SeedInfo::getNextInput(const MemoryObject *mo,
 void SeedInfo::patchSeed(const ExecutionState &state, 
                          ref<Expr> condition,
                          TimingSolver *solver) {
-  std::vector< ref<Expr> > required(state.constraints.begin(),
-                                    state.constraints.end());
-  ExecutionState tmp(required);
-  tmp.addConstraint(condition);
+  ConstraintSet required(state.constraints);
+  ConstraintManager cm(required);
+  cm.addConstraint(condition);
 
   // Try and patch direct reads first, this is likely to resolve the
   // problem quickly and avoids long traversal of all seed
@@ -98,26 +97,29 @@ void SeedInfo::patchSeed(const ExecutionState &state,
                                         ConstantExpr::alloc(it2->second[i], 
                                                             Expr::Int8));
       bool res;
-      bool success = solver->mustBeFalse(tmp, isSeed, res);
+      bool success =
+          solver->mustBeFalse(required, isSeed, res, state.queryMetaData);
       assert(success && "FIXME: Unhandled solver failure");
       (void) success;
       if (res) {
         ref<ConstantExpr> value;
-        bool success = solver->getValue(tmp, read, value);
+        bool success =
+            solver->getValue(required, read, value, state.queryMetaData);
         assert(success && "FIXME: Unhandled solver failure");            
         (void) success;
         it2->second[i] = value->getZExtValue(8);
-        tmp.addConstraint(EqExpr::create(read, 
-                                         ConstantExpr::alloc(it2->second[i], 
-                                                             Expr::Int8)));
+        cm.addConstraint(EqExpr::create(
+            read, ConstantExpr::alloc(it2->second[i], Expr::Int8)));
       } else {
-        tmp.addConstraint(isSeed);
+        cm.addConstraint(isSeed);
       }
     }
   }
 
   bool res;
-  bool success = solver->mayBeTrue(state, assignment.evaluate(condition), res);
+  bool success =
+      solver->mayBeTrue(state.constraints, assignment.evaluate(condition), res,
+                        state.queryMetaData);
   assert(success && "FIXME: Unhandled solver failure");
   (void) success;
   if (res)
@@ -135,20 +137,21 @@ void SeedInfo::patchSeed(const ExecutionState &state,
                                         ConstantExpr::alloc(it->second[i], 
                                                             Expr::Int8));
       bool res;
-      bool success = solver->mustBeFalse(tmp, isSeed, res);
+      bool success =
+          solver->mustBeFalse(required, isSeed, res, state.queryMetaData);
       assert(success && "FIXME: Unhandled solver failure");
       (void) success;
       if (res) {
         ref<ConstantExpr> value;
-        bool success = solver->getValue(tmp, read, value);
+        bool success =
+            solver->getValue(required, read, value, state.queryMetaData);
         assert(success && "FIXME: Unhandled solver failure");            
         (void) success;
         it->second[i] = value->getZExtValue(8);
-        tmp.addConstraint(EqExpr::create(read, 
-                                         ConstantExpr::alloc(it->second[i], 
-                                                             Expr::Int8)));
+        cm.addConstraint(EqExpr::create(
+            read, ConstantExpr::alloc(it->second[i], Expr::Int8)));
       } else {
-        tmp.addConstraint(isSeed);
+        cm.addConstraint(isSeed);
       }
     }
   }
@@ -156,8 +159,9 @@ void SeedInfo::patchSeed(const ExecutionState &state,
 #ifndef NDEBUG
   {
     bool res;
-    bool success = 
-      solver->mayBeTrue(state, assignment.evaluate(condition), res);
+    bool success =
+        solver->mayBeTrue(state.constraints, assignment.evaluate(condition),
+                          res, state.queryMetaData);
     assert(success && "FIXME: Unhandled solver failure");            
     (void) success;
     assert(res && "seed patching failed");
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index d6429883..57f059a4 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -249,7 +249,6 @@ SpecialFunctionHandler::readStringAtAddress(ExecutionState &state,
         Executor::TerminateReason::User);
     return "";
   }
-
   const MemoryObject *mo = op.first;
   const ObjectState *os = op.second;
 
@@ -430,7 +429,8 @@ void SpecialFunctionHandler::handleMemalign(ExecutionState &state,
   }
 
   std::pair<ref<Expr>, ref<Expr>> alignmentRangeExpr =
-      executor.solver->getRange(state, arguments[0]);
+      executor.solver->getRange(state.constraints, arguments[0],
+                                state.queryMetaData);
   ref<Expr> alignmentExpr = alignmentRangeExpr.first;
   auto alignmentConstExpr = dyn_cast<ConstantExpr>(alignmentExpr);
 
@@ -464,7 +464,8 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state,
     e = NeExpr::create(e, ConstantExpr::create(0, e->getWidth()));
   
   bool res;
-  bool success __attribute__ ((unused)) = executor.solver->mustBeFalse(state, e, res);
+  bool success __attribute__((unused)) = executor.solver->mustBeFalse(
+      state.constraints, e, res, state.queryMetaData);
   assert(success && "FIXME: Unhandled solver failure");
   if (res) {
     if (SilentKleeAssume) {
@@ -579,19 +580,20 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state,
   if (!isa<ConstantExpr>(arguments[1])) {
     // FIXME: Pull into a unique value method?
     ref<ConstantExpr> value;
-    bool success __attribute__ ((unused)) = executor.solver->getValue(state, arguments[1], value);
+    bool success __attribute__((unused)) = executor.solver->getValue(
+        state.constraints, arguments[1], value, state.queryMetaData);
     assert(success && "FIXME: Unhandled solver failure");
     bool res;
-    success = executor.solver->mustBeTrue(state, 
-                                          EqExpr::create(arguments[1], value), 
-                                          res);
+    success = executor.solver->mustBeTrue(state.constraints,
+                                          EqExpr::create(arguments[1], value),
+                                          res, state.queryMetaData);
     assert(success && "FIXME: Unhandled solver failure");
     if (res) {
       llvm::errs() << " == " << value;
     } else { 
       llvm::errs() << " ~= " << value;
-      std::pair< ref<Expr>, ref<Expr> > res =
-        executor.solver->getRange(state, arguments[1]);
+      std::pair<ref<Expr>, ref<Expr>> res = executor.solver->getRange(
+          state.constraints, arguments[1], state.queryMetaData);
       llvm::errs() << " (in [" << res.first << ", " << res.second <<"])";
     }
   }
@@ -812,12 +814,12 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
 
     // FIXME: Type coercion should be done consistently somewhere.
     bool res;
-    bool success __attribute__ ((unused)) =
-      executor.solver->mustBeTrue(*s, 
-                                  EqExpr::create(ZExtExpr::create(arguments[1],
-                                                                  Context::get().getPointerWidth()),
-                                                 mo->getSizeExpr()),
-                                  res);
+    bool success __attribute__((unused)) = executor.solver->mustBeTrue(
+        s->constraints,
+        EqExpr::create(
+            ZExtExpr::create(arguments[1], Context::get().getPointerWidth()),
+            mo->getSizeExpr()),
+        res, s->queryMetaData);
     assert(success && "FIXME: Unhandled solver failure");
     
     if (res) {
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index cc0afff8..fc31e72d 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -23,8 +23,9 @@ using namespace llvm;
 
 /***/
 
-bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
-                            Solver::Validity &result) {
+bool TimingSolver::evaluate(const ConstraintSet &constraints, ref<Expr> expr,
+                            Solver::Validity &result,
+                            SolverQueryMetaData &metaData) {
   // Fast path, to avoid timer and OS overhead.
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
     result = CE->isTrue() ? Solver::True : Solver::False;
@@ -34,17 +35,17 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
   TimerStatIncrementer timer(stats::solverTime);
 
   if (simplifyExprs)
-    expr = ConstraintManager::simplifyExpr(state.constraints, expr);
+    expr = ConstraintManager::simplifyExpr(constraints, expr);
 
-  bool success = solver->evaluate(Query(state.constraints, expr), result);
+  bool success = solver->evaluate(Query(constraints, expr), result);
 
-  state.queryCost += timer.delta();
+  metaData.queryCost += timer.delta();
 
   return success;
 }
 
-bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr, 
-                              bool &result) {
+bool TimingSolver::mustBeTrue(const ConstraintSet &constraints, ref<Expr> expr,
+                              bool &result, SolverQueryMetaData &metaData) {
   // Fast path, to avoid timer and OS overhead.
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
     result = CE->isTrue() ? true : false;
@@ -54,40 +55,41 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr,
   TimerStatIncrementer timer(stats::solverTime);
 
   if (simplifyExprs)
-    expr = ConstraintManager::simplifyExpr(state.constraints, expr);
+    expr = ConstraintManager::simplifyExpr(constraints, expr);
 
-  bool success = solver->mustBeTrue(Query(state.constraints, expr), result);
+  bool success = solver->mustBeTrue(Query(constraints, expr), result);
 
-  state.queryCost += timer.delta();
+  metaData.queryCost += timer.delta();
 
   return success;
 }
 
-bool TimingSolver::mustBeFalse(const ExecutionState& state, ref<Expr> expr,
-                               bool &result) {
-  return mustBeTrue(state, Expr::createIsZero(expr), result);
+bool TimingSolver::mustBeFalse(const ConstraintSet &constraints, ref<Expr> expr,
+                               bool &result, SolverQueryMetaData &metaData) {
+  return mustBeTrue(constraints, Expr::createIsZero(expr), result, metaData);
 }
 
-bool TimingSolver::mayBeTrue(const ExecutionState& state, ref<Expr> expr, 
-                             bool &result) {
+bool TimingSolver::mayBeTrue(const ConstraintSet &constraints, ref<Expr> expr,
+                             bool &result, SolverQueryMetaData &metaData) {
   bool res;
-  if (!mustBeFalse(state, expr, res))
+  if (!mustBeFalse(constraints, expr, res, metaData))
     return false;
   result = !res;
   return true;
 }
 
-bool TimingSolver::mayBeFalse(const ExecutionState& state, ref<Expr> expr, 
-                              bool &result) {
+bool TimingSolver::mayBeFalse(const ConstraintSet &constraints, ref<Expr> expr,
+                              bool &result, SolverQueryMetaData &metaData) {
   bool res;
-  if (!mustBeTrue(state, expr, res))
+  if (!mustBeTrue(constraints, expr, res, metaData))
     return false;
   result = !res;
   return true;
 }
 
-bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr, 
-                            ref<ConstantExpr> &result) {
+bool TimingSolver::getValue(const ConstraintSet &constraints, ref<Expr> expr,
+                            ref<ConstantExpr> &result,
+                            SolverQueryMetaData &metaData) {
   // Fast path, to avoid timer and OS overhead.
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
     result = CE;
@@ -97,36 +99,37 @@ bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr,
   TimerStatIncrementer timer(stats::solverTime);
 
   if (simplifyExprs)
-    expr = ConstraintManager::simplifyExpr(state.constraints, expr);
+    expr = ConstraintManager::simplifyExpr(constraints, expr);
 
-  bool success = solver->getValue(Query(state.constraints, expr), result);
+  bool success = solver->getValue(Query(constraints, expr), result);
 
-  state.queryCost += timer.delta();
+  metaData.queryCost += timer.delta();
 
   return success;
 }
 
-bool 
-TimingSolver::getInitialValues(const ExecutionState& state, 
-                               const std::vector<const Array*>
-                                 &objects,
-                               std::vector< std::vector<unsigned char> >
-                                 &result) {
+bool TimingSolver::getInitialValues(
+    const ConstraintSet &constraints, const std::vector<const Array *> &objects,
+    std::vector<std::vector<unsigned char>> &result,
+    SolverQueryMetaData &metaData) {
   if (objects.empty())
     return true;
 
   TimerStatIncrementer timer(stats::solverTime);
 
-  bool success = solver->getInitialValues(Query(state.constraints,
-                                                ConstantExpr::alloc(0, Expr::Bool)), 
-                                          objects, result);
-  
-  state.queryCost += timer.delta();
-  
+  bool success = solver->getInitialValues(
+      Query(constraints, ConstantExpr::alloc(0, Expr::Bool)), objects, result);
+
+  metaData.queryCost += timer.delta();
+
   return success;
 }
 
-std::pair< ref<Expr>, ref<Expr> >
-TimingSolver::getRange(const ExecutionState& state, ref<Expr> expr) {
-  return solver->getRange(Query(state.constraints, expr));
+std::pair<ref<Expr>, ref<Expr>>
+TimingSolver::getRange(const ConstraintSet &constraints, ref<Expr> expr,
+                       SolverQueryMetaData &metaData) {
+  TimerStatIncrementer timer(stats::solverTime);
+  auto result = solver->getRange(Query(constraints, expr));
+  metaData.queryCost += timer.delta();
+  return result;
 }
diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
index 9470bd31..1f179e54 100644
--- a/lib/Core/TimingSolver.h
+++ b/lib/Core/TimingSolver.h
@@ -19,54 +19,58 @@
 #include <vector>
 
 namespace klee {
-  class ExecutionState;
-  class Solver;  
-
-  /// TimingSolver - A simple class which wraps a solver and handles
-  /// tracking the statistics that we care about.
-  class TimingSolver {
-  public:
-    std::unique_ptr<Solver> solver;
-    bool simplifyExprs;
-
-  public:
-    /// TimingSolver - Construct a new timing solver.
-    ///
-    /// \param _simplifyExprs - Whether expressions should be
-    /// simplified (via the constraint manager interface) prior to
-    /// querying.
-    TimingSolver(Solver *_solver, bool _simplifyExprs = true) 
+class ConstraintSet;
+class Solver;
+
+/// TimingSolver - A simple class which wraps a solver and handles
+/// tracking the statistics that we care about.
+class TimingSolver {
+public:
+  std::unique_ptr<Solver> solver;
+  bool simplifyExprs;
+
+public:
+  /// TimingSolver - Construct a new timing solver.
+  ///
+  /// \param _simplifyExprs - Whether expressions should be
+  /// simplified (via the constraint manager interface) prior to
+  /// querying.
+  TimingSolver(Solver *_solver, bool _simplifyExprs = true)
       : solver(_solver), simplifyExprs(_simplifyExprs) {}
 
-    void setTimeout(time::Span t) {
-      solver->setCoreSolverTimeout(t);
-    }
-    
-    char *getConstraintLog(const Query& query) {
-      return solver->getConstraintLog(query);
-    }
+  void setTimeout(time::Span t) { solver->setCoreSolverTimeout(t); }
 
-    bool evaluate(const ExecutionState&, ref<Expr>, Solver::Validity &result);
+  char *getConstraintLog(const Query &query) {
+    return solver->getConstraintLog(query);
+  }
 
-    bool mustBeTrue(const ExecutionState&, ref<Expr>, bool &result);
+  bool evaluate(const ConstraintSet &, ref<Expr>, Solver::Validity &result,
+                SolverQueryMetaData &metaData);
 
-    bool mustBeFalse(const ExecutionState&, ref<Expr>, bool &result);
+  bool mustBeTrue(const ConstraintSet &, ref<Expr>, bool &result,
+                  SolverQueryMetaData &metaData);
 
-    bool mayBeTrue(const ExecutionState&, ref<Expr>, bool &result);
+  bool mustBeFalse(const ConstraintSet &, ref<Expr>, bool &result,
+                   SolverQueryMetaData &metaData);
 
-    bool mayBeFalse(const ExecutionState&, ref<Expr>, bool &result);
+  bool mayBeTrue(const ConstraintSet &, ref<Expr>, bool &result,
+                 SolverQueryMetaData &metaData);
 
-    bool getValue(const ExecutionState &, ref<Expr> expr, 
-                  ref<ConstantExpr> &result);
+  bool mayBeFalse(const ConstraintSet &, ref<Expr>, bool &result,
+                  SolverQueryMetaData &metaData);
 
-    bool getInitialValues(const ExecutionState&, 
-                          const std::vector<const Array*> &objects,
-                          std::vector< std::vector<unsigned char> > &result);
+  bool getValue(const ConstraintSet &, ref<Expr> expr,
+                ref<ConstantExpr> &result, SolverQueryMetaData &metaData);
 
-    std::pair< ref<Expr>, ref<Expr> >
-    getRange(const ExecutionState&, ref<Expr> query);
-  };
+  bool getInitialValues(const ConstraintSet &,
+                        const std::vector<const Array *> &objects,
+                        std::vector<std::vector<unsigned char>> &result,
+                        SolverQueryMetaData &metaData);
 
+  std::pair<ref<Expr>, ref<Expr>> getRange(const ConstraintSet &,
+                                           ref<Expr> query,
+                                           SolverQueryMetaData &metaData);
+};
 }
 
 #endif /* KLEE_TIMINGSOLVER_H */