Save exited states' formula

2 files changed, 7 insertions, 1 deletions

diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index 74c33a4c..5df7ad70 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -229,6 +229,9 @@ public:
   /// @ brief The patch number, starting from 1; 0 being the original.
   std::uint64_t patchNo = 0;
 
+  /// @ brief Terminated on exit, awaiting comparison.
+  std::string formula = "";
+
   /// @brief The numbers of times this state has run through Executor::stepInstruction
   std::uint64_t steppedInstructions = 0;
 
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index bc27c5f3..a2c28dee 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -3417,7 +3417,8 @@ void Executor::updateStates(ExecutionState *current) {
     if (it3 != seedMap.end())
       seedMap.erase(it3);
     executionTree->remove(es->executionTreeNode);
-    delete es;
+    if (es->formula.empty())
+      delete es;
   }
   removedStates.clear();
 }
@@ -3809,6 +3810,8 @@ void Executor::terminateStateOnExit(ExecutionState &state) {
         terminationTypeFileExtension(StateTerminationType::Exit).c_str());
 
   interpreterHandler->incPathsCompleted();
+  getConstraintLog(state, state.formula, Interpreter::SMTLIB2);
+  exitStates.insert(&state);
   terminateState(state, StateTerminationType::Exit);
 }