2 files changed, 7 insertions, 1 deletions
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index f81c134c..2ae22284 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 5194aff2..de22d006 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -3346,7 +3346,8 @@ void Executor::updateStates(ExecutionState *current) {
     if (it3 != seedMap.end())
       seedMap.erase(it3);
     processTree->remove(es->ptreeNode);
-    delete es;
+    if (es->formula.empty())
+      delete es;
   }
   removedStates.clear();
 }
@@ -3680,6 +3681,8 @@ void Executor::terminateStateOnExit(ExecutionState &state) {
         terminationTypeFileExtension(StateTerminationType::Exit).c_str());
 
   interpreterHandler->incPathsCompleted();
+  getConstraintLog(state, state.formula, Interpreter::SMTLIB2);
+  exitStates.insert(&state);
   terminateState(state);
 }