diff options
| author | Martin Nowack <martin@se.inf.tu-dresden.de> | 2016-03-22 16:39:28 +0100 |
|---|---|---|
| committer | Martin Nowack <martin@se.inf.tu-dresden.de> | 2016-07-08 21:56:28 +0200 |
| commit | f3ff3b06318cae93db4d682e6451ddbca4760328 (patch) | |
| tree | b984df4d0ab09629ef423831f542ff746ff8e34c /lib/Core/Executor.h | |
| parent | 07632e75e21e3c61f1ab46f76618cb1b807bd6c3 (diff) | |
| download | klee-f3ff3b06318cae93db4d682e6451ddbca4760328.tar.gz | |
Use vector instead of set to add/remove states
Deterministic adding/removing of states.
Diffstat (limited to 'lib/Core/Executor.h')
| -rw-r--r-- | lib/Core/Executor.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 99f5921b..92edc364 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -122,12 +122,12 @@ private: /// instructions step. /// \invariant \ref addedStates is a subset of \ref states. /// \invariant \ref addedStates and \ref removedStates are disjoint. - std::set<ExecutionState*> addedStates; + std::vector<ExecutionState *> addedStates; /// Used to track states that have been removed during the current /// instructions step. /// \invariant \ref removedStates is a subset of \ref states. /// \invariant \ref addedStates and \ref removedStates are disjoint. - std::set<ExecutionState*> removedStates; + std::vector<ExecutionState *> removedStates; /// When non-empty the Executor is running in "seed" mode. The /// states in this map will be executed in an arbitrary order |