diff options
Diffstat (limited to 'lib/Core/Executor.h')
-rw-r--r-- | lib/Core/Executor.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 1bc91be0..852aaf3c 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -85,6 +85,7 @@ class Executor : public Interpreter { friend class SpecialFunctionHandler; friend class StatsTracker; friend class MergeHandler; + friend class MergingSearcher; public: class Timer { @@ -133,6 +134,12 @@ private: std::vector<TimerInfo*> timers; PTree *processTree; + std::vector<MergeHandler *> mergeGroups; + + // Set of vectors that are currently paused from scheduling because they are + // waiting to be merged in a klee_close_merge instruction + std::set<ExecutionState *> inCloseMerge; + /// Used to track states that have been added during the current /// instructions step. /// \invariant \ref addedStates is a subset of \ref states. |