diff --git a/include/klee/ADT/KTest.h b/include/klee/ADT/KTest.h
index 6c92e8b62bd..fc6714bd8b3 100644
--- a/include/klee/ADT/KTest.h
+++ b/include/klee/ADT/KTest.h
@@ -65,6 +65,7 @@ int kTest_toFile(const KTest *, const char *path);
 unsigned kTest_numBytes(KTest *);
 
 void kTest_free(KTest *);
+void test_kTest_free(KTest *);
 
 #ifdef __cplusplus
 }
diff --git a/include/klee/Core/BranchTypes.h b/include/klee/Core/BranchTypes.h
index 1c8af978c40..6c3ebc39fc3 100644
--- a/include/klee/Core/BranchTypes.h
+++ b/include/klee/Core/BranchTypes.h
@@ -25,7 +25,8 @@
   BTYPE(Realloc, 8U)                                                           \
   BTYPE(Free, 9U)                                                              \
   BTYPE(GetVal, 10U)                                                           \
-  BMARK(END, 10U)
+  BTYPE(InitialBranch, 11U)                                                    \
+  BMARK(END, 11U)
 /// \endcond
 
 /** @enum BranchType
diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h
index aceb78dcfce..827b8734762 100644
--- a/include/klee/Core/Interpreter.h
+++ b/include/klee/Core/Interpreter.h
@@ -12,6 +12,7 @@
 #include "TerminationTypes.h"
 #include "klee/Module/Annotation.h"
 
+#include "klee/ADT/KTest.h"
 #include "klee/Module/SarifReport.h"
 
 #include <cstdint>
@@ -58,8 +59,11 @@ class InterpreterHandler {
 
   virtual void processTestCase(const ExecutionState &state, const char *message,
                                const char *suffix, bool isError = false) = 0;
-
   virtual ToolJson info() const = 0;
+
+  // used for writing .ktest files
+  virtual int argc() = 0;
+  virtual char **argv() = 0;
 };
 
 /// [File][Line][Column] -> Opcode
@@ -209,10 +213,6 @@ class Interpreter {
   // a user specified path. use null to reset.
   virtual void setReplayPath(const std::vector<bool> *path) = 0;
 
-  // supply a set of symbolic bindings that will be used as "seeds"
-  // for the search. use null to reset.
-  virtual void useSeeds(const std::vector<struct KTest *> *seeds) = 0;
-
   virtual void runFunctionAsMain(llvm::Function *f, int argc, char **argv,
                                  char **envp) = 0;
 
@@ -237,7 +237,10 @@ class Interpreter {
   virtual void getConstraintLog(const ExecutionState &state, std::string &res,
                                 LogType logFormat = STP) = 0;
 
-  virtual bool getSymbolicSolution(const ExecutionState &state, KTest &res) = 0;
+  virtual void getSteppedInstructions(const ExecutionState &state,
+                                      unsigned &res) = 0;
+
+  virtual bool getSymbolicSolution(const ExecutionState &state, KTest *res) = 0;
 
   virtual void addSARIFReport(const ExecutionState &state) = 0;
 
diff --git a/lib/Basic/KTest.cpp b/lib/Basic/KTest.cpp
index 71aaf96c939..59fabdc9983 100644
--- a/lib/Basic/KTest.cpp
+++ b/lib/Basic/KTest.cpp
@@ -9,10 +9,13 @@
 
 #include "klee/ADT/KTest.h"
 
+#include <cassert>
+#include <fstream>
 #include <stdint.h>
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
+#include <string>
 
 #define KTEST_VERSION 4
 #define KTEST_MAGIC_SIZE 5
@@ -295,3 +298,14 @@ void kTest_free(KTest *bo) {
   free(bo->objects);
   free(bo);
 }
+
+void test_kTest_free(KTest *bo) {
+  unsigned i;
+  for (i = 0; i < bo->numObjects; i++) {
+    free(bo->objects[i].name);
+    free(bo->objects[i].bytes);
+    free(bo->objects[i].pointers);
+  }
+  free(bo->objects);
+  free(bo);
+}
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 89957362142..29ac2e0ac26 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -178,7 +178,7 @@ ExecutionState::ExecutionState(const ExecutionState &state)
       gepExprBases(state.gepExprBases), multiplexKF(state.multiplexKF),
       prevTargets_(state.prevTargets_), targets_(state.targets_),
       prevHistory_(state.prevHistory_), history_(state.history_),
-      isTargeted_(state.isTargeted_) {
+      isTargeted_(state.isTargeted_), isSeeded(state.isSeeded) {
   queryMetaData.id = state.id;
 }
 
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index 613c3767628..f0003a67785 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -151,6 +151,9 @@ struct ExecutionStack {
   inline const call_stack_ty &uniqueFrames() const { return uniqueFrames_; }
 
   void forceReturnLocation(const ref<CodeLocation> &location) {
+    if (callStack_.empty()) {
+      llvm::errs() << callStack_.size() << "\n";
+    }
     assert(!callStack_.empty() && "Call stack should contain at least one "
                                   "stack frame to force return location");
     std::optional<ref<CodeLocation>> &callStackReturnLocation =
@@ -300,6 +303,7 @@ class ExecutionState {
 public:
   using stack_ty = ExecutionStack;
 
+  bool isSeeded = false;
   // Execution - Control Flow specific
 
   /// @brief Pointer to initial instruction
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index c6a395731c0..fdc6a19a8da 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -358,12 +358,38 @@ cl::opt<bool> AllExternalWarnings(
 
 /*** Seeding options ***/
 
+cl::opt<bool> RunForever("run-forever",
+                         cl::desc("Store states when out of memory and explore "
+                                  "them later (default=false)"),
+                         cl::init(false), cl::cat(SeedingCat));
+
+cl::opt<bool> StoreSeedsLocally(
+    "store-seeds-locally",
+    cl::desc(
+        "Partialy executed states are stored locally as ktests (default=true)"),
+    cl::init(false), cl::cat(SeedingCat));
+
+cl::opt<bool> PruneAlreadyExecutedStates(
+    "prune-already-executed-states",
+    cl::desc(
+        "Do not explore paths that have already explored seeds (default=true)"),
+    cl::init(false), cl::cat(SeedingCat));
+
+cl::opt<unsigned>
+    UploadAmount("upload-amount",
+                 cl::desc("Amount of seeds that are uploaded every time "
+                          "seeding begins, 0 = upload all (default=0)"),
+                 cl::init(0), cl::cat(SeedingCat));
+
 cl::opt<bool> AlwaysOutputSeeds(
     "always-output-seeds", cl::init(true),
     cl::desc(
         "Dump test cases even if they are driven by seeds only (default=true)"),
     cl::cat(SeedingCat));
 
+cl::opt<bool> PatchSeeds("patch-seeds", cl::desc("Patch seeds (default=false)"),
+                         cl::init(false), cl::cat(SeedingCat));
+
 cl::opt<bool> OnlyReplaySeeds(
     "only-replay-seeds", cl::init(false),
     cl::desc("Discard states that do not have a seed (default=false)."),
@@ -402,6 +428,16 @@ cl::opt<std::string>
                       "search (default=0s (off))"),
              cl::cat(SeedingCat));
 
+cl::list<std::string> SeedOutFile("seed-file",
+                                  cl::desc(".ktest file to be used as seed"),
+                                  cl::cat(SeedingCat));
+
+cl::list<std::string>
+    SeedOutDir("seed-dir",
+               cl::desc("Directory with .ktest files to be used as seeds"),
+               cl::cat(SeedingCat));
+/***/
+
 /*** Debugging options ***/
 
 /// The different query logging solvers that can switched on/off
@@ -516,13 +552,14 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
                                       *targetCalculator)),
       targetedExecutionManager(
           new TargetedExecutionManager(*codeGraphInfo, *targetManager)),
