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)

1 files changed, 2 insertions, 1 deletions

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;