diff --git a/klee/include/klee/Executor.h b/klee/include/klee/Executor.h
index 4d8a0bbb..b0be5022 100644
--- a/klee/include/klee/Executor.h
+++ b/klee/include/klee/Executor.h
@@ -125,12 +125,6 @@ class Executor {
     void executeMemoryOperation(ExecutionState &state, bool isWrite, ref<Expr> address,
                                 ref<Expr> value /* undef if read */, KInstruction *target /* undef if write */);
 
-    /// When the fork is complete and state properly updated,
-    /// notify the S2EExecutor, so that it can generate an onFork event.
-    /// Sending notification after the fork completed
-    /// allows plugins to kill states and exit to the CPU loop safely.
-    virtual void notifyFork(ExecutionState &originalState, ref<Expr> &condition, Executor::StatePair &targets) = 0;
-
     const Cell &eval(KInstruction *ki, unsigned index, LLVMExecutionState &state) const;
 
     typedef void (*FunctionHandler)(Executor *executor, ExecutionState *state, KInstruction *target,
@@ -150,17 +144,17 @@ class Executor {
     // keepConditionTrueInCurrentState makes sure original state will have condition equal true.
     // This is useful when forking one state with several different values.
     // NOTE: In concolic mode it will recompute initial values for current state, do not use it for seed state.
-    virtual StatePair fork(ExecutionState &current, const ref<Expr> &condition,
-                           bool keepConditionTrueInCurrentState = false);
-
-    // Unconditional fork
-    virtual StatePair fork(ExecutionState &current);
+    virtual StatePair fork(ExecutionState &current, const ref<Expr> &condition, bool keepConditionTrueInCurrentState,
+                           std::function<void(ExecutionStatePtr, const StatePair &)> onBeforeNotify) = 0;
 
     // remove state from queue and delete
-    virtual void terminateState(ExecutionState &state);
+    virtual void terminateState(ExecutionStatePtr state);
 
     virtual const llvm::Module *setModule(llvm::Module *module);
 
+    static void reexecuteCurrentInstructionInForkedState(ExecutionStatePtr state, const StatePair &sp);
+    static void skipCurrentInstructionInForkedState(ExecutionStatePtr state, const StatePair &sp);
+
     /*** State accessor methods ***/
     size_t getStatesCount() const {
         return m_states.size();
diff --git a/klee/lib/Core/Executor.cpp b/klee/lib/Core/Executor.cpp
index 7dd7e453..360c2315 100644
--- a/klee/lib/Core/Executor.cpp
+++ b/klee/lib/Core/Executor.cpp
@@ -290,124 +290,6 @@ void Executor::initializeGlobals(ExecutionState &state) {
     }
 }
 
-Executor::StatePair Executor::fork(ExecutionState &current, const ref<Expr> &condition_,
-                                   bool keepConditionTrueInCurrentState) {
-    auto condition = current.simplifyExpr(condition_);
-
-    // If we are passed a constant, no need to do anything
-    if (auto ce = dyn_cast<ConstantExpr>(condition)) {
-        if (ce->isTrue()) {
-            return StatePair(&current, nullptr);
-        } else {
-            return StatePair(nullptr, &current);
-        }
-    }
-
-    // Evaluate the expression using the current variable assignment
-    ref<Expr> evalResult = current.concolics()->evaluate(condition);
-    ConstantExpr *ce = dyn_cast<ConstantExpr>(evalResult);
-    check(ce, "Could not evaluate the expression to a constant.");
-    bool conditionIsTrue = ce->isTrue();
-
-    if (current.forkDisabled) {
-        if (conditionIsTrue) {
-            if (!current.addConstraint(condition)) {
-                abort();
-            }
-            return StatePair(&current, nullptr);
-        } else {
-            if (!current.addConstraint(Expr::createIsZero(condition))) {
-                abort();
-            }
-            return StatePair(nullptr, &current);
-        }
-    }
-
-    if (keepConditionTrueInCurrentState && !conditionIsTrue) {
-        // Recompute concrete values to keep condition true in current state
-
-        // Build constraints where condition must be true
-        ConstraintManager tmpConstraints = current.constraints();
-        tmpConstraints.addConstraint(condition);
-
-        if (!current.solve(tmpConstraints, *(current.concolics()))) {
-            // Condition is always false in the current state
-            return StatePair(nullptr, &current);
-        }
-
-        conditionIsTrue = true;
-    }
-
-    // Build constraints for branched state
-    ConstraintManager tmpConstraints = current.constraints();
-    if (conditionIsTrue) {
-        tmpConstraints.addConstraint(Expr::createIsZero(condition));
-    } else {
-        tmpConstraints.addConstraint(condition);
-    }
-
-    AssignmentPtr concolics = Assignment::create(true);
-    if (!current.solve(tmpConstraints, *concolics)) {
-        if (conditionIsTrue) {
-            return StatePair(&current, nullptr);
-        } else {
-            return StatePair(nullptr, &current);
-        }
-    }
-
-    // Branch
-    auto branchedState = current.clone();
-    m_addedStates.insert(branchedState);
-
-    *klee::stats::forks += 1;
-
-    // Update concrete values for the branched state
-    branchedState->setConcolics(concolics);
-
-    // Add constraint to both states
-    if (conditionIsTrue) {
-        if (!current.addConstraint(condition)) {
-            abort();
-        }
-        if (!branchedState->addConstraint(Expr::createIsZero(condition))) {
-            abort();
-        }
-    } else {
-        if (!current.addConstraint(Expr::createIsZero(condition))) {
-            abort();
-        }
-        if (!branchedState->addConstraint(condition)) {
-            abort();
-        }
-    }
-
-    // Classify states
-    ExecutionStatePtr trueState, falseState;
-    if (conditionIsTrue) {
-        trueState = &current;
-        falseState = branchedState;
-    } else {
-        falseState = &current;
-        trueState = branchedState;
-    }
-
-    return StatePair(trueState, falseState);
-}
-
-Executor::StatePair Executor::fork(ExecutionState &current) {
-    if (current.forkDisabled) {
-        return StatePair(&current, nullptr);
-    }
-
-    auto clonedState = current.clone();
-    m_addedStates.insert(clonedState);
-
-    // Deep copy concolics().
-    clonedState->setConcolics(Assignment::create(current.concolics()));
-
-    return StatePair(&current, clonedState);
-}
-
 const Cell &Executor::eval(KInstruction *ki, unsigned index, LLVMExecutionState &state) const {
     assert(index < ki->inst->getNumOperands());
     int vnumber = ki->operands[index];
@@ -702,6 +584,17 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f,
     }
 }
 
+void Executor::reexecuteCurrentInstructionInForkedState(ExecutionStatePtr state, const StatePair &sp) {
+    assert(sp.first == state);
+    if (sp.second) {
+        sp.second->llvm.pc = sp.second->llvm.prevPC;
+    }
+}
+
+void Executor::skipCurrentInstructionInForkedState(ExecutionStatePtr state, const StatePair &sp) {
+    // This is a noop for llvm.
+}
+
 void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     *klee::stats::instructions += 1;
     auto &llvmState = state.llvm;
@@ -771,16 +664,14 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
                 // FIXME: Find a way that we don't have this hidden dependency.
                 assert(bi->getCondition() == bi->getOperand(0) && "Wrong operand index!");
                 ref<Expr> cond = eval(ki, 0, llvmState).value;
-                Executor::StatePair branches = fork(state, cond);
-
-                if (branches.first) {
-                    branches.first->llvm.transferToBasicBlock(bi->getSuccessor(0), bi->getParent());
-                }
-                if (branches.second) {
-                    branches.second->llvm.transferToBasicBlock(bi->getSuccessor(1), bi->getParent());
-                }
-
-                notifyFork(state, cond, branches);
+                fork(state, cond, false, [&](ExecutionStatePtr state, const StatePair &sp) {
+                    if (sp.first) {
+                        sp.first->llvm.transferToBasicBlock(bi->getSuccessor(0), bi->getParent());
+                    }
+                    if (sp.second) {
+                        sp.second->llvm.transferToBasicBlock(bi->getSuccessor(1), bi->getParent());
+                    }
+                });
             }
             break;
         }