-      replayKTest(0), replayPath(0), usingSeeds(0), atMemoryLimit(false),
+      replayKTest(0), replayPath(0), atMemoryLimit(false),
       inhibitForking(false), coverOnTheFly(false),
       haltExecution(HaltExecution::NotHalt), ivcEnabled(false),
       debugLogBuffer(debugBufferString), sarifReport({}) {
 
   objectManager = std::make_unique<ObjectManager>();
   seedMap = std::make_unique<SeedMap>();
+  storedSeeds = std::make_unique<std::deque<StoredSeed>>();
   objectManager->addSubscriber(seedMap.get());
 
   // Add first entry for single run
@@ -1115,10 +1152,11 @@ void Executor::initializeGlobalObjects(ExecutionState &state) {
 
 bool Executor::branchingPermitted(ExecutionState &state, unsigned N) {
   assert(N);
-  if ((MaxMemoryInhibit && atMemoryLimit) || state.forkDisabled ||
-      inhibitForking || (MaxForks != ~0u && stats::forks >= MaxForks)) {
+  if ((MaxMemoryInhibit && atMemoryLimit && !state.isSeeded) ||
+      state.forkDisabled || inhibitForking ||
+      (MaxForks != ~0u && stats::forks >= MaxForks)) {
 
-    if (MaxMemoryInhibit && atMemoryLimit)
+    if (MaxMemoryInhibit && atMemoryLimit && !state.isSeeded)
       klee_warning_once(0, "skipping fork (memory cap exceeded)");
     else if (state.forkDisabled)
       klee_warning_once(0, "skipping fork (fork disabled on current path)");
@@ -1172,17 +1210,17 @@ void Executor::branch(ExecutionState &state,
   // states if necessary due to OnlyReplaySeeds (inefficient but
   // simple).
 
-  std::map<ExecutionState *, std::vector<SeedInfo>>::iterator it =
+  std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
       seedMap->find(&state);
   if (it != seedMap->end()) {
-    std::vector<SeedInfo> seeds = it->second;
+    std::vector<ExecutingSeed> seeds = it->second;
     seedMap->erase(it);
-
+    objectManager->unseed(it->first);
     // Assume each seed only satisfies one condition (necessarily true
     // when conditions are mutually exclusive and their conjunction is
     // a tautology).
-    for (std::vector<SeedInfo>::iterator siit = seeds.begin(),
-                                         siie = seeds.end();
+    for (std::vector<ExecutingSeed>::iterator siit = seeds.begin(),
+                                              siie = seeds.end();
          siit != siie; ++siit) {
       unsigned i;
       for (i = 0; i < N; ++i) {
@@ -1202,18 +1240,9 @@ void Executor::branch(ExecutionState &state,
         i = theRNG.getInt32() % N;
 
       // Extra check in case we're replaying seeds with a max-fork
-      if (result[i])
+      if (result[i]) {
+        objectManager->seed(result[i]);
         seedMap->at(result[i]).push_back(*siit);
-    }
-
-    if (OnlyReplaySeeds) {
-      for (unsigned i = 0; i < N; ++i) {
-        if (result[i] && !seedMap->count(result[i])) {
-          terminateStateEarlyAlgorithm(*result[i],
-                                       "Unseeded path during replay",
-                                       StateTerminationType::Replay);
-          result[i] = nullptr;
-        }
       }
     }
   }
@@ -1317,46 +1346,102 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
                                    KBlock *ifTrueBlock, KBlock *ifFalseBlock,
                                    BranchType reason) {
   bool isInternal = ifTrueBlock == ifFalseBlock;
-  std::map<ExecutionState *, std::vector<SeedInfo>>::iterator it =
+  std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
       seedMap->find(&current);
   bool isSeeding = it != seedMap->end();
+  PartialValidity res = PartialValidity::None;
 
-  if (!isSeeding)
-    condition = maxStaticPctChecks(current, condition);
-
+  std::vector<ExecutingSeed> trueSeeds;
+  std::vector<ExecutingSeed> falseSeeds;
   time::Span timeout = coreSolverTimeout;
-  if (isSeeding)
-    timeout *= static_cast<unsigned>(it->second.size());
-  solver->setTimeout(timeout);
-
   bool shouldCheckTrueBlock = true, shouldCheckFalseBlock = true;
+
   if (!isInternal) {
     shouldCheckTrueBlock = canReachSomeTargetFromBlock(current, ifTrueBlock);
     shouldCheckFalseBlock = canReachSomeTargetFromBlock(current, ifFalseBlock);
   }
-  PartialValidity res = PartialValidity::None;
+
+  if (!isSeeding) {
+    if (replayPath && !isInternal) {
+      assert(replayPosition < replayPath->size() &&
+             "ran out of branches in replay path mode");
+      bool branch = (*replayPath)[replayPosition++];
+      if (branch) {
+        res = PValidity::MustBeTrue;
+        addConstraint(current, condition);
+      } else {
+        res = PValidity::MustBeFalse;
+        addConstraint(current, Expr::createIsZero(condition));
+      }
+    }
+  } else if (!it->second.empty()) {
+    timeout *= static_cast<unsigned>(it->second.size());
+    for (std::vector<ExecutingSeed>::iterator siit = it->second.begin(),
+                                              siie = it->second.end();
+         siit != siie; ++siit) {
+      if (siit->maxInstructions &&
+          siit->maxInstructions < current.steppedInstructions) {
+        continue;
+      }
+      ref<ConstantExpr> result;
+      bool success = solver->getValue(current.constraints.cs(),
+                                      siit->assignment.evaluate(condition),
+                                      result, current.queryMetaData);
+      assert(success && "FIXME: Unhandled solver failure");
+      (void)success;
+      if (result->isTrue()) {
+        trueSeeds.push_back(*siit);
+      } else if (result->isFalse()) {
+        falseSeeds.push_back(*siit);
+      }
+    }
+    if (!trueSeeds.empty() && falseSeeds.empty()) {
+      if (!shouldCheckFalseBlock) {
+        res = PartialValidity::MustBeTrue;
+      } else {
+        res = PartialValidity::MayBeTrue;
+      }
+    } else if (trueSeeds.empty() && !falseSeeds.empty()) {
+      if (!shouldCheckTrueBlock) {
+        res = PartialValidity::MustBeFalse;
+      } else {
+        res = PartialValidity::MayBeFalse;
+      }
+    } else if (!trueSeeds.empty() && !falseSeeds.empty()) {
+      res = PValidity::TrueOrFalse;
+    }
+  }
+
+  solver->setTimeout(timeout);
   bool terminateEverything = false, success = true;
-  if (!shouldCheckTrueBlock) {
-    bool mayBeFalse = false;
-    if (shouldCheckFalseBlock) {
-      // only solver->check-sat(!condition)
-      success = solver->mayBeFalse(current.constraints.cs(), condition,
-                                   mayBeFalse, current.queryMetaData);
-    }
-    if (!success || !mayBeFalse)
-      terminateEverything = true;
-    else
-      res = PartialValidity::MayBeFalse;
-  } else if (!shouldCheckFalseBlock) {
-    // only solver->check-sat(condition)
-    bool mayBeTrue;
-    success = solver->mayBeTrue(current.constraints.cs(), condition, mayBeTrue,
-                                current.queryMetaData);
-    if (!success || !mayBeTrue)
-      terminateEverything = true;
-    else
-      res = PartialValidity::MayBeTrue;
+
+  if (res == PartialValidity::None) {
+    success = true;
+    condition = maxStaticPctChecks(current, condition);
+
+    if (!shouldCheckTrueBlock) {
+      bool mayBeFalse = false;
+      if (shouldCheckFalseBlock) {
+        // only solver->check-sat(!condition)
+        success = solver->mayBeFalse(current.constraints.cs(), condition,
+                                     mayBeFalse, current.queryMetaData);
+      }
+      if (!success || !mayBeFalse)
+        terminateEverything = true;
+      else
+        res = PartialValidity::MayBeFalse;
+    } else if (!shouldCheckFalseBlock) {
+      // only solver->check-sat(condition)
+      bool mayBeTrue;
+      success = solver->mayBeTrue(current.constraints.cs(), condition,
+                                  mayBeTrue, current.queryMetaData);
+      if (!success || !mayBeTrue)
+        terminateEverything = true;
+      else
+        res = PartialValidity::MayBeTrue;
+    }
   }
+
   if (terminateEverything) {
     current.pc = current.prevPC;
     terminateStateEarlyAlgorithm(current, "State missed all it's targets.",
@@ -1376,70 +1461,17 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
     return StatePair(nullptr, nullptr);
   }
 
-  if (!isSeeding) {
-    if (replayPath && !isInternal) {
-      assert(replayPosition < replayPath->size() &&
-             "ran out of branches in replay path mode");
-      bool branch = (*replayPath)[replayPosition++];
-
-      if (res == PValidity::MustBeTrue) {
-        assert(branch && "hit invalid branch in replay path mode");
-      } else if (res == PValidity::MustBeFalse) {
-        assert(!branch && "hit invalid branch in replay path mode");
-      } else {
-        // add constraints
-        if (branch) {
-          res = PValidity::MustBeTrue;
-          addConstraint(current, condition);
-        } else {
-          res = PValidity::MustBeFalse;
-          addConstraint(current, Expr::createIsZero(condition));
-        }
-      }
-    } else if (res == PValidity::TrueOrFalse) {
-      assert(!replayKTest && "in replay mode, only one branch can be true.");
-
-      if (!branchingPermitted(current, 2)) {
-        TimerStatIncrementer timer(stats::forkTime);
-        if (theRNG.getBool()) {
-          res = PValidity::MayBeTrue;
-        } else {
-          res = PValidity::MayBeFalse;
-        }
-        ++stats::inhibitedForks;
-      }
-    }
-  }
+  if (res == PValidity::TrueOrFalse) {
+    assert(!replayKTest && "in replay mode, only one branch can be true.");
 
-  // Fix branch in only-replay-seed mode, if we don't have both true
-  // and false seeds.
-  if (isSeeding && (current.forkDisabled || OnlyReplaySeeds) &&
-      res == PValidity::TrueOrFalse) {
-    bool trueSeed = false, falseSeed = false;
-    // Is seed extension still ok here?
-    for (std::vector<SeedInfo>::iterator siit = it->second.begin(),
-                                         siie = it->second.end();
-         siit != siie; ++siit) {
-      ref<ConstantExpr> res;
-      bool success = solver->getValue(current.constraints.cs(),
-                                      siit->assignment.evaluate(condition), res,
-                                      current.queryMetaData);
-      assert(success && "FIXME: Unhandled solver failure");
-      (void)success;
-      if (res->isTrue()) {
-        trueSeed = true;
+    if (!branchingPermitted(current, 2)) {
+      TimerStatIncrementer timer(stats::forkTime);
+      if (theRNG.getBool()) {
+        res = PValidity::MayBeTrue;
       } else {
-        falseSeed = true;
+        res = PValidity::MayBeFalse;
       }
-      if (trueSeed && falseSeed)
-        break;
-    }
-    if (!(trueSeed && falseSeed)) {
-      assert(trueSeed || falseSeed);
-
-      res = trueSeed ? PValidity::MustBeTrue : PValidity::MustBeFalse;
-      addConstraint(current,
-                    trueSeed ? condition : Expr::createIsZero(condition));
+      ++stats::inhibitedForks;
     }
   }
 
@@ -1460,7 +1492,9 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
     if (res == PValidity::MayBeTrue) {
       addConstraint(current, condition);
     }
-
+    if (isSeeding) {
+      seedMap->at(&current) = trueSeeds;
+    }
     return StatePair(&current, nullptr);
   } else if (res == PValidity::MustBeFalse || res == PValidity::MayBeFalse) {
     if (!isInternal) {
@@ -1472,7 +1506,9 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
     if (res == PValidity::MayBeFalse) {
       addConstraint(current, Expr::createIsZero(condition));
     }
-
+    if (isSeeding) {
+      seedMap->at(&current) = falseSeeds;
+    }
     return StatePair(nullptr, &current);
   } else {
     // When does PValidity::None happen?
@@ -1484,42 +1520,10 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
 
     falseState = objectManager->branchState(trueState, reason);
 
-    if (it != seedMap->end()) {
-      std::vector<SeedInfo> seeds = it->second;
-      it->second.clear();
-      std::vector<SeedInfo> &trueSeeds = seedMap->at(trueState);
-      std::vector<SeedInfo> &falseSeeds = seedMap->at(falseState);
-      for (std::vector<SeedInfo>::iterator siit = seeds.begin(),
-                                           siie = seeds.end();
-           siit != siie; ++siit) {
-        ref<ConstantExpr> res;
-        bool success = solver->getValue(current.constraints.cs(),
-                                        siit->assignment.evaluate(condition),
-                                        res, current.queryMetaData);
-        assert(success && "FIXME: Unhandled solver failure");
-        (void)success;
-        if (res->isTrue()) {
-          trueSeeds.push_back(*siit);
-        } else {
-          falseSeeds.push_back(*siit);
-        }
-      }
-
-      bool swapInfo = false;
-      if (trueSeeds.empty()) {
-        if (&current == trueState)
-          swapInfo = true;
-        seedMap->erase(trueState);
-      }
-      if (falseSeeds.empty()) {
-        if (&current == falseState)
-          swapInfo = true;
-        seedMap->erase(falseState);
-      }
-      if (swapInfo) {
-        std::swap(trueState->coveredNew, falseState->coveredNew);
-        std::swap(trueState->coveredLines, falseState->coveredLines);
-      }
+    bool swapInfo = false;
+    if (swapInfo) {
+      std::swap(trueState->coveredNew, falseState->coveredNew);
+      std::swap(trueState->coveredLines, falseState->coveredLines);
     }
 
     if (pathWriter) {
@@ -1553,6 +1557,11 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
       return StatePair(nullptr, nullptr);
     }
 
+    if (isSeeding) {
+      seedMap->at(trueState) = trueSeeds;
+      seedMap->at(falseState) = falseSeeds;
+    }
+
     return StatePair(trueState, falseState);
   }
 }
@@ -1573,12 +1582,12 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
   }
 
   // Check to see if this constraint violates seeds.
-  std::map<ExecutionState *, std::vector<SeedInfo>>::iterator it =
+  std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
       seedMap->find(&state);
-  if (it != seedMap->end()) {
+  if (PatchSeeds && it != seedMap->end()) {
     bool warn = false;
-    for (std::vector<SeedInfo>::iterator siit = it->second.begin(),
-                                         siie = it->second.end();
+    for (std::vector<ExecutingSeed>::iterator siit = it->second.begin(),
+                                              siie = it->second.end();
          siit != siie; ++siit) {
       bool res;
       solver->setTimeout(coreSolverTimeout);
@@ -1723,7 +1732,7 @@ Executor::toConstantPointer(ExecutionState &state, ref<PointerExpr> e,
 void Executor::executeGetValue(ExecutionState &state, ref<Expr> e,
                                KInstruction *target) {
   e = Simplificator::simplifyExpr(state.constraints.cs(), e).simplified;
-  std::map<ExecutionState *, std::vector<SeedInfo>>::iterator it =
+  std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
       seedMap->find(&state);
   if (it == seedMap->end() || isa<ConstantExpr>(e) ||
       isa<ConstantPointerExpr>(e)) {
@@ -1736,8 +1745,8 @@ void Executor::executeGetValue(ExecutionState &state, ref<Expr> e,
     bindLocal(target, state, value);
   } else {
     std::set<ref<Expr>> values;
-    for (std::vector<SeedInfo>::iterator siit = it->second.begin(),
-                                         siie = it->second.end();
+    for (std::vector<ExecutingSeed>::iterator siit = it->second.begin(),
+                                              siie = it->second.end();
          siit != siie; ++siit) {
       ref<Expr> cond = siit->assignment.evaluate(e);
       cond = optimizer.optimizeExpr(cond, true);
@@ -4372,9 +4381,15 @@ void Executor::bindModuleConstants(llvm::APFloat::roundingMode rm) {
   }
 }
 
-bool Executor::checkMemoryUsage() {
+size_t Executor::getMemoryUsage() {
+  const auto mallocUsage = util::GetTotalMallocUsage();
+  const auto mmapUsage = memory->getUsedDeterministicSize();
+  return mallocUsage + mmapUsage;
+}
+
+Executor::MemoryUsage Executor::checkMemoryUsage() {
   if (!MaxMemory)
-    return true;
+    return None;
 
   // We need to avoid calling GetTotalMallocUsage() often because it
   // is O(elts on freelist). This is really bad since we start
@@ -4384,12 +4399,11 @@ bool Executor::checkMemoryUsage() {
       maxNewWriteableOSSize < OSCopySizeMemoryCheckThreshold &&
 
       maxNewStateStackSize < StackCopySizeMemoryCheckThreshold)
-    return true;
+    return None;
 
   // check memory limit
-  const auto mallocUsage = util::GetTotalMallocUsage() >> 20U;
-  const auto mmapUsage = memory->getUsedDeterministicSize() >> 20U;
-  const auto totalUsage = mallocUsage + mmapUsage;
+
+  const auto totalUsage = getMemoryUsage() >> 20U;
 
   if (MemoryTriggerCoverOnTheFly && totalUsage > MaxMemory * 0.75) {
     klee_warning_once(0,
@@ -4399,12 +4413,17 @@ bool Executor::checkMemoryUsage() {
   }
 
   atMemoryLimit = totalUsage > MaxMemory; // inhibit forking
-  if (!atMemoryLimit)
-    return true;
+  if (!atMemoryLimit) {
+    if (totalUsage < MaxMemory * 0.6) {
+      return Executor::Low;
+    } else {
+      return Executor::High;
+    }
+  }
 
   // only terminate states when threshold (+100MB) exceeded
-  if (totalUsage <= MaxMemory + 100)
-    return true;
+  if (totalUsage <= MaxMemory * 1.01)
+    return Executor::High;
 
   // just guess at how many to kill
   auto states = objectManager->getStates();
@@ -4416,6 +4435,7 @@ bool Executor::checkMemoryUsage() {
   // randomly select states for early termination
   std::vector<ExecutionState *> arr(states.begin(),
                                     states.end()); // FIXME: expensive
+
   for (unsigned i = 0, N = arr.size(); N && i < toKill; ++i, --N) {
     unsigned idx = theRNG.getInt32() % N;
     // Make two pulls to try and not hit a state that
@@ -4428,7 +4448,7 @@ bool Executor::checkMemoryUsage() {
                         StateTerminationType::OutOfMemory);
   }
 
-  return false;
+  return Executor::Full;
 }
 
 void Executor::decreaseConfidenceFromStoppedStates(
@@ -4494,72 +4514,113 @@ const KFunction *Executor::getKFunction(const llvm::Function *f) const {
   return (kfIt == kmodule->functionMap.end()) ? nullptr : kfIt->second;
 }
 
-void Executor::seed(ExecutionState &initialState) {
-  std::vector<SeedInfo> &v = seedMap->at(&initialState);
+void Executor::getKTestFilesInDir(std::string directoryPath,
+                                  std::vector<std::string> &results) {
+  std::error_code ec;
+  llvm::sys::fs::directory_iterator i(directoryPath, ec), e;
+  for (; i != e && !ec; i.increment(ec)) {
+    auto f = i->path();
+    if (f.size() >= 6 && f.substr(f.size() - 6, f.size()) == ".ktest") {
+      results.push_back(f);
+    }
+  }
 
-  for (std::vector<KTest *>::const_iterator it = usingSeeds->begin(),
-                                            ie = usingSeeds->end();
-       it != ie; ++it)
-    v.push_back(SeedInfo(*it));
+  if (ec) {
+    llvm::errs() << "ERROR: unable to read output directory: " << directoryPath
+                 << ": " << ec.message() << "\n";
+    exit(1);
+  }
+}
 
-  int lastNumSeeds = usingSeeds->size() + 10;
-  time::Point lastTime, startTime = lastTime = time::getWallTime();
-  ExecutionState *lastState = 0;
-  while (!seedMap->empty()) {
-    if (haltExecution) {
-      doDumpStates();
-      return;
+std::vector<ExecutingSeed> Executor::uploadNewSeeds() {
+  std::vector<ExecutingSeed> seeds;
+  if (StoreSeedsLocally) {
+    while ((!UploadAmount || seeds.size() < UploadAmount) &&
+           !storedSeeds->empty()) {
+      seeds.push_back(ExecutingSeed(storedSeeds->front()));
+      storedSeeds->pop_front();
     }
+  }
 
-    std::map<ExecutionState *, std::vector<SeedInfo>>::iterator it =
-        seedMap->upper_bound(lastState);
-    if (it == seedMap->end())
-      it = seedMap->begin();
-    lastState = it->first;
-    ExecutionState &state = *lastState;
-    KInstruction *ki = state.pc;
-    objectManager->setCurrentState(&state);
-    stepInstruction(state);
+  if (UploadAmount && seeds.size() >= UploadAmount) {
+    return seeds;
+  }
 
-    executeInstruction(state, ki);
-    timers.invoke();
-    if (::dumpStates)
-      dumpStates();
-    if (::dumpPForest)
-      dumpPForest();
-    objectManager->updateSubscribers();
+  for (std::vector<std::string>::iterator it = SeedOutFile.begin(),
+                                          ie = SeedOutFile.end();
+       it != ie && (!UploadAmount || seeds.size() < UploadAmount); ++it) {
+    ExecutingSeed out(it->substr(0, it->size() - 5));
+    if (!out.input) {
+      klee_error("unable to open: %s\n", (*it).c_str());
+    } else if (!PruneAlreadyExecutedStates || !out.isCompleted) {
+      seeds.push_back(out);
+    }
+  }
 
-    if ((stats::instructions % 1000) == 0) {
-      int numSeeds = 0, numStates = 0;
-      for (std::map<ExecutionState *, std::vector<SeedInfo>>::iterator
-               it = seedMap->begin(),
-               ie = seedMap->end();
-           it != ie; ++it) {
-        numSeeds += it->second.size();
-        numStates++;
-      }
-      const auto time = time::getWallTime();
-      const time::Span seedTime(SeedTime);
-      if (seedTime && time > startTime + seedTime) {
-        klee_warning("seed time expired, %d seeds remain over %d states",
-                     numSeeds, numStates);
-        break;
-      } else if (numSeeds <= lastNumSeeds - 10 ||
-                 time - lastTime >= time::seconds(10)) {
-        lastTime = time;
-        lastNumSeeds = numSeeds;
-        klee_message("%d seeds remaining over: %d states", numSeeds, numStates);
+  for (std::vector<std::string>::iterator it = SeedOutDir.begin(),
+                                          ie = SeedOutDir.end();
+       it != ie; ++it) {
+    std::vector<std::string> kTestFiles;
+    getKTestFilesInDir(*it, kTestFiles);
+    for (std::vector<std::string>::iterator it2 = kTestFiles.begin(),
+                                            ie = kTestFiles.end();
+         it2 != ie && (!UploadAmount || seeds.size() < UploadAmount); ++it2) {
+      ExecutingSeed out(it2->substr(0, it2->size() - 5));
+      if (!out.input) {
+        klee_error("unable to open: %s\n", (*it2).c_str());
+      } else if (!PruneAlreadyExecutedStates || !out.isCompleted) {
+        seeds.push_back(out);
       }
     }
+    if (kTestFiles.empty() && !RunForever) {
+      llvm::errs() << "seeds directory is empty: " << (*it).c_str() << "\n";
+    }
   }
+  // FIX: store all seed information like path and early termination reason in
+  // seedinfo file (preferably make it json)
+  for (auto it : seeds) {
+    if (RunForever && !it.path.empty()) {
+      std::remove((it.path + "seedinfo").c_str());
+      std::remove((it.path + "path").c_str());
+      std::remove((it.path + "early").c_str());
+      std::remove((it.path + "ktest").c_str());
+    }
+  }
+  return seeds;
+}
 
-  klee_message("seeding done (%d states remain)",
-               (int)objectManager->getStates().size());
-
-  if (OnlySeed) {
-    doDumpStates();
+void Executor::initialSeed(ExecutionState &initialState) {
+  // FIX: better file managment when seeding + flag if all seeds are completed
+  std::vector<ExecutingSeed> usingSeeds = uploadNewSeeds();
+  if (usingSeeds.empty()) {
     return;
   }
+  std::vector<ExecutingSeed> &v = seedMap->at(&initialState);
+  for (std::vector<ExecutingSeed>::const_iterator it = usingSeeds.begin(),
+                                                  ie = usingSeeds.end();
+       it != ie; ++it) {
+    v.push_back(*it);
+  }
+  klee_message("Seeding began using %ld seeds!\n", usingSeeds.size());
+  objectManager->seed(&initialState);
+  objectManager->updateSubscribers();
+}
+
+StoredSeed Executor::storeState(const ExecutionState &state) {
+  KTest *ktest = 0;
+  ktest = new KTest;
+  bool success = getSymbolicSolution(state, ktest);
+  size_t size = 0;
+  for (unsigned i = 0; i < ktest->numObjects; i++) {
+    size += std::strlen(ktest->objects[i].name) * sizeof(char);
+    size += ktest->objects[i].numBytes * sizeof(unsigned char);
+    size += ktest->objects[i].numPointers * sizeof(Pointer);
+  }
+  llvm::errs() << size << "\n";
+  if (!success)
+    klee_warning("unable to get symbolic solution, losing test case");
+  StoredSeed seed(ktest, state.steppedInstructions, 0);
+  return seed;
 }
 
 void Executor::reportProgressTowardsTargets(std::string prefix,
@@ -4614,10 +4675,6 @@ void Executor::run(ExecutionState *initialState) {
   if (guidanceKind != GuidanceKind::ErrorGuidance)
     timers.reset();
 
-  if (usingSeeds) {
-    seed(*initialState);
-  }
-
   searcher =
       std::make_unique<ForwardOnlySearcher>(constructUserSearcher(*this));
 
@@ -4635,16 +4692,30 @@ void Executor::run(ExecutionState *initialState) {
 
   objectManager->addSubscriber(searcher.get());
 
+  ExecutionState *firstState =
+      objectManager->branchState(initialState, BranchType::InitialBranch);
+
   objectManager->initialUpdate();
 
+  initialSeed(*firstState);
   // main interpreter loop
   while (!haltExecution && !searcher->empty()) {
     auto action = searcher->selectAction();
     executeAction(action);
     objectManager->updateSubscribers();
-
-    if (!checkMemoryUsage()) {
-      objectManager->updateSubscribers();
+    MemoryUsage usage = checkMemoryUsage();
+    if (usage != Full) {
+      if (RunForever && usage == Low) {
+        ExecutionState *newSeededState =
+            objectManager->branchState(initialState, BranchType::InitialBranch);
+        initialSeed(*newSeededState);
+      }
+    }
+    objectManager->updateSubscribers();
+    if (RunForever && searcher->empty()) {
+      ExecutionState *newSeededState =
+          objectManager->branchState(initialState, BranchType::InitialBranch);
+      initialSeed(*newSeededState);
     }
   }
 
@@ -4722,6 +4793,27 @@ void Executor::executeAction(ref<SearcherAction> action) {
   timers.invoke();
 }
 
+bool Executor::reachedMaxSeedInstructions(ExecutionState *state) {
+  assert(state->isSeeded);
+  auto it = seedMap->find(state);
+  assert(it != seedMap->end());
+  if (it->second.size() != 1) {
+    return false;
+  }
+
+  std::vector<ExecutingSeed>::iterator siit = it->second.begin();
+  if (siit->maxInstructions &&
+      siit->maxInstructions >= state->steppedInstructions) {
+    seedMap->erase(state);
+    objectManager->unseed(state);
+    if (seedMap->size() == 0) {
+      klee_message("Seeding done!\n");
+    }
+    return true;
+  }
+  return false;
+}
+
 void Executor::goForward(ref<ForwardAction> action) {
   ref<ForwardAction> fa = cast<ForwardAction>(action);
   objectManager->setCurrentState(fa->state);
@@ -4754,7 +4846,7 @@ void Executor::goForward(ref<ForwardAction> action) {
   } else if (state.isSymbolicCycled(MaxSymbolicCycles)) {
     terminateStateEarly(state, "max-sym-cycles exceeded.",
                         StateTerminationType::MaxCycles);
-  } else {
+  } else if (!fa->state->isSeeded || !reachedMaxSeedInstructions(fa->state)) {
     maxNewWriteableOSSize = 0;
     maxNewStateStackSize = 0;
 
@@ -4864,6 +4956,10 @@ HaltExecution::Reason fromStateTerminationType(StateTerminationType t) {
 
 void Executor::terminateState(ExecutionState &state,
                               StateTerminationType terminationType) {
+  if (seedMap->find(&state) != seedMap->end()) {
+    seedMap->erase(&state);
+    objectManager->unseed(&state);
+  }
   state.terminationReasonType = fromStateTerminationType(terminationType);
   if (terminationType >= StateTerminationType::MaxDepth &&
       terminationType <= StateTerminationType::EARLY) {
@@ -4907,11 +5003,15 @@ void Executor::terminateStateEarly(ExecutionState &state, const Twine &message,
        shouldWriteTest(state)) ||
       (AlwaysOutputSeeds && seedMap->count(&state))) {
     state.clearCoveredNew();
-    interpreterHandler->processTestCase(
-        state, (message + "\n").str().c_str(),
-        terminationTypeFileExtension(reason).c_str(),
-        reason > StateTerminationType::EARLY &&
-            reason <= StateTerminationType::EXECERR);
+    if (RunForever && StoreSeedsLocally) {
+      storedSeeds->push_back(storeState(state));
+    } else {
+      interpreterHandler->processTestCase(
+          state, (message + "\n").str().c_str(),
+          terminationTypeFileExtension(reason).c_str(),
+          reason > StateTerminationType::EARLY &&
+              reason <= StateTerminationType::EXECERR);
+    }
   }
   terminateState(state, reason);
 }
@@ -6740,14 +6840,14 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
     }
     state.addSymbolic(mo, array, type);
 
-    std::map<ExecutionState *, std::vector<SeedInfo>>::iterator it =
+    std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
         seedMap->find(&state);
     if (it != seedMap->end()) { // In seed mode we need to add this as a
                                 // binding.
-      for (std::vector<SeedInfo>::iterator siit = it->second.begin(),
-                                           siie = it->second.end();
+      for (std::vector<ExecutingSeed>::iterator siit = it->second.begin(),
+                                                siie = it->second.end();
            siit != siie; ++siit) {
-        SeedInfo &si = *siit;
+        ExecutingSeed &si = *siit;
         KTestObject *obj = si.getNextInput(mo, NamedSeedMatching);
 
         if (!obj) {
@@ -7393,7 +7493,7 @@ bool isMakeSymbolic(const klee::Symbolic &symb) {
   return good;
 }
 
-bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
+bool Executor::getSymbolicSolution(const ExecutionState &state, KTest *res) {
   solver->setTimeout(coreSolverTimeout);
 
   PathConstraints extendedConstraints(state.constraints);
@@ -7574,9 +7674,13 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
     }
   }
 
-  res.numObjects = symbolics.size();
-  res.objects = new KTestObject[res.numObjects];
-  res.uninitCoeff = uninitObjects.size() * UninitMemoryTestMultiplier;
+  res->numArgs = interpreterHandler->argc();
+  res->args = interpreterHandler->argv();
+  res->symArgvs = 0;
+  res->symArgvLen = 0;
+  res->numObjects = symbolics.size();
+  res->objects = new KTestObject[res->numObjects];
+  res->uninitCoeff = uninitObjects.size() * UninitMemoryTestMultiplier;
 
   {
     size_t i = 0;
@@ -7584,8 +7688,9 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
     for (auto &symbolic : symbolics) {
       auto mo = symbolic.memoryObject;
       auto &values = model.bindings.at(symbolic.array);
-      KTestObject *o = &res.objects[i];
-      o->name = const_cast<char *>(mo->name.c_str());
+      KTestObject *o = &res->objects[i];
+      o->name = new char[mo->name.size()];
+      std::strcpy(o->name, mo->name.c_str());
       o->address = cast<ConstantExpr>(evaluator.visit(mo->getBaseExpr()))
                        ->getZExtValue();
       o->numBytes = cast<ConstantExpr>(evaluator.visit(mo->getSizeExpr()))
@@ -7600,7 +7705,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) {
     }
   }
 
-  setInitializationGraph(state, symbolics, model, res);
+  setInitializationGraph(state, symbolics, model, *res);
 
   return true;
 }
@@ -7615,6 +7720,11 @@ void Executor::getBlockPath(const ExecutionState &state,
   blockPath = state.constraints.path().toString();
 }
 
+void Executor::getSteppedInstructions(const ExecutionState &state,
+                                      unsigned &res) {
+  res = state.steppedInstructions;
+}
+
 void Executor::doImpliedValueConcretization(ExecutionState &state, ref<Expr> e,
                                             ref<ConstantExpr> value) {
   abort(); // FIXME: Broken until we sort out how to do the write back.
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index eb769d18310..64604680dd1 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -94,7 +94,7 @@ class MemoryObject;
 class ObjectState;
 class PForest;
 class Searcher;
-class SeedInfo;
+class ExecutingSeed;
 class SpecialFunctionHandler;
 struct StackFrame;
 class SymbolicSource;
@@ -161,6 +161,7 @@ class Executor : public Interpreter {
   std::unique_ptr<TargetCalculator> targetCalculator;
   std::unique_ptr<TargetManager> targetManager;
 
+  // cringe
   /// When non-empty the Executor is running in "seed" mode. The
   /// states in this map will be executed in an arbitrary order
   /// (outside the normal search interface) until they terminate. When
@@ -170,6 +171,8 @@ class Executor : public Interpreter {
   /// on as-yet-to-be-determined flags.
   std::unique_ptr<SeedMap> seedMap;
 
+  std::unique_ptr<std::deque<StoredSeed>> storedSeeds;
+
   /// Map of globals to their representative memory object.
   std::map<const llvm::GlobalValue *, MemoryObject *> globalObjects;
 
@@ -195,10 +198,6 @@ class Executor : public Interpreter {
   /// object.
   unsigned replayPosition;
 
-  /// When non-null a list of "seed" inputs which will be used to
-  /// drive execution.
-  const std::vector<struct KTest *> *usingSeeds;
-
   /// Disables forking, instead a random path is chosen. Enabled as
   /// needed to control memory usage. \see fork()
   bool atMemoryLimit;
@@ -260,7 +259,15 @@ class Executor : public Interpreter {
 
   void executeInstruction(ExecutionState &state, KInstruction *ki);
 
-  void seed(ExecutionState &initialState);
+  states_ty &getSeedChanges() { return objectManager->getSeedChanges(); }
+
+  void getKTestFilesInDir(std::string directoryPath,
+                          std::vector<std::string> &results);
+  std::vector<ExecutingSeed> uploadNewSeeds();
+  void initialSeed(ExecutionState &initialState);
+
+  StoredSeed storeState(const ExecutionState &state);
+
   void run(ExecutionState *initialState);
 
   void initializeTypeManager();
@@ -697,10 +704,15 @@ class Executor : public Interpreter {
   void doImpliedValueConcretization(ExecutionState &state, ref<Expr> e,
                                     ref<ConstantExpr> value);
 
+  size_t getMemoryUsage();
+
   /// check memory usage and terminate states when over threshold of -max-memory
   /// + 100MB \return true if below threshold, false otherwise (states were
   /// terminated)
-  bool checkMemoryUsage();
+
+  enum MemoryUsage { None, Low, High, Full };
+
+  MemoryUsage checkMemoryUsage();
 
   /// check if branching/forking into N branches is allowed
   bool branchingPermitted(ExecutionState &state, unsigned N);
@@ -713,6 +725,8 @@ class Executor : public Interpreter {
   void dumpPForest();
 
   void executeAction(ref<SearcherAction> action);
+
+  bool reachedMaxSeedInstructions(ExecutionState *state);
   void goForward(ref<ForwardAction> action);
 
   const KInstruction *getKInst(const llvm::Instruction *ints) const;
@@ -756,10 +770,6 @@ class Executor : public Interpreter {
 
   void setFunctionsByModule(FunctionsByModule &&functionsByModule) override;
 
-  void useSeeds(const std::vector<struct KTest *> *seeds) override {
-    usingSeeds = seeds;
-  }
-
   ExecutionState *formState(llvm::Function *f);
   ExecutionState *formState(llvm::Function *f, int argc, char **argv,
                             char **envp);
@@ -828,7 +838,7 @@ class Executor : public Interpreter {
   void logState(const ExecutionState &state, int id,
                 std::unique_ptr<llvm::raw_fd_ostream> &f) override;
 
-  bool getSymbolicSolution(const ExecutionState &state, KTest &res) override;
+  bool getSymbolicSolution(const ExecutionState &state, KTest *res) override;
 
   void getCoveredLines(const ExecutionState &state,
                        std::map<std::string, std::set<unsigned>> &res) override;
@@ -836,6 +846,8 @@ class Executor : public Interpreter {
   void getBlockPath(const ExecutionState &state,
                     std::string &blockPath) override;
 
+  void getSteppedInstructions(const ExecutionState &state, unsigned &res);
+
   Expr::Width getWidthForLLVMType(llvm::Type *type) const;
   size_t getAllocationAlignment(const llvm::Value *allocSite) const;
 
diff --git a/lib/Core/ObjectManager.cpp b/lib/Core/ObjectManager.cpp
index d79d1d28a85..d0cdada4d27 100644
--- a/lib/Core/ObjectManager.cpp
+++ b/lib/Core/ObjectManager.cpp
@@ -23,10 +23,13 @@ void ObjectManager::addSubscriber(Subscriber *s) { subscribers.push_back(s); }
 void ObjectManager::addProcessForest(PForest *pf) { processForest = pf; }
 
 void ObjectManager::addInitialState(ExecutionState *state) {
-  states.insert(state);
   processForest->addRoot(state);
 }
 
+void ObjectManager::addFirstState(ExecutionState *state) {
+  states.insert(state);
+}
+
 void ObjectManager::setCurrentState(ExecutionState *_current) {
   assert(current == nullptr);
   current = _current;
@@ -35,7 +38,6 @@ void ObjectManager::setCurrentState(ExecutionState *_current) {
 
 ExecutionState *ObjectManager::branchState(ExecutionState *state,
                                            BranchType reason) {
-  assert(statesUpdated);
   ExecutionState *newState = state->branch();
   addedStates.push_back(newState);
   processForest->attach(state->ptreeNode, newState, state, reason);
@@ -44,6 +46,7 @@ ExecutionState *ObjectManager::branchState(ExecutionState *state,
 }
 
 void ObjectManager::removeState(ExecutionState *state) {
+
   std::vector<ExecutionState *>::iterator itr =
       std::find(removedStates.begin(), removedStates.end(), state);
   assert(itr == removedStates.end());
@@ -55,6 +58,23 @@ void ObjectManager::removeState(ExecutionState *state) {
   removedStates.push_back(state);
 }
 
+void ObjectManager::unseed(ExecutionState *state) {
+  if (state->isSeeded) {
+    state->isSeeded = false;
+    seedChanges.insert(state);
+    statesUpdated = true;
+  }
+}
+void ObjectManager::seed(ExecutionState *state) {
+  if (!state->isSeeded) {
+    state->isSeeded = true;
+    seedChanges.insert(state);
+    statesUpdated = true;
+  }
+}
+
+states_ty &ObjectManager::getSeedChanges() { return seedChanges; }
+
 void ObjectManager::updateSubscribers() {
   if (statesUpdated) {
     ref<Event> e = new States(current, addedStates, removedStates);
@@ -75,6 +95,7 @@ void ObjectManager::updateSubscribers() {
     current = nullptr;
     addedStates.clear();
     removedStates.clear();
+    seedChanges.clear();
     statesUpdated = false;
   }
 }
diff --git a/lib/Core/ObjectManager.h b/lib/Core/ObjectManager.h
index 3f7034f3c9d..fa25dbf0b42 100644
--- a/lib/Core/ObjectManager.h
+++ b/lib/Core/ObjectManager.h
@@ -54,12 +54,21 @@ class ObjectManager {
   void addProcessForest(PForest *);
 
   void addInitialState(ExecutionState *state);
+  void addFirstState(ExecutionState *state);
 
   void setCurrentState(ExecutionState *_current);
 
   ExecutionState *branchState(ExecutionState *state, BranchType reason);
   void removeState(ExecutionState *state);
 
+  void unseed(ExecutionState *state);
+  void seed(ExecutionState *state);
+
+  states_ty &getSeedChanges();
+
+  ExecutionState *initializeState(KInstruction *location,
+                                  std::set<ref<Target>> targets);
+
   const states_ty &getStates();
 
   void updateSubscribers();
@@ -80,6 +89,8 @@ class ObjectManager {
   ExecutionState *current = nullptr;
   std::vector<ExecutionState *> addedStates;
   std::vector<ExecutionState *> removedStates;
+
+  states_ty seedChanges;
 };
 
 class Subscriber {
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 1bfdb2620de..f8b56a3427e 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -926,3 +926,86 @@ bool DiscreteTimeFairSearcher::empty() { return functions.empty(); }
 void DiscreteTimeFairSearcher::printName(llvm::raw_ostream &os) {
   os << "DiscreteTimeFairSearcher\n";
 }
+
+//
+
+SeededSearcher::SeededSearcher(Searcher *_searcher, states_ty &_seedChanges)
+    : baseSearcher(_searcher), seedChanges(_seedChanges) {
+  seededSearcher = std::unique_ptr<BFSSearcher>(new BFSSearcher());
+}
+
+ExecutionState &SeededSearcher::selectState() {
+  update(nullptr, {}, {});
+  if (!seededSearcher->empty()) {
+    return seededSearcher->selectState();
+  }
+  return baseSearcher->selectState();
+}
+
+void SeededSearcher::update(
+    ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
+    const std::vector<ExecutionState *> &removedStates) {
+
+  for (auto state : seedChanges) {
+    if (state->isSeeded && baseSearcherStates.count(state) != 0) {
+      baseSearcher->update(nullptr, {}, {state});
+      baseSearcherStates.erase(state);
+    }
+    if (state->isSeeded && seededSearcherStates.count(state) == 0) {
+      seededSearcher->update(nullptr, {state}, {});
+      seededSearcherStates.insert(state);
+    }
+    if (!state->isSeeded && seededSearcherStates.count(state) != 0) {
+      seededSearcher->update(nullptr, {}, {state});
+      seededSearcherStates.erase(state);
+    }
+    if (!state->isSeeded && baseSearcherStates.count(state) == 0) {
+      baseSearcher->update(nullptr, {state}, {});
+      baseSearcherStates.insert(state);
+    }
+  }
+
+  std::vector<ExecutionState *> addedUnseededStates;
+  std::vector<ExecutionState *> addedSeededStates;
+  std::vector<ExecutionState *> removedUnseededStates;
+  std::vector<ExecutionState *> removedSeededStates;
+  for (auto state : addedStates) {
+    if (state->isSeeded && seededSearcherStates.count(state) == 0) {
+      addedSeededStates.push_back(state);
+      seededSearcherStates.insert(state);
+    } else if (!state->isSeeded && baseSearcherStates.count(state) == 0) {
+      addedUnseededStates.push_back(state);
+      baseSearcherStates.insert(state);
+    }
+  }
+  for (auto state : removedStates) {
+    if (state->isSeeded && seededSearcherStates.count(state) != 0) {
+      removedSeededStates.push_back(state);
+      seededSearcherStates.erase(state);
+    } else if (!state->isSeeded && baseSearcherStates.count(state) != 0) {
+      removedUnseededStates.push_back(state);
+      baseSearcherStates.erase(state);
+    }
+  }
+
+  if (current && current->isSeeded) {
+    baseSearcher->update(nullptr, addedUnseededStates, removedUnseededStates);
+    seededSearcher->update(current, addedSeededStates, removedSeededStates);
+  } else if (current && !current->isSeeded) {
+    baseSearcher->update(current, addedUnseededStates, removedUnseededStates);
+    seededSearcher->update(nullptr, addedSeededStates, removedSeededStates);
+  } else {
+    baseSearcher->update(nullptr, addedUnseededStates, removedUnseededStates);
+    seededSearcher->update(nullptr, addedSeededStates, removedSeededStates);
+  }
+}
+
+bool SeededSearcher::empty() {
+  return baseSearcher->empty() && seededSearcher->empty();
+}
+
+void SeededSearcher::printName(llvm::raw_ostream &os) {
+  os << "<SeededSearcher> with base searcher:\n";
+  baseSearcher->printName(os);
+  os << "</SeededSearcher> \n";
+} // cringe
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index ee1bc186906..6222de713e9 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -425,6 +425,27 @@ class DiscreteTimeFairSearcher final : public Searcher {
   bool empty() override;
   void printName(llvm::raw_ostream &os) override;
 };
+
+/// Seeded searcher is used to select seeded states before unseeded
+class SeededSearcher final : public Searcher {
+  std::unique_ptr<Searcher> baseSearcher;
+  std::unique_ptr<BFSSearcher> seededSearcher;
+  states_ty &seedChanges;
+  states_ty baseSearcherStates;
+  states_ty seededSearcherStates;
+
+public:
+  explicit SeededSearcher(Searcher *_searcher, states_ty &_seedChanges);
+
+  ExecutionState &selectState() override;
+
+  void update(ExecutionState *current,
+              const std::vector<ExecutionState *> &addedStates,
+              const std::vector<ExecutionState *> &removedStates) override;
+  ~SeededSearcher() override = default;
+  bool empty() override;
+  void printName(llvm::raw_ostream &os) override;
+};
 } // namespace klee
 
 #endif /* KLEE_SEARCHER_H */
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index efd2df76174..ab4aba864af 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -1,4 +1,5 @@
-//===-- SeedInfo.cpp ------------------------------------------------------===//
+//===-- ExecutingSeed.cpp
+//------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -18,11 +19,30 @@
 #include "klee/Expr/ExprUtil.h"
 #include "klee/Support/ErrorHandling.h"
 
+#include <fstream>
 #include <set>
 
 using namespace klee;
 
-KTestObject *SeedInfo::getNextInput(const MemoryObject *mo, bool byName) {
+void KTestDeleter::kTestDeleter(KTest *kTest) { kTest_free(kTest); }
+void KTestDeleter::testKTestDeleter(KTest *kTest) { test_kTest_free(kTest); }
+
+ExecutingSeed::ExecutingSeed(std::string _path)
+    : input(kTest_fromFile((_path + "ktest").c_str()),
+            KTestDeleter::kTestDeleter),
+      path(_path) {
+  std::ifstream seedInfoStream(_path + "seedinfo");
+  if (seedInfoStream.good()) {
+    seedInfoStream >> maxInstructions;
+    seedInfoStream >> isCompleted;
+  }
+}
+
+ExecutingSeed::ExecutingSeed(StoredSeed seed)
+    : input(seed.output), maxInstructions(seed.steppedInstructions),
+      isCompleted(seed.isCompleted), inputPosition(0) {}
+
+KTestObject *ExecutingSeed::getNextInput(const MemoryObject *mo, bool byName) {
   if (byName) {
     unsigned i;
 
@@ -63,8 +83,8 @@ KTestObject *SeedInfo::getNextInput(const MemoryObject *mo, bool byName) {
   }
 }
 
-void SeedInfo::patchSeed(const ExecutionState &state, ref<Expr> condition,
-                         TimingSolver *solver) {
+void ExecutingSeed::patchSeed(const ExecutionState &state, ref<Expr> condition,
+                              TimingSolver *solver) {
   ConstraintSet required = state.constraints.cs();
   required.addConstraint(condition);
 
diff --git a/lib/Core/SeedInfo.h b/lib/Core/SeedInfo.h
index ee84133bc39..4e579666c3a 100644
--- a/lib/Core/SeedInfo.h
+++ b/lib/Core/SeedInfo.h
@@ -1,4 +1,4 @@
-//===-- SeedInfo.h ----------------------------------------------*- C++ -*-===//
+//===--SeedInfo.h ----------------------------------------------*- C++ -*-===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -24,15 +24,46 @@ class ExecutionState;
 class TimingSolver;
 class MemoryObject;
 
-class SeedInfo {
+struct KTestDeleter {
+  static void kTestDeleter(KTest *kTest);
+  static void testKTestDeleter(KTest *kTest);
+};
+
+class StoredSeed {
+public:
+  std::shared_ptr<KTest> output;
+  unsigned steppedInstructions;
+  bool isCompleted;
+
+public:
+  ~StoredSeed() {}
+
+  explicit StoredSeed(KTest *output, unsigned steppedInstructions,
+                      bool isCompleted)
+      : output(output, KTestDeleter::testKTestDeleter),
+        steppedInstructions(steppedInstructions), isCompleted(isCompleted) {}
+};
+
+class ExecutingSeed {
 public:
   Assignment assignment;
-  KTest *input;
-  unsigned inputPosition;
+  std::shared_ptr<KTest> input;
+  unsigned maxInstructions = 0;
+  bool isCompleted = 0;
+  unsigned inputPosition = 0;
   std::set<struct KTestObject *> used;
+  std::string path = "";
 
 public:
-  explicit SeedInfo(KTest *_input) : input(_input), inputPosition(0) {}
+  ~ExecutingSeed() {}
+
+  explicit ExecutingSeed(KTest *input, unsigned maxInstructions,
+                         bool isCompleted)
+      : input(input, KTestDeleter::testKTestDeleter),
+        maxInstructions(maxInstructions), isCompleted(isCompleted),
+        inputPosition(0) {}
+  ExecutingSeed(StoredSeed seed);
+  ExecutingSeed(std::string _path);
 
   KTestObject *getNextInput(const MemoryObject *mo, bool byName);
 
diff --git a/lib/Core/SeedMap.cpp b/lib/Core/SeedMap.cpp
index f740caed812..8fb28804ebd 100644
--- a/lib/Core/SeedMap.cpp
+++ b/lib/Core/SeedMap.cpp
@@ -8,7 +8,7 @@ SeedMap::SeedMap() {}
 void SeedMap::update(ref<ObjectManager::Event> e) {
   if (auto statesEvent = dyn_cast<ObjectManager::States>(e)) {
     for (const auto state : statesEvent->removed) {
-      std::map<ExecutionState *, std::vector<SeedInfo>>::iterator it =
+      std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
           seedMap.find(state);
       if (it != seedMap.end()) {
         seedMap.erase(it);
@@ -17,33 +17,35 @@ void SeedMap::update(ref<ObjectManager::Event> e) {
   }
 }
 
-std::map<ExecutionState *, std::vector<SeedInfo>>::iterator
+std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator
 SeedMap::upper_bound(ExecutionState *state) {
   return seedMap.upper_bound(state);
 }
 
-std::map<ExecutionState *, std::vector<SeedInfo>>::iterator
+std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator
 SeedMap::find(ExecutionState *state) {
   return seedMap.find(state);
 }
 
-std::map<ExecutionState *, std::vector<SeedInfo>>::iterator SeedMap::begin() {
+std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator
+SeedMap::begin() {
   return seedMap.begin();
 }
 
-std::map<ExecutionState *, std::vector<SeedInfo>>::iterator SeedMap::end() {
+std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator
+SeedMap::end() {
   return seedMap.end();
 }
 
 void SeedMap::erase(
-    std::map<ExecutionState *, std::vector<SeedInfo>>::iterator it) {
+    std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it) {
   seedMap.erase(it);
 }
 
 void SeedMap::erase(ExecutionState *state) { seedMap.erase(state); }
 
 void SeedMap::push_back(ExecutionState *state,
-                        std::vector<SeedInfo>::iterator siit) {
+                        std::vector<ExecutingSeed>::iterator siit) {
   seedMap[state].push_back(*siit);
 }
 
@@ -51,7 +53,7 @@ std::size_t SeedMap::count(ExecutionState *state) {
   return seedMap.count(state);
 }
 
-std::vector<SeedInfo> &SeedMap::at(ExecutionState *state) {
+std::vector<ExecutingSeed> &SeedMap::at(ExecutionState *state) {
   return seedMap[state];
 }
 
diff --git a/lib/Core/SeedMap.h b/lib/Core/SeedMap.h
index 783a729282f..75f5235320e 100644
--- a/lib/Core/SeedMap.h
+++ b/lib/Core/SeedMap.h
@@ -10,24 +10,27 @@
 namespace klee {
 class SeedMap : public Subscriber {
 private:
-  std::map<ExecutionState *, std::vector<SeedInfo>> seedMap;
+  std::map<ExecutionState *, std::vector<ExecutingSeed>> seedMap;
 
 public:
   SeedMap();
 
   void update(ref<ObjectManager::Event> e) override;
 
-  std::map<ExecutionState *, std::vector<SeedInfo>>::iterator
+  std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator
   upper_bound(ExecutionState *state);
-  std::map<ExecutionState *, std::vector<SeedInfo>>::iterator
+  std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator
   find(ExecutionState *state);
-  std::map<ExecutionState *, std::vector<SeedInfo>>::iterator end();
-  std::map<ExecutionState *, std::vector<SeedInfo>>::iterator begin();
-  void erase(std::map<ExecutionState *, std::vector<SeedInfo>>::iterator it);
+  std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator end();
+  std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator begin();
+  void
+  erase(std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it);
   void erase(ExecutionState *state);
-  void push_back(ExecutionState *state, std::vector<SeedInfo>::iterator siit);
+  void push_back(ExecutionState *state,
+                 std::vector<ExecutingSeed>::iterator siit);
   std::size_t count(ExecutionState *state);
-  std::vector<SeedInfo> &at(ExecutionState *state);
+  std::vector<ExecutingSeed> &at(ExecutionState *state);
+  unsigned size() { return seedMap.size(); }
   bool empty();
 
   virtual ~SeedMap();
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index cdd9cb09a59..63d965779fe 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -74,6 +74,12 @@ cl::opt<bool> UseBatchingSearch(
              "(default=false)"),
     cl::init(false), cl::cat(SearchCat));
 
+cl::opt<bool>
+    UseSeededSearch("use-seeded-search",
+                    cl::desc("Use seeded searcher (explores seeded states "
+                             "before unseeded) (default=false)"),
+                    cl::init(false), cl::cat(SearchCat));
+
 cl::opt<unsigned> BatchInstructions(
     "batch-instructions",
     cl::desc("Number of instructions to batch when using "
@@ -206,6 +212,11 @@ Searcher *klee::constructUserSearcher(Executor &executor) {
     searcher = constructBaseSearcher(executor);
   }
 
+  if (UseSeededSearch) {
+    states_ty &seedChandes = executor.getSeedChanges();
+    searcher = new SeededSearcher(searcher, seedChandes);
+  }
+
   llvm::raw_ostream &os = executor.getHandler().getInfoStream();
 
   os << "BEGIN searcher description\n";
diff --git a/scripts/kleef b/scripts/kleef
index a5a99fcc23e..0cec8c0b097 100755
--- a/scripts/kleef
+++ b/scripts/kleef
@@ -20,6 +20,7 @@ def klee_options(
     f_err,
     f_cov,
     write_ktests,
+    run_forever
 ):
     if max_time and int(max_time) > 30:
         MAX_SOLVER_TIME = 15
@@ -65,7 +66,13 @@ def klee_options(
         "--memory-backend=mixed",
         "--max-fixed-size-structures-size=64",
     ]
-
+    if run_forever:
+        cmd += [
+            f"--seed-dir={test_output_dir}",
+            "--use-seeded-search",
+            "--prune-already-executed-states",
+            "--store-seeds-locally",
+        ]
     if is32:
         cmd += [
             "--allocate-determ",
@@ -73,7 +80,7 @@ def klee_options(
             "--allocate-determ-start-address=0x00030000000",
             "--x86FP-as-x87FP80",
         ]
-
+    
     if f_err:
         cmd += [
             "--optimize=true",
@@ -189,6 +196,7 @@ class KLEEF(object):
         use_perf=False,
         use_valgrind=False,
         write_ktests=False,
+        run_forever=False
     ):
         self.source = Path(source) if source else None
         self.is32 = is32
@@ -204,6 +212,7 @@ class KLEEF(object):
             self.write_ktests = "true"
         else:
             self.write_ktests = "false"
+        self.run_forever = run_forever
 
         # This file is inside the bin directory - use the root as base
         self.bin_directory = Path(__file__).parent
@@ -308,6 +317,7 @@ class KLEEF(object):
             self.f_err,
             self.f_cov,
             self.write_ktests,
+            self.run_forever
         )
         if self.isModifyingUlimitPermitted():
             cmd = ["ulimit -s unlimited", "&&"] + cmd
@@ -407,6 +417,7 @@ def run(args):
         use_perf=args.perf,
         use_valgrind=args.valgrind,
         write_ktests=args.write_ktests,
+        run_forever=args.run_forever
     )
     wrapper.compile()
     return wrapper.run()
@@ -458,6 +469,10 @@ def main():
     parser.add_argument(
         "--write-ktests", help="Write tests in KTest format", action="store_true"
     )
+    parser.add_argument(
+        "--run-forever", help="Run symbolic execution forever", action="store_true"
+    )
+
     args = parser.parse_args()
     run(args)
 
diff --git a/test/Feature/TestSeeding.c b/test/Feature/TestSeeding.c
new file mode 100644
index 00000000000..765c055f4be
--- /dev/null
+++ b/test/Feature/TestSeeding.c
@@ -0,0 +1,30 @@
+// REQUIRES: z3
+// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
+// RUN: rm -rf %t1.klee-out
+// RUN: rm -rf %t2.klee-out
+// RUN: rm -rf %t3.klee-out
+// RUN: rm -rf %t4.klee-out
+// RUN: %klee --output-dir=%t1.klee-out  %t1.bc
+// RUN: %klee --output-dir=%t2.klee-out --max-instructions=500 %t1.bc
+// RUN: %klee --seed-dir=%t1.klee-out --use-seeded-search --output-dir=%t3.klee-out  %t1.bc
+// RUN: %klee --seed-dir=%t2.klee-out --use-seeded-search --output-dir=%t4.klee-out  %t1.bc
+// RUN: %klee-stats --print-columns 'SolverQueries' --table-format=csv %t3.klee-out > %t3.stats
+// RUN: %klee-stats --print-columns 'SolverQueries' --table-format=csv %t4.klee-out > %t4.stats
+// RUN: FileCheck -check-prefix=CHECK-NO-MAX-INSTRUCTIONS -input-file=%t3.stats %s
+// RUN: FileCheck -check-prefix=CHECK-MAX-INSTRUCTIONS -input-file=%t4.stats %s
+
+#include "klee/klee.h"
+
+int main(int argc, char **argv) {
+  int a;
+  klee_make_symbolic(&a, sizeof(a), "a");
+  for (int i = 0; i < 100; i++) {
+    if (a + i == 2 * i) {
+      break;
+    }
+  }
+}
+// CHECK-NO-MAX-INSTRUCTIONS: SolverQueries
+// CHECK-NO-MAX-INSTRUCTIONS: 101
+// CHECK-MAX-INSTRUCTIONS: SolverQueries
+// CHECK-MAX-INSTRUCTIONS: 172
\ No newline at end of file
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 48d1f85c061..3a56f36cf91 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -101,6 +101,11 @@ cl::opt<bool> WriteKTests(
     cl::desc("Write .ktest files for each test case (default=true)"),
     cl::cat(TestCaseCat));
 
+cl::opt<bool> WriteSeeds(
+    "write-seeds", cl::init(true),
+    cl::desc("Write seed files files for each test case (default=true)"),
+    cl::cat(TestCaseCat));
+
 cl::opt<bool>
     WriteCVCs("write-cvcs",
               cl::desc("Write .cvc files for each test case (default=false)"),
@@ -178,6 +183,12 @@ cl::opt<std::string> OutputDir(
     cl::desc("Directory in which to write results (default=klee-out-<N>)"),
     cl::init(""), cl::cat(StartCat));
 
+cl::opt<std::string> OutputEarlyDir(
+    "output-early-dir",
+    cl::desc(
+        "Directory in which to write early results (default=klee-out-<N>)"),
+    cl::init(""), cl::cat(StartCat));
+
 cl::opt<std::string> Environ(
     "env-file",
     cl::desc("Parse environment from the given file (in \"env\" format)"),
@@ -302,15 +313,6 @@ cl::opt<std::string> ReplayPathFile("replay-path",
                                     cl::value_desc("path file"),
                                     cl::cat(ReplayCat));
 
-cl::list<std::string> SeedOutFile("seed-file",
-                                  cl::desc(".ktest file to be used as seed"),
-                                  cl::cat(SeedingCat));
-
-cl::list<std::string>
-    SeedOutDir("seed-dir",
-               cl::desc("Directory with .ktest files to be used as seeds"),
-               cl::cat(SeedingCat));
-
 cl::opt<unsigned> MakeConcreteSymbolic(
     "make-concrete-symbolic",
     cl::desc("Probabilistic rate at which to make concrete reads symbolic, "
@@ -453,6 +455,9 @@ class KleeHandler : public InterpreterHandler {
   int m_argc;
   char **m_argv;
 
+  int argc() { return m_argc; }
+  char **argv() { return m_argv; }
+
 public:
   KleeHandler(int argc, char **argv);
   ~KleeHandler();
@@ -464,6 +469,8 @@ class KleeHandler : public InterpreterHandler {
   unsigned getNumPathsExplored() { return m_pathsExplored; }
   void incPathsCompleted() { ++m_pathsCompleted; }
   void incPathsExplored(std::uint32_t num = 1) { m_pathsExplored += num; }
+  bool seedToFile(unsigned instructions, unsigned isCompleted, const KTest *bo,
+                  std::string path);
 
   void setInterpreter(Interpreter *i);
 
@@ -484,9 +491,6 @@ class KleeHandler : public InterpreterHandler {
   // load a .path file
   static void loadPathFile(std::string name, std::vector<bool> &buffer);
 
-  static void getKTestFilesInDir(std::string directoryPath,
-                                 std::vector<std::string> &results);
-
   static std::string getRunTimeLibraryPath(const char *argv0);
 
   void setOutputDirectory(const std::string &directory);
@@ -673,6 +677,17 @@ KleeHandler::openTestFile(const std::string &suffix, unsigned id,
   return openOutputFile(getTestFilename(suffix, id, version));
 }
 
+bool KleeHandler::seedToFile(unsigned instructions, unsigned isCompleted,
+                             const KTest *bo, std::string path) {
+  if (!kTest_toFile(bo, (path + "ktest").c_str())) {
+    return false;
+  }
+  std::ofstream out(path + "seedinfo");
+  out << instructions << "\n";
+  out << isCompleted;
+  return true;
+}
+
 /* Outputs all files (.ktest, .kquery, .cov etc.) describing a test case */
 void KleeHandler::processTestCase(const ExecutionState &state,
                                   const char *message, const char *suffix,
@@ -684,12 +699,9 @@ void KleeHandler::processTestCase(const ExecutionState &state,
        (DumpStatesOnHalt == HaltExecution::Reason::UnreachedTarget &&
         m_interpreter->getHaltExecution() ==
             HaltExecution::Reason::UnreachedTarget))) {
-    KTest ktest;
-    ktest.numArgs = m_argc;
-    ktest.args = m_argv;
-    ktest.symArgvs = 0;
-    ktest.symArgvLen = 0;
-
+    KTest *ktest = 0;
+    ktest = new KTest;
+    bool isCompleted = message == nullptr;
     bool success = m_interpreter->getSymbolicSolution(state, ktest);
 
     if (!success)
@@ -699,10 +711,27 @@ void KleeHandler::processTestCase(const ExecutionState &state,
     bool atLeastOneGenerated = false;
 
     if (success) {
-      if (WriteKTests) {
-        for (unsigned i = 0; i < ktest.uninitCoeff + 1; ++i) {
+      if (WriteSeeds) {
+
+        for (unsigned i = 0; i < ktest->uninitCoeff + 1; ++i) {
+          unsigned steppedInstructions;
+          m_interpreter->getSteppedInstructions(state, steppedInstructions);
+          if (!seedToFile(steppedInstructions, isCompleted, ktest,
+                          getOutputFilename(getTestFilename("", id, i)))) {
+            klee_warning("unable to write output test case, losing it");
+          } else {
+            atLeastOneGenerated = true;
+          }
+        }
+
+        if (WriteStates) {
+          auto f = openTestFile("state", id);
+          m_interpreter->logState(state, id, f);
+        }
+      } else if (WriteKTests) {
+        for (unsigned i = 0; i < ktest->uninitCoeff + 1; ++i) {
           if (!kTest_toFile(
-                  &ktest,
+                  ktest,
                   getOutputFilename(getTestFilename("ktest", id, i)).c_str())) {
             klee_warning("unable to write output test case, losing it");
           } else {
@@ -717,17 +746,15 @@ void KleeHandler::processTestCase(const ExecutionState &state,
       }
 
       if (WriteXMLTests) {
-        for (unsigned i = 0; i < ktest.uninitCoeff + 1; ++i) {
-          writeTestCaseXML(message != nullptr, ktest, id, i);
+        for (unsigned i = 0; i < ktest->uninitCoeff + 1; ++i) {
+          writeTestCaseXML(message != nullptr, *ktest, id, i);
           atLeastOneGenerated = true;
         }
       }
 
-      for (unsigned i = 0; i < ktest.numObjects; i++) {
-        delete[] ktest.objects[i].bytes;
-        delete[] ktest.objects[i].pointers;
-      }
-      delete[] ktest.objects;
+      test_kTest_free(ktest);
+    } else {
+      delete ktest;
     }
 
     if (message) {
@@ -915,24 +942,6 @@ void KleeHandler::loadPathFile(std::string name, std::vector<bool> &buffer) {
   }
 }
 
-void KleeHandler::getKTestFilesInDir(std::string directoryPath,
-                                     std::vector<std::string> &results) {
-  std::error_code ec;
-  llvm::sys::fs::directory_iterator i(directoryPath, ec), e;
-  for (; i != e && !ec; i.increment(ec)) {
-    auto f = i->path();
-    if (f.size() >= 6 && f.substr(f.size() - 6, f.size()) == ".ktest") {
-      results.push_back(f);
-    }
-  }
-
-  if (ec) {
-    llvm::errs() << "ERROR: unable to read output directory: " << directoryPath
-                 << ": " << ec.message() << "\n";
-    exit(1);
-  }
-}
-
 std::string KleeHandler::getRunTimeLibraryPath(const char *argv0) {
   // allow specifying the path to the runtime library
   const char *env = getenv("KLEE_RUNTIME_LIBRARY_PATH");
@@ -1529,103 +1538,16 @@ static int run_klee_on_function(int pArgc, char **pArgv, char **pEnvp,
     handler->getInfoStream().flush();
   }
 
-  if (!ReplayKTestDir.empty() || !ReplayKTestFile.empty()) {
-    assert(SeedOutFile.empty());
-    assert(SeedOutDir.empty());
-
-    std::vector<std::string> kTestFiles = ReplayKTestFile;
-    for (std::vector<std::string>::iterator it = ReplayKTestDir.begin(),
-                                            ie = ReplayKTestDir.end();
-         it != ie; ++it)
-      KleeHandler::getKTestFilesInDir(*it, kTestFiles);
-    std::vector<KTest *> kTests;
-    for (std::vector<std::string>::iterator it = kTestFiles.begin(),
-                                            ie = kTestFiles.end();
-         it != ie; ++it) {
-      KTest *out = kTest_fromFile(it->c_str());
-      if (out) {
-        kTests.push_back(out);
-      } else {
-        klee_warning("unable to open: %s\n", (*it).c_str());
-      }
-    }
-
-    if (RunInDir != "") {
-      int res = chdir(RunInDir.c_str());
-      if (res < 0) {
-        klee_error("Unable to change directory to: %s - %s", RunInDir.c_str(),
-                   sys::StrError(errno).c_str());
-      }
-    }
-
-    unsigned i = 0;
-    for (std::vector<KTest *>::iterator it = kTests.begin(), ie = kTests.end();
-         it != ie; ++it) {
-      KTest *out = *it;
-      interpreter->setReplayKTest(out);
-      llvm::errs() << "KLEE: replaying: " << *it << " (" << kTest_numBytes(out)
-                   << " bytes)"
-                   << " (" << ++i << "/" << kTestFiles.size() << ")\n";
-      // XXX should put envp in .ktest ?
-      interpreter->runFunctionAsMain(mainFn, out->numArgs, out->args, pEnvp);
-      if (interrupted)
-        break;
-    }
-    interpreter->setReplayKTest(0);
-    while (!kTests.empty()) {
-      kTest_free(kTests.back());
-      kTests.pop_back();
-    }
-  } else {
-    std::vector<KTest *> seeds;
-    for (std::vector<std::string>::iterator it = SeedOutFile.begin(),
-                                            ie = SeedOutFile.end();
-         it != ie; ++it) {
-      KTest *out = kTest_fromFile(it->c_str());
-      if (!out) {
-        klee_error("unable to open: %s\n", (*it).c_str());
-      }
-      seeds.push_back(out);
-    }
-    for (std::vector<std::string>::iterator it = SeedOutDir.begin(),
-                                            ie = SeedOutDir.end();
-         it != ie; ++it) {
-      std::vector<std::string> kTestFiles;
-      KleeHandler::getKTestFilesInDir(*it, kTestFiles);
-      for (std::vector<std::string>::iterator it2 = kTestFiles.begin(),
-                                              ie = kTestFiles.end();
-           it2 != ie; ++it2) {
-        KTest *out = kTest_fromFile(it2->c_str());
-        if (!out) {
-          klee_error("unable to open: %s\n", (*it2).c_str());
-        }
-        seeds.push_back(out);
-      }
-      if (kTestFiles.empty()) {
-        klee_error("seeds directory is empty: %s\n", (*it).c_str());
-      }
-    }
-
-    if (!seeds.empty()) {
-      klee_message("KLEE: using %lu seeds\n", seeds.size());
-      interpreter->useSeeds(&seeds);
-    }
-    if (RunInDir != "") {
-      int res = chdir(RunInDir.c_str());
-      if (res < 0) {
-        klee_error("Unable to change directory to: %s - %s", RunInDir.c_str(),
-                   sys::StrError(errno).c_str());
-      }
-    }
-
-    interpreter->runFunctionAsMain(mainFn, pArgc, pArgv, pEnvp);
-
-    while (!seeds.empty()) {
-      kTest_free(seeds.back());
-      seeds.pop_back();
+  if (RunInDir != "") {
+    int res = chdir(RunInDir.c_str());
+    if (res < 0) {
+      klee_error("Unable to change directory to: %s - %s", RunInDir.c_str(),
+                 sys::StrError(errno).c_str());
     }
   }
 
+  interpreter->runFunctionAsMain(mainFn, pArgc, pArgv, pEnvp);
+
   auto endTime = std::time(nullptr);
   { // output end and elapsed time
     std::uint32_t h;