Clone state more completely

2 files changed, 5 insertions, 2 deletions

diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index b4af092a..2a754acd 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -109,6 +109,8 @@ ExecutionState::ExecutionState(const ExecutionState& state):
     cexPreferences(state.cexPreferences),
     arrayNames(state.arrayNames),
     openMergeStack(state.openMergeStack),
+    patchNo(state.patchNo),
+    formula(state.formula),
     steppedInstructions(state.steppedInstructions),
     instsSinceCovNew(state.instsSinceCovNew),
     unwindingInformation(state.unwindingInformation
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index b335e566..cfbe7357 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -3893,7 +3893,8 @@ void Executor::terminateStateOnExit(ExecutionState &state) {
 
   interpreterHandler->incPathsCompleted();
   getConstraintLog(state, state.formula, Interpreter::SMTLIB2);
-  searchDifferentiators(&state);
+  if (state.patchNo)
+    searchDifferentiators(&state);
   exitStates.insert(&state);
   terminateState(state, StateTerminationType::Exit);
 }
@@ -4703,7 +4704,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
       assert(std::atoi(name.c_str() + 3) == this->symArgs.size());
       this->symArgs.push_back(mo->size - 1); // string's null termination
     } else if (isSymOut(uniqueName)) {
-      assert(this->symOuts.find(uniqueName) == this->symOuts.end());
+      // assert(this->symOuts.find(uniqueName) == this->symOuts.end());
       this->symOuts[uniqueName] = mo->size;
     }