@@ -792,12 +683,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
 
             klee::ref<klee::Expr> concreteCond = state.concolics()->evaluate(cond);
             klee::ref<klee::Expr> condition = EqExpr::create(concreteCond, cond);
-            StatePair sp = fork(state, condition);
-            assert(sp.first == &state);
-            if (sp.second) {
-                sp.second->llvm.pc = sp.second->llvm.prevPC;
-            }
-            notifyFork(state, condition, sp);
+            StatePair sp = fork(state, condition, false, reexecuteCurrentInstructionInForkedState);
+
             cond = concreteCond;
 
             if (ConstantExpr *CE = dyn_cast<ConstantExpr>(cond)) {
@@ -1557,15 +1444,15 @@ void Executor::updateStates(ExecutionStatePtr current) {
     m_removedStates.clear();
 }
 
-void Executor::terminateState(ExecutionState &state) {
+void Executor::terminateState(ExecutionStatePtr state) {
     *klee::stats::completedPaths += 1;
 
-    StateSet::iterator it = m_addedStates.find(&state);
+    StateSet::iterator it = m_addedStates.find(state);
     if (it == m_addedStates.end()) {
         // XXX: the following line makes delayed state termination impossible
         // llvmState.pc = llvmState.prevPC;
 
-        m_removedStates.insert(&state);
+        m_removedStates.insert(state);
     } else {
         // never reached searcher, just delete immediately
         m_addedStates.erase(it);
@@ -1600,21 +1487,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target,
 
             klee::ref<klee::Expr> condition = EqExpr::create(concreteArg, arg);
 
-            StatePair sp = fork(state, condition);
-
-            assert(sp.first == &state);
-
-            if (sp.second) {
-                sp.second->llvm.pc = sp.second->llvm.prevPC;
-            }
-
-            KInstIterator savedPc = sp.first->llvm.pc;
-            sp.first->llvm.pc = sp.first->llvm.prevPC;
-
-            // This might throw an exception
-            notifyFork(state, condition, sp);
-
-            sp.first->llvm.pc = savedPc;
+            fork(state, condition, false, reexecuteCurrentInstructionInForkedState);
 
             cas.push_back(concreteArg->getZExtValue());
         }
@@ -1749,15 +1622,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, bool isWrite, ref<E
 
     assert(state.concolics()->evaluate(condition)->isTrue());
 
-    StatePair branches = fork(state, condition);
-
-    assert(branches.first == &state);
-    if (branches.second) {
-        // The forked state will have to re-execute the memory op
-        branches.second->llvm.pc = branches.second->llvm.prevPC;
-    }
-
-    notifyFork(state, condition, branches);
+    fork(state, condition, false, reexecuteCurrentInstructionInForkedState);
 
     if (isa<ConstantExpr>(address)) {
         auto ce = dyn_cast<ConstantExpr>(address)->getZExtValue();
diff --git a/libs2ecore/include/s2e/S2E.h b/libs2ecore/include/s2e/S2E.h
index 75c56c54..afbb8b01 100644
--- a/libs2ecore/include/s2e/S2E.h
+++ b/libs2ecore/include/s2e/S2E.h
@@ -295,7 +295,7 @@ template <class PluginClass> PluginClass *S2E::getPlugin() const {
                                        << ": " << message << "\n";                                                \
             print_stacktrace(s2e_warning_print, "state assertion failed");                                        \
             assert(currentState != nullptr && "state assertion failed, no current state to terminate");           \
-            g_s2e->getExecutor()->terminateState(*currentState, "state assertion failed");                        \
+            g_s2e->getExecutor()->terminateState(currentState, "state assertion failed");                         \
             assert(false && "Unreachable code - current state must be terminated");                               \
         }                                                                                                         \
     } while (0)
diff --git a/libs2ecore/include/s2e/S2EExecutor.h b/libs2ecore/include/s2e/S2EExecutor.h
index ea7465c1..7ca457fb 100644
--- a/libs2ecore/include/s2e/S2EExecutor.h
+++ b/libs2ecore/include/s2e/S2EExecutor.h
@@ -61,8 +61,6 @@ class S2EExecutor : public klee::Executor {
 
     bool m_executeAlwaysKlee;
 
-    bool m_forkProcTerminateCurrentState;
-
     bool m_inLoadBalancing;
 
     struct CPUTimer *m_stateSwitchTimer;
@@ -76,7 +74,8 @@ class S2EExecutor : public klee::Executor {
 
     /** Called on fork, used to trace forks */
     StatePair fork(klee::ExecutionState &current, const klee::ref<klee::Expr> &condition,
-                   bool keepConditionTrueInCurrentState = false);
+                   bool keepConditionTrueInCurrentState,
+                   std::function<void(klee::ExecutionStatePtr, const StatePair &)> onBeforeNotify);
 
     // A special version of fork() which does not take any symbolic condition,
     // so internally it will just work like the regular fork method
@@ -169,16 +168,13 @@ class S2EExecutor : public klee::Executor {
     }
 
     /** Kills the specified state and raises an exception to exit the cpu loop */
-    virtual void terminateState(klee::ExecutionState &state);
+    virtual void terminateState(klee::ExecutionStatePtr state);
 
     /** Kills the specified state and raises an exception to exit the cpu loop */
-    virtual void terminateState(klee::ExecutionState &state, const std::string &message);
+    virtual void terminateState(klee::ExecutionStatePtr state, const std::string &message);
 
     void resetStateSwitchTimer();
 
-    // Should be public because of manual forks in plugins
-    void notifyFork(klee::ExecutionState &originalState, klee::ref<klee::Expr> &condition, StatePair &targets);
-
     /**
      * To be called by plugin code
      */
@@ -216,6 +212,17 @@ class S2EExecutor : public klee::Executor {
     // If `condition` is a nullptr, then no path constraints will be added.
     StatePair doFork(klee::ExecutionState &current, const klee::ref<klee::Expr> &condition,
                      bool keepConditionTrueInCurrentState);
+
+    StatePair unconditionalFork(klee::ExecutionState &current);
+
+    StatePair conditionalFork(klee::ExecutionState &current, const klee::ref<klee::Expr> &condition_,
+                              bool keepConditionTrueInCurrentState);
+
+    /// When the fork is complete and state properly updated,
+    /// notify the S2EExecutor, so that it can generate an onFork event.
+    /// Sending notification after the fork completed
+    /// allows plugins to kill states and exit to the CPU loop safely.
+    void notifyFork(klee::ExecutionState &originalState, const klee::ref<klee::Expr> &condition, StatePair &targets);
 };
 
 } // namespace s2e
diff --git a/libs2ecore/src/FunctionHandlers.cpp b/libs2ecore/src/FunctionHandlers.cpp
index 3f4d60b3..29db15db 100644
--- a/libs2ecore/src/FunctionHandlers.cpp
+++ b/libs2ecore/src/FunctionHandlers.cpp
@@ -98,23 +98,10 @@ void handleForkAndConcretize(Executor *executor, ExecutionState *state, klee::KI
     }
 
     // XXX: may create deep paths!
-    Executor::StatePair sp = s2eExecutor->fork(*state, condition);
-
-    // The condition is always true in the current state
-    //(i.e., expr == concreteAddress holds).
-    assert(sp.first == state);
-
-    // It may happen that the simplifier figures out that
-    // the condition is always true, in which case, no fork is needed.
-    // TODO: find a test case for that
-    if (sp.second) {
-        // Will have to reexecute handleForkAndConcretize in the speculative state
-        sp.second->llvm.pc = sp.second->llvm.prevPC;
-    }
+    Executor::StatePair sp =
+        s2eExecutor->fork(*state, condition, false, S2EExecutor::reexecuteCurrentInstructionInForkedState);
 
     state->llvm.bindLocal(target, concreteAddress);
-
-    s2eExecutor->notifyFork(*state, condition, sp);
 }
 
 static void handleGetValue(klee::Executor *executor, klee::ExecutionState *state, klee::KInstruction *target,
diff --git a/libs2ecore/src/S2EExecutor.cpp b/libs2ecore/src/S2EExecutor.cpp
index 55c41deb..88a2e3a1 100644
--- a/libs2ecore/src/S2EExecutor.cpp
+++ b/libs2ecore/src/S2EExecutor.cpp
@@ -241,7 +241,7 @@ volatile void *tb_function_args[3];
 
 S2EExecutor::S2EExecutor(S2E *s2e, TCGLLVMTranslator *translator)
     : Executor(translator->getContext()), m_s2e(s2e), m_llvmTranslator(translator), m_executeAlwaysKlee(false),
-      m_forkProcTerminateCurrentState(false), m_inLoadBalancing(false) {
+      m_inLoadBalancing(false) {
     m_externalDispatcher = std::make_unique<S2EExternalDispatcher>();
 
     LLVMContext &ctx = m_llvmTranslator->getContext();
@@ -659,7 +659,7 @@ void S2EExecutor::doLoadBalancing() {
     for (auto state : allStates) {
         auto s2estate = static_pointer_cast<S2EExecutionState>(state);
         if (!currentSet.count(s2estate)) {
-            Executor::terminateState(*s2estate);
+            Executor::terminateState(s2estate);
 
             // This is important if we kill the current state
             s2estate->zombify();
@@ -893,18 +893,10 @@ inline bool S2EExecutor::executeInstructions(S2EExecutionState *state, unsigned
             try {
                 executeInstruction(*state, ki);
             } catch (const klee::LLVMExecutorException &e) {
-                terminateState(*state, e.what());
+                terminateState(state, e.what());
             }
 
             updateStates(state);
-
-            // Handle the case where we killed the current state inside processFork
-            if (m_forkProcTerminateCurrentState) {
-                state->regs()->write<int>(CPU_OFFSET(exception_index), EXCP_SE);
-                state->zombify();
-                m_forkProcTerminateCurrentState = false;
-                return true;
-            }
         }
     } catch (CpuExitException &) {
         updateStates(state);
@@ -1190,20 +1182,25 @@ klee::ref<klee::Expr> S2EExecutor::executeFunction(S2EExecutionState *state, con
     return executeFunction(state, function, args);
 }
 
-void S2EExecutor::notifyFork(ExecutionState &originalState, klee::ref<Expr> &condition, Executor::StatePair &targets) {
+void S2EExecutor::notifyFork(ExecutionState &originalState, const klee::ref<Expr> &condition,
+                             Executor::StatePair &targets) {
     if (targets.first == nullptr || targets.second == nullptr) {
         return;
     }
 
-    std::vector<S2EExecutionState *> newStates(2);
-    std::vector<klee::ref<Expr>> newConditions(2);
-
     S2EExecutionState *state = static_cast<S2EExecutionState *>(&originalState);
+
+    std::vector<S2EExecutionState *> newStates(2);
     newStates[0] = static_pointer_cast<S2EExecutionState>(targets.first).get();
     newStates[1] = static_pointer_cast<S2EExecutionState>(targets.second).get();
 
-    newConditions[0] = condition;
-    newConditions[1] = klee::NotExpr::create(condition);
+    std::vector<klee::ref<Expr>> newConditions;
+
+    if (condition) {
+        newConditions.resize(2);
+        newConditions[0] = condition;
+        newConditions[1] = klee::NotExpr::create(condition);
+    }
 
     try {
         m_s2e->getCorePlugin()->onStateFork.emit(state, newStates, newConditions);
@@ -1223,32 +1220,142 @@ Executor::StatePair S2EExecutor::forkAndConcretize(S2EExecutionState *state, kle
     klee::ref<klee::ConstantExpr> concreteValue = state->toConstantSilent(value);
 
     klee::ref<klee::Expr> condition = EqExpr::create(concreteValue, value);
-    Executor::StatePair sp = fork(*state, condition);
-
-    // The condition is always true in the current state
-    //(i.e., value == concreteValue holds).
-    assert(sp.first == state);
-
-    // It may happen that the simplifier figures out that
-    // the condition is always true, in which case, no fork is needed.
-    // TODO: find a test case for that
-    if (sp.second) {
-        // Re-execute the plugin invocation in the other state
-        sp.second->llvm.pc = sp.second->llvm.prevPC;
-    }
-
-    notifyFork(*state, condition, sp);
+    Executor::StatePair sp = fork(*state, condition, false, reexecuteCurrentInstructionInForkedState);
     value_ = concreteValue;
     return sp;
 }
 
 S2EExecutor::StatePair S2EExecutor::fork(ExecutionState &current, const klee::ref<Expr> &condition,
-                                         bool keepConditionTrueInCurrentState) {
-    return doFork(current, condition, keepConditionTrueInCurrentState);
+                                         bool keepConditionTrueInCurrentState,
+                                         std::function<void(ExecutionStatePtr, const StatePair &)> onBeforeNotify) {
+    auto ret = doFork(current, condition, keepConditionTrueInCurrentState);
+    onBeforeNotify(&current, ret);
+    notifyFork(current, condition, ret);
+    return ret;
 }
 
 S2EExecutor::StatePair S2EExecutor::fork(ExecutionState &current) {
-    return doFork(current, nullptr, false);
+    auto ret = doFork(current, nullptr, false);
+    notifyFork(current, nullptr, ret);
+    return ret;
+}
+
+Executor::StatePair S2EExecutor::conditionalFork(ExecutionState &current, const klee::ref<Expr> &condition_,
+                                                 bool keepConditionTrueInCurrentState) {
+    auto condition = current.simplifyExpr(condition_);
+
+    // If we are passed a constant, no need to do anything
+    if (auto ce = dyn_cast<klee::ConstantExpr>(condition)) {
+        if (ce->isTrue()) {
+            return StatePair(&current, nullptr);
+        } else {
+            return StatePair(nullptr, &current);
+        }
+    }
+
+    // Evaluate the expression using the current variable assignment
+    klee::ref<Expr> evalResult = current.concolics()->evaluate(condition);
+    klee::ConstantExpr *ce = dyn_cast<klee::ConstantExpr>(evalResult);
+    check(ce, "Could not evaluate the expression to a constant.");
+    bool conditionIsTrue = ce->isTrue();
+
+    if (current.forkDisabled) {
+        if (conditionIsTrue) {
+            if (!current.addConstraint(condition)) {
+                abort();
+            }
+            return StatePair(&current, nullptr);
+        } else {
+            if (!current.addConstraint(Expr::createIsZero(condition))) {
+                abort();
+            }
+            return StatePair(nullptr, &current);
+        }
+    }
+
+    if (keepConditionTrueInCurrentState && !conditionIsTrue) {
+        // Recompute concrete values to keep condition true in current state
+
+        // Build constraints where condition must be true
+        ConstraintManager tmpConstraints = current.constraints();
+        tmpConstraints.addConstraint(condition);
+
+        if (!current.solve(tmpConstraints, *(current.concolics()))) {
+            // Condition is always false in the current state
+            return StatePair(nullptr, &current);
+        }
+
+        conditionIsTrue = true;
+    }
+
+    // Build constraints for branched state
+    ConstraintManager tmpConstraints = current.constraints();
+    if (conditionIsTrue) {
+        tmpConstraints.addConstraint(Expr::createIsZero(condition));
+    } else {
+        tmpConstraints.addConstraint(condition);
+    }
+
+    AssignmentPtr concolics = Assignment::create(true);
+    if (!current.solve(tmpConstraints, *concolics)) {
+        if (conditionIsTrue) {
+            return StatePair(&current, nullptr);
+        } else {
+            return StatePair(nullptr, &current);
+        }
+    }
+
+    // Branch
+    auto branchedState = current.clone();
+    m_addedStates.insert(branchedState);
+
+    *klee::stats::forks += 1;
+
+    // Update concrete values for the branched state
+    branchedState->setConcolics(concolics);
+
+    // Add constraint to both states
+    if (conditionIsTrue) {
+        if (!current.addConstraint(condition)) {
+            abort();
+        }
+        if (!branchedState->addConstraint(Expr::createIsZero(condition))) {
+            abort();
+        }
+    } else {
+        if (!current.addConstraint(Expr::createIsZero(condition))) {
+            abort();
+        }
+        if (!branchedState->addConstraint(condition)) {
+            abort();
+        }
+    }
+
+    // Classify states
+    ExecutionStatePtr trueState, falseState;
+    if (conditionIsTrue) {
+        trueState = &current;
+        falseState = branchedState;
+    } else {
+        falseState = &current;
+        trueState = branchedState;
+    }
+
+    return StatePair(trueState, falseState);
+}
+
+Executor::StatePair S2EExecutor::unconditionalFork(ExecutionState &current) {
+    if (current.forkDisabled) {
+        return StatePair(&current, nullptr);
+    }
+
+    auto clonedState = current.clone();
+    m_addedStates.insert(clonedState);
+
+    // Deep copy concolics().
+    clonedState->setConcolics(Assignment::create(current.concolics()));
+
+    return StatePair(&current, clonedState);
 }
 
 S2EExecutor::StatePair S2EExecutor::doFork(ExecutionState &current, const klee::ref<Expr> &condition,
@@ -1282,9 +1389,9 @@ S2EExecutor::StatePair S2EExecutor::doFork(ExecutionState &current, const klee::
     }
 
     if (condition) {
-        res = Executor::fork(current, condition, keepConditionTrueInCurrentState);
+        res = conditionalFork(current, condition, keepConditionTrueInCurrentState);
     } else {
-        res = Executor::fork(current);
+        res = unconditionalFork(current);
     }
 
     currentState->forkDisabled = oldForkStatus;
@@ -1349,7 +1456,8 @@ S2EExecutor::StatePair S2EExecutor::doFork(ExecutionState &current, const klee::
 ///
 S2EExecutor::StatePair S2EExecutor::forkCondition(S2EExecutionState *state, klee::ref<Expr> condition,
                                                   bool keepConditionTrueInCurrentState) {
-    S2EExecutor::StatePair sp = fork(*state, condition, keepConditionTrueInCurrentState);
+    S2EExecutor::StatePair sp =
+        fork(*state, condition, keepConditionTrueInCurrentState, skipCurrentInstructionInForkedState);
     notifyFork(*state, condition, sp);
     return sp;
 }
@@ -1394,8 +1502,7 @@ std::vector<ExecutionStatePtr> S2EExecutor::forkValues(S2EExecutionState *state,
             }
         }
 
-        StatePair sp = fork(*state, condition);
-        notifyFork(*state, condition, sp);
+        StatePair sp = fork(*state, condition, false, skipCurrentInstructionInForkedState);
 
         ret.push_back(sp.second);
 
@@ -1458,26 +1565,26 @@ bool S2EExecutor::merge(klee::ExecutionState &_base, klee::ExecutionState &_othe
     return result;
 }
 
-void S2EExecutor::terminateState(klee::ExecutionState &state, const std::string &message) {
-    S2EExecutionState *s2estate = static_cast<S2EExecutionState *>(&state);
-    m_s2e->getInfoStream(s2estate) << "Terminating state: " << message << "\n";
+void S2EExecutor::terminateState(klee::ExecutionStatePtr state, const std::string &message) {
+    auto s2estate = static_pointer_cast<S2EExecutionState>(state);
+    m_s2e->getInfoStream(s2estate.get()) << "Terminating state: " << message << "\n";
     terminateState(state);
 }
 
-void S2EExecutor::terminateState(ExecutionState &s) {
-    S2EExecutionState &state = static_cast<S2EExecutionState &>(s);
+void S2EExecutor::terminateState(ExecutionStatePtr s) {
+    auto state = static_pointer_cast<S2EExecutionState>(s);
 
-    m_s2e->getCorePlugin()->onStateKill.emit(&state);
+    m_s2e->getCorePlugin()->onStateKill.emit(state.get());
 
     Executor::terminateState(state);
-    state.zombify();
+    state->zombify();
 
     g_s2e->getWarningsStream().flush();
     g_s2e->getDebugStream().flush();
 
     // No need for exiting the loop if we kill another state.
-    if (!m_inLoadBalancing && (&state == g_s2e_state)) {
-        state.regs()->write<int>(CPU_OFFSET(exception_index), EXCP_SE);
+    if (!m_inLoadBalancing && (state == g_s2e_state)) {
+        state->regs()->write<int>(CPU_OFFSET(exception_index), EXCP_SE);
         throw CpuExitException();
     }
 }
@@ -1712,7 +1819,7 @@ uint64_t s2e_read_mem_io_vaddr(int masked) {
 }
 
 void s2e_kill_state(const char *message) {
-    g_s2e->getExecutor()->terminateState(*g_s2e_state, message);
+    g_s2e->getExecutor()->terminateState(g_s2e_state, message);
 }
 
 void s2e_print_instructions(bool val) {
diff --git a/libs2eplugins/src/s2e/Plugins/Core/BaseInstructions.cpp b/libs2eplugins/src/s2e/Plugins/Core/BaseInstructions.cpp
index 3d6d33d3..d09f72ca 100644
--- a/libs2eplugins/src/s2e/Plugins/Core/BaseInstructions.cpp
+++ b/libs2eplugins/src/s2e/Plugins/Core/BaseInstructions.cpp
@@ -285,7 +285,7 @@ void BaseInstructions::killState(S2EExecutionState *state) {
     os << "State was terminated by opcode\n"
        << "            message: \"" << message << "\"\n"
        << "            status: " << status;
-    s2e()->getExecutor()->terminateState(*state, os.str());
+    s2e()->getExecutor()->terminateState(state, os.str());
 }
 
 void BaseInstructions::printExpression(S2EExecutionState *state) {
@@ -635,7 +635,7 @@ void BaseInstructions::assumeInternal(S2EExecutionState *state, klee::ref<klee::
     getDebugStream(state) << "Assuming " << boolExpr << "\n";
 
     if (!state->addConstraint(boolExpr, true)) {
-        s2e()->getExecutor()->terminateState(*state, "Tried to add an invalid constraint");
+        s2e()->getExecutor()->terminateState(state, "Tried to add an invalid constraint");
     }
 }
 
diff --git a/libs2eplugins/src/s2e/Plugins/ExecutionTracers/TestCaseGenerator.cpp b/libs2eplugins/src/s2e/Plugins/ExecutionTracers/TestCaseGenerator.cpp
index 3e5fbe39..eb308367 100644
--- a/libs2eplugins/src/s2e/Plugins/ExecutionTracers/TestCaseGenerator.cpp
+++ b/libs2eplugins/src/s2e/Plugins/ExecutionTracers/TestCaseGenerator.cpp
@@ -481,7 +481,7 @@ void TestCaseGenerator::handleAddConcreteFileChunk(S2EExecutionState *state,
     std::string name;
     if (!state->mem()->readString(chunk.name, name)) {
         getWarningsStream() << "could not read file name at address " << hexval(chunk.name) << "\n";
-        s2e()->getExecutor()->terminateState(*state, "TestCaseGenerator call failed");
+        s2e()->getExecutor()->terminateState(state, "TestCaseGenerator call failed");
     }
 
     std::vector<uint8_t> data;
@@ -489,7 +489,7 @@ void TestCaseGenerator::handleAddConcreteFileChunk(S2EExecutionState *state,
 
     if (!state->mem()->read(chunk.data, data.data(), chunk.size)) {
         getWarningsStream() << "could not read chunk data from guest at address " << hexval(chunk.data) << "\n";
-        s2e()->getExecutor()->terminateState(*state, "TestCaseGenerator call failed");
+        s2e()->getExecutor()->terminateState(state, "TestCaseGenerator call failed");
     }
 
     DECLARE_PLUGINSTATE(TestCaseGeneratorState, state);
diff --git a/libs2eplugins/src/s2e/Plugins/Lua/LuaFunctionInstrumentation.cpp b/libs2eplugins/src/s2e/Plugins/Lua/LuaFunctionInstrumentation.cpp
index bda248f9..9cb5644c 100644
--- a/libs2eplugins/src/s2e/Plugins/Lua/LuaFunctionInstrumentation.cpp
+++ b/libs2eplugins/src/s2e/Plugins/Lua/LuaFunctionInstrumentation.cpp
@@ -237,7 +237,7 @@ void LuaFunctionInstrumentation::invokeInstrumentation(S2EExecutionState *state,
     Lunar<LuaFunctionInstrumentationState>::push(L, &luaInstrumentation);
 
     if (entry.paramCount > 0 && state->getPointerSize() == 8) {
-        s2e()->getExecutor()->terminateState(*state, "64-bit support not implemented");
+        s2e()->getExecutor()->terminateState(state, "64-bit support not implemented");
     }
 
     lua_pushboolean(L, isCall);
diff --git a/libs2eplugins/src/s2e/Plugins/Lua/LuaS2EExecutionState.cpp b/libs2eplugins/src/s2e/Plugins/Lua/LuaS2EExecutionState.cpp
index 0cea11ca..2934b092 100644
--- a/libs2eplugins/src/s2e/Plugins/Lua/LuaS2EExecutionState.cpp
+++ b/libs2eplugins/src/s2e/Plugins/Lua/LuaS2EExecutionState.cpp
@@ -87,7 +87,7 @@ int LuaS2EExecutionState::kill(lua_State *L) {
 
     std::stringstream ss;
     ss << "LuaS2EExecutionState: killed status:" << status << " message:" << message;
-    g_s2e->getExecutor()->terminateState(*m_state, ss.str());
+    g_s2e->getExecutor()->terminateState(m_state, ss.str());
 
     return 0;
 }
diff --git a/libs2eplugins/src/s2e/Plugins/Lua/LuaS2EExecutionStateRegisters.cpp b/libs2eplugins/src/s2e/Plugins/Lua/LuaS2EExecutionStateRegisters.cpp
index aa9d527d..68f26385 100644
--- a/libs2eplugins/src/s2e/Plugins/Lua/LuaS2EExecutionStateRegisters.cpp
+++ b/libs2eplugins/src/s2e/Plugins/Lua/LuaS2EExecutionStateRegisters.cpp
@@ -76,7 +76,7 @@ int LuaS2EExecutionStateRegisters::read(lua_State *L) {
                 default: {
                     std::stringstream ss;
                     ss << "LuaS2EExecutionStateRegisters::read: Incorrect size " << size << "\n";
-                    g_s2e->getExecutor()->terminateState(*m_state, ss.str());
+                    g_s2e->getExecutor()->terminateState(m_state, ss.str());
                     break;
                 }
             }
@@ -90,7 +90,7 @@ int LuaS2EExecutionStateRegisters::read(lua_State *L) {
         default: {
             std::stringstream ss;
             ss << "LuaS2EExecutionStateRegisters::read: Incorrect flags " << flags << "\n";
-            g_s2e->getExecutor()->terminateState(*m_state, ss.str());
+            g_s2e->getExecutor()->terminateState(m_state, ss.str());
         }
     }
 
diff --git a/libs2eplugins/src/s2e/Plugins/OSMonitors/Linux/BaseLinuxMonitor.h b/libs2eplugins/src/s2e/Plugins/OSMonitors/Linux/BaseLinuxMonitor.h
index 49e611b7..bfe821c9 100644
--- a/libs2eplugins/src/s2e/Plugins/OSMonitors/Linux/BaseLinuxMonitor.h
+++ b/libs2eplugins/src/s2e/Plugins/OSMonitors/Linux/BaseLinuxMonitor.h
@@ -204,7 +204,7 @@ class BaseLinuxMonitor : public OSMonitor, public IPluginInvoker {
     virtual void handleKernelPanic(S2EExecutionState *state, uint64_t message, uint64_t messageSize) {
         std::string str = "kernel panic";
         state->mem()->readString(message, str, messageSize);
-        g_s2e->getExecutor()->terminateState(*state, str);
+        g_s2e->getExecutor()->terminateState(state, str);
     }
 
     // Get the current process identifier
diff --git a/libs2eplugins/src/s2e/Plugins/OSMonitors/Linux/DecreeMonitor.cpp b/libs2eplugins/src/s2e/Plugins/OSMonitors/Linux/DecreeMonitor.cpp
index 1432f8f4..7361ff87 100644
--- a/libs2eplugins/src/s2e/Plugins/OSMonitors/Linux/DecreeMonitor.cpp
+++ b/libs2eplugins/src/s2e/Plugins/OSMonitors/Linux/DecreeMonitor.cpp
@@ -246,7 +246,7 @@ ref<Expr> DecreeMonitor::makeSymbolicRead(S2EExecutionState *state, uint64_t pid
         return E_CONST(feedCount, Expr::Int32);
     }
 
-    g_s2e->getExecutor()->terminateState(*state, "read data limit exceeded");
+    g_s2e->getExecutor()->terminateState(state, "read data limit exceeded");
     return E_CONST(0, Expr::Int32);
 }
 
diff --git a/libs2eplugins/src/s2e/Plugins/OSMonitors/Linux/LinuxMonitor.cpp b/libs2eplugins/src/s2e/Plugins/OSMonitors/Linux/LinuxMonitor.cpp
index fabe3316..7db939a8 100644
--- a/libs2eplugins/src/s2e/Plugins/OSMonitors/Linux/LinuxMonitor.cpp
+++ b/libs2eplugins/src/s2e/Plugins/OSMonitors/Linux/LinuxMonitor.cpp
@@ -97,7 +97,7 @@ void LinuxMonitor::handleSegfault(S2EExecutionState *state, const S2E_LINUXMON_C
 
     if (m_terminateOnSegfault) {
         getDebugStream(state) << "Terminating state: received segfault\n";
-        s2e()->getExecutor()->terminateState(*state, "Segfault");
+        s2e()->getExecutor()->terminateState(state, "Segfault");
     }
 
     if (m_terminateProcessGroupOnSegfault) {
@@ -140,7 +140,7 @@ void LinuxMonitor::handleTrap(S2EExecutionState *state, const S2E_LINUXMON_COMMA
 
     if (m_terminateOnTrap) {
         getDebugStream(state) << "Terminating state: received trap\n";
-        s2e()->getExecutor()->terminateState(*state, "Trap");
+        s2e()->getExecutor()->terminateState(state, "Trap");
     }
 }
 
diff --git a/libs2eplugins/src/s2e/Plugins/OSMonitors/Windows/BlueScreenInterceptor.cpp b/libs2eplugins/src/s2e/Plugins/OSMonitors/Windows/BlueScreenInterceptor.cpp
index 19b359dd..f19fc6ae 100644
--- a/libs2eplugins/src/s2e/Plugins/OSMonitors/Windows/BlueScreenInterceptor.cpp
+++ b/libs2eplugins/src/s2e/Plugins/OSMonitors/Windows/BlueScreenInterceptor.cpp
@@ -138,7 +138,7 @@ void BlueScreenInterceptor::onBsod(S2EExecutionState *state, uint64_t pc) {
     ss << "BSOD: code=" << hexval(code) << " param1=" << hexval(param1) << " param2=" << hexval(param2)
        << " param3=" << hexval(param3) << " param4=" << hexval(param4);
 
-    s2e()->getExecutor()->terminateState(*state, ss.str());
+    s2e()->getExecutor()->terminateState(state, ss.str());
 }
 
 void BlueScreenInterceptor::handleOpcodeInvocation(S2EExecutionState *state, uint64_t guestDataPtr,
@@ -174,7 +174,7 @@ void BlueScreenInterceptor::handleOpcodeInvocation(S2EExecutionState *state, uin
 
     onBlueScreen.emit(state, &info);
 
-    s2e()->getExecutor()->terminateState(*state, ss.str());
+    s2e()->getExecutor()->terminateState(state, ss.str());
 }
 } // namespace plugins
 } // namespace s2e
diff --git a/libs2eplugins/src/s2e/Plugins/OSMonitors/Windows/WindowsCrashMonitor.cpp b/libs2eplugins/src/s2e/Plugins/OSMonitors/Windows/WindowsCrashMonitor.cpp
index 0e00326b..1dea5e80 100644
--- a/libs2eplugins/src/s2e/Plugins/OSMonitors/Windows/WindowsCrashMonitor.cpp
+++ b/libs2eplugins/src/s2e/Plugins/OSMonitors/Windows/WindowsCrashMonitor.cpp
@@ -101,7 +101,7 @@ void WindowsCrashMonitor::onBlueScreen(S2EExecutionState *state, vmi::windows::B
     onKernelModeCrash.emit(state, *info);
 
     // There is no point of letting the state up at this point, the guest is stuck with a BSOD
-    s2e()->getExecutor()->terminateState(*state, "BSOD");
+    s2e()->getExecutor()->terminateState(state, "BSOD");
 }
 
 /*****************************************************************/
@@ -134,7 +134,7 @@ void WindowsCrashMonitor::opUserModeCrash(S2EExecutionState *state, uint64_t gue
     }
 
     if (m_terminateOnCrash) {
-        s2e()->getExecutor()->terminateState(*state, "User mode crash");
+        s2e()->getExecutor()->terminateState(state, "User mode crash");
     }
 }
 
diff --git a/libs2eplugins/src/s2e/Plugins/OSMonitors/Windows/WindowsMonitor.cpp b/libs2eplugins/src/s2e/Plugins/OSMonitors/Windows/WindowsMonitor.cpp
index 5d6bb6e7..439033fe 100644
--- a/libs2eplugins/src/s2e/Plugins/OSMonitors/Windows/WindowsMonitor.cpp
+++ b/libs2eplugins/src/s2e/Plugins/OSMonitors/Windows/WindowsMonitor.cpp
@@ -462,7 +462,7 @@ template <typename UNICODE_STRING> void WindowsMonitor::unloadModule(S2EExecutio
                     base = state->regs()->read<target_ulong>(CPU_OFFSET(regs[9]));
 
                     if (!state->mem()->read(state->regs()->getSp() + (1 + 4) * pointerSize, &size, pointerSize)) {
-                        s2e()->getExecutor()->terminateState(*state, "WindowsMonitor: could not read stack");
+                        s2e()->getExecutor()->terminateState(state, "WindowsMonitor: could not read stack");
                     }
                 } break;
 
@@ -479,16 +479,16 @@ template <typename UNICODE_STRING> void WindowsMonitor::unloadModule(S2EExecutio
                         pName = state->regs()->read<target_ulong>(CPU_OFFSET(regs[R_EDX]));
 
                         if (!state->mem()->read(state->regs()->getSp() + 1 * pointerSize, &pid, pointerSize)) {
-                            s2e()->getExecutor()->terminateState(*state, "WindowsMonitor: could not read stack");
+                            s2e()->getExecutor()->terminateState(state, "WindowsMonitor: could not read stack");
                         }
                         if (!state->mem()->read(state->regs()->getSp() + 2 * pointerSize, &base, pointerSize)) {
-                            s2e()->getExecutor()->terminateState(*state, "WindowsMonitor: could not read stack");
+                            s2e()->getExecutor()->terminateState(state, "WindowsMonitor: could not read stack");
                         }
                     }
                 } break;
 
                 default:
-                    s2e()->getExecutor()->terminateState(*state,
+                    s2e()->getExecutor()->terminateState(state,
                                                          "WindowsMonitor: unsupported OS for onPerfLogImageUnload");
             }
         } break;
@@ -502,12 +502,12 @@ template <typename UNICODE_STRING> void WindowsMonitor::unloadModule(S2EExecutio
             base = state->regs()->read<target_ulong>(CPU_OFFSET(regs[9]));
 
             if (!state->mem()->read(state->regs()->getSp() + (1 + 4) * pointerSize, &size, pointerSize)) {
-                s2e()->getExecutor()->terminateState(*state, "WindowsMonitor: could not read stack");
+                s2e()->getExecutor()->terminateState(state, "WindowsMonitor: could not read stack");
             }
         } break;
 
         default: {
-            s2e()->getExecutor()->terminateState(*state, "WindowsMonitor: unsupported OS for onPerfLogImageUnload");
+            s2e()->getExecutor()->terminateState(state, "WindowsMonitor: unsupported OS for onPerfLogImageUnload");
             break;
         }
     }
diff --git a/libs2eplugins/src/s2e/Plugins/PathLimiters/EdgeKiller.cpp b/libs2eplugins/src/s2e/Plugins/PathLimiters/EdgeKiller.cpp
index 522501e5..ab244c0c 100644
--- a/libs2eplugins/src/s2e/Plugins/PathLimiters/EdgeKiller.cpp
+++ b/libs2eplugins/src/s2e/Plugins/PathLimiters/EdgeKiller.cpp
@@ -72,7 +72,7 @@ void EdgeKiller::onEdge(S2EExecutionState *state, uint64_t sourcePc, EdgeType ty
     llvm::raw_string_ostream ss(s);
     ss << "EdgeKiller: " << hexval(sourcePc) << " => " << hexval(state->regs()->getPc()) << "\n";
     ss.flush();
-    s2e()->getExecutor()->terminateState(*state, s);
+    s2e()->getExecutor()->terminateState(state, s);
 }
 
 } // namespace plugins
diff --git a/libs2eplugins/src/s2e/Plugins/PathLimiters/ResourceMonitor.cpp b/libs2eplugins/src/s2e/Plugins/PathLimiters/ResourceMonitor.cpp
index a5dff655..0239ebc5 100644
--- a/libs2eplugins/src/s2e/Plugins/PathLimiters/ResourceMonitor.cpp
+++ b/libs2eplugins/src/s2e/Plugins/PathLimiters/ResourceMonitor.cpp
@@ -180,7 +180,7 @@ void ResourceMonitor::dropStates() {
 
             // We might terminate the current state so the executor could throw an exception
             try {
-                executor->terminateState(*state);
+                executor->terminateState(state);
             } catch (s2e::CpuExitException &) {
             }
         }
diff --git a/libs2eplugins/src/s2e/Plugins/Searchers/MergingSearcher.cpp b/libs2eplugins/src/s2e/Plugins/Searchers/MergingSearcher.cpp
index 70e48dfb..0b96aabc 100644
--- a/libs2eplugins/src/s2e/Plugins/Searchers/MergingSearcher.cpp
+++ b/libs2eplugins/src/s2e/Plugins/Searchers/MergingSearcher.cpp
@@ -223,7 +223,7 @@ bool MergingSearcher::mergeEnd(S2EExecutionState *state, bool skipOpcode, bool c
     }
 
     if (success) {
-        g_s2e->getExecutor()->terminateState(*state, "Killed by merge");
+        g_s2e->getExecutor()->terminateState(state, "Killed by merge");
     } else {
         plgState->setGroupId(0);
         getDebugStream(state) << "Merge failed\n";
diff --git a/libs2eplugins/src/s2e/Plugins/VulnerabilityAnalysis/PovGenerationPolicy.cpp b/libs2eplugins/src/s2e/Plugins/VulnerabilityAnalysis/PovGenerationPolicy.cpp
index 078a1c87..453bbc85 100644
--- a/libs2eplugins/src/s2e/Plugins/VulnerabilityAnalysis/PovGenerationPolicy.cpp
+++ b/libs2eplugins/src/s2e/Plugins/VulnerabilityAnalysis/PovGenerationPolicy.cpp
@@ -92,7 +92,7 @@ void PovGenerationPolicy::onSymbolicAddress(S2EExecutionState *state, ref<Expr>
     for (const auto &it : m_uniquePovMap) {
         auto pc = std::get<0>(it.first);
         if (state->regs()->getPc() == pc) {
-            s2e()->getExecutor()->terminateState(*state, "Killing state because that PC has already generated a PoV");
+            s2e()->getExecutor()->terminateState(state, "Killing state because that PC has already generated a PoV");
         }
     }
 }
diff --git a/libs2eplugins/src/s2e/Plugins/VulnerabilityAnalysis/Recipe/Recipe.cpp b/libs2eplugins/src/s2e/Plugins/VulnerabilityAnalysis/Recipe/Recipe.cpp
index 909f1f6c..7df7a6b0 100644
--- a/libs2eplugins/src/s2e/Plugins/VulnerabilityAnalysis/Recipe/Recipe.cpp
+++ b/libs2eplugins/src/s2e/Plugins/VulnerabilityAnalysis/Recipe/Recipe.cpp
@@ -410,7 +410,7 @@ void Recipe::suppressExecutionWithInvalidAddress(S2EExecutionState *state, ref<E
 
         // NOTE: This will produce non replayable crash PoV in case address was valid
         injectSegFault(invalidState);
-        s2e()->getExecutor()->terminateState(*invalidState, "Suppress execution with invalid memory address");
+        s2e()->getExecutor()->terminateState(invalidState, "Suppress execution with invalid memory address");
     }
 }