diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml
index 31053ee2ec..a679c4e4b8 100644
--- a/.github/workflows/build.yaml
+++ b/.github/workflows/build.yaml
@@ -5,7 +5,7 @@ on:
   pull_request:
     branches: [main, utbot-main]
   push:
-   branches: [main, utbot-main, testheheh]
+    branches: [main, utbot-main, testheheh]
   workflow_dispatch:
     inputs:
       warnings_as_errors:
diff --git a/include/klee/ADT/KTest.h b/include/klee/ADT/KTest.h
index e540b9941d..d8a0d87ac1 100644
--- a/include/klee/ADT/KTest.h
+++ b/include/klee/ADT/KTest.h
@@ -66,7 +66,7 @@ unsigned kTest_numBytes(KTest *);
 
 void kTest_free(KTest *);
 
-unsigned getkTestMemoryUsage(KTest *ktest);
+unsigned getKTestMemoryUsage(KTest *ktest);
 #ifdef __cplusplus
 }
 #endif
diff --git a/include/klee/ADT/SeedFromFile.h b/include/klee/ADT/SeedFromFile.h
new file mode 100644
index 0000000000..8f13220d6a
--- /dev/null
+++ b/include/klee/ADT/SeedFromFile.h
@@ -0,0 +1,19 @@
+#ifndef KLEE_SEED_FROM_FILE_H
+#include <string>
+
+class KTest;
+
+namespace klee {
+
+class SeedFromFile {
+public:
+  KTest *ktest;
+  unsigned maxInstructions;
+
+  SeedFromFile() {}
+  SeedFromFile(std::string _path);
+};
+
+} // namespace klee
+#define KLEE_SEED_FROM_FILE_H
+#endif
\ No newline at end of file
diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h
index fdb695fc1a..93e5a6dddb 100644
--- a/include/klee/Core/Interpreter.h
+++ b/include/klee/Core/Interpreter.h
@@ -10,6 +10,7 @@
 #define KLEE_INTERPRETER_H
 
 #include "TerminationTypes.h"
+#include "klee/ADT/SeedFromFile.h"
 #include "klee/Module/Annotation.h"
 
 #include "klee/Module/SarifReport.h"
@@ -58,11 +59,8 @@ 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;
+  virtual ToolJson info() const = 0;
 };
 
 /// [File][Line][Column] -> Opcode
@@ -212,6 +210,10 @@ 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(std::vector<SeedFromFile> seeds) = 0;
+
   virtual void runFunctionAsMain(llvm::Function *f, int argc, char **argv,
                                  char **envp) = 0;
 
@@ -239,7 +241,7 @@ class Interpreter {
   virtual void getSteppedInstructions(const ExecutionState &state,
                                       unsigned &res) = 0;
 
-  virtual bool getSymbolicSolution(const ExecutionState &state, KTest *res) = 0;
+  virtual bool getSymbolicSolution(const ExecutionState &state, KTest &res) = 0;
 
   virtual void addSARIFReport(const ExecutionState &state) = 0;
 
diff --git a/lib/ADT/CMakeLists.txt b/lib/ADT/CMakeLists.txt
index f013a88af4..07eaf524c2 100644
--- a/lib/ADT/CMakeLists.txt
+++ b/lib/ADT/CMakeLists.txt
@@ -8,6 +8,7 @@
 #===------------------------------------------------------------------------===#
 add_library(kleeADT
   SparseStorage.cpp
+  SeedFromFile.cpp
 )
 
 llvm_config(kleeADT "${USE_LLVM_SHARED}" support)
diff --git a/lib/ADT/SeedFromFile.cpp b/lib/ADT/SeedFromFile.cpp
new file mode 100644
index 0000000000..3d3c36a068
--- /dev/null
+++ b/lib/ADT/SeedFromFile.cpp
@@ -0,0 +1,14 @@
+#include "klee/ADT/SeedFromFile.h"
+#include "klee/ADT/KTest.h"
+
+#include <fstream>
+
+using namespace klee;
+
+SeedFromFile::SeedFromFile(std::string _path)
+    : ktest(kTest_fromFile((_path + "ktest").c_str())) {
+  std::ifstream seedInfoStream(_path + "seedinfo");
+  if (seedInfoStream.good()) {
+    seedInfoStream >> maxInstructions;
+  }
+}
\ No newline at end of file
diff --git a/lib/Basic/KTest.cpp b/lib/Basic/KTest.cpp
index 1f2f8c1f3b..dd39ea083a 100644
--- a/lib/Basic/KTest.cpp
+++ b/lib/Basic/KTest.cpp
@@ -13,7 +13,6 @@
 #include <cstdio>
 #include <cstdlib>
 #include <cstring>
-#include <fstream>
 
 #define KTEST_VERSION 4
 #define KTEST_MAGIC_SIZE 5
@@ -297,7 +296,7 @@ void kTest_free(KTest *bo) {
   free(bo);
 }
 
-unsigned getkTestMemoryUsage(KTest *ktest) {
+unsigned getKTestMemoryUsage(KTest *ktest) {
   size_t size = 0;
   for (unsigned i = 0; i < ktest->numObjects; i++) {
     size += std::strlen(ktest->objects[i].name) * sizeof(char);
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index b8fdd64fde..5f6e0dd02f 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -229,6 +229,12 @@ cl::opt<HaltExecution::Reason> DumpStatesOnHalt(
         clEnumValN(HaltExecution::Reason::Unspecified, "all",
                    "Dump test cases for all active states on exit (default)")),
     cl::cat(TestGenCat));
+
+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));
+
 } // namespace klee
 
 namespace {
@@ -347,27 +353,6 @@ cl::opt<ExtCallWarnings> ExternalCallWarnings(
 
 /*** 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("Partially executed states are stored "
-                                         "locally as ktests (default=false)"),
-                                cl::init(false), cl::cat(SeedingCat));
-
-cl::opt<bool> ExploreCompletedSeeds(
-    "explore-completed-seeds",
-    cl::desc("Explore seeds created from completed paths (default=true)"),
-    cl::init(true), 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<unsigned> UploadPercentage(
     "upload-percentage",
     cl::desc(
@@ -381,9 +366,6 @@ cl::opt<bool> AlwaysOutputSeeds(
         "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)."),
@@ -421,15 +403,6 @@ cl::opt<std::string>
              cl::desc("Amount of time to dedicate to seeds, before normal "
                       "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 ***/
@@ -1191,11 +1164,14 @@ void Executor::initializeGlobalObjects(ExecutionState &state) {
 
 bool Executor::branchingPermitted(ExecutionState &state, unsigned N) {
   assert(N);
-  if ((MaxMemoryInhibit && atMemoryLimit && !state.isSeeded) ||
+  if (state.isSeeded) {
+    return true;
+  }
+  if ((MaxMemoryInhibit && atMemoryLimit) ||
       state.forkDisabled || inhibitForking ||
       (MaxForks != ~0u && stats::forks >= MaxForks)) {
 
-    if (MaxMemoryInhibit && atMemoryLimit && !state.isSeeded)
+    if (MaxMemoryInhibit && atMemoryLimit)
       klee_warning_once(0, "skipping fork (memory cap exceeded)");
     else if (state.forkDisabled)
       klee_warning_once(0, "skipping fork (fork disabled on current path)");
@@ -1278,7 +1254,6 @@ void Executor::branch(ExecutionState &state,
 
       // Extra check in case we're replaying seeds with a max-fork
       if (result[i]) {
-        objectManager->seed(result[i]);
         seedMap->at(result[i]).push_back(*siit);
       }
     }
@@ -1396,6 +1371,7 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
   }
 
   if (!isSeeding) {
+    assert(seedMap->empty());
     if (replayPath && !isInternal) {
       assert(replayPosition < replayPath->size() &&
              "ran out of branches in replay path mode");
@@ -1615,33 +1591,6 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
     return;
   }
 
-  // Check to see if this constraint violates seeds.
-  if (PatchSeeds && state.isSeeded) {
-    std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
-        seedMap->find(&state);
-    assert(it != seedMap->end());
-    assert(!it->second.empty());
-    bool warn = false;
-    for (std::vector<ExecutingSeed>::iterator siit = it->second.begin(),
-                                              siie = it->second.end();
-         siit != siie; ++siit) {
-      bool res;
-      solver->setTimeout(coreSolverTimeout);
-      bool success = solver->mustBeFalse(state.constraints.cs(),
-                                         siit->assignment.evaluate(condition),
-                                         res, state.queryMetaData);
-      solver->setTimeout(time::Span());
-      assert(success && "FIXME: Unhandled solver failure");
-      (void)success;
-      if (res) {
-        siit->patchSeed(state, condition, solver.get());
-        warn = true;
-      }
-    }
-    if (warn)
-      klee_warning("seeds patched for violating constraint");
-  }
-
   state.addConstraint(condition);
 
   if (ivcEnabled)
@@ -4590,87 +4539,23 @@ const KFunction *Executor::getKFunction(const llvm::Function *f) const {
   return (kfIt == kmodule->functionMap.end()) ? nullptr : kfIt->second;
 }
 
-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);
-    }
-  }
-
-  if (ec) {
-    llvm::errs() << "ERROR: unable to read output directory: " << directoryPath
-                 << ": " << ec.message() << "\n";
-    exit(1);
-  }
-}
-
 std::vector<ExecutingSeed> Executor::uploadNewSeeds() {
   std::vector<ExecutingSeed> seeds;
-  //FIX: experimental option + storedseedslocally behaviour (yes, no, mixed)
-  unsigned toUpload = UploadAmount;
-  if(UploadPercentage){
-    toUpload = (storedSeeds->size() * UploadPercentage) / 100;
-    if(toUpload == 0) toUpload = 1;
-  }
-  if (StoreSeedsLocally) {
-    while ((!toUpload || seeds.size() <= toUpload) &&
-           !storedSeeds->empty()) {
-      if (ExploreCompletedSeeds || !storedSeeds->front().isCompleted) {
-        seeds.push_back(storedSeeds->front());
-      }
-      storedSeeds->pop_front();
-    }
+  if(!usingInitialSeeds.empty()){
+    seeds = usingInitialSeeds;
+    usingInitialSeeds.clear();
     return seeds;
   }
 
-  if (toUpload && seeds.size() >= toUpload) {
-    return seeds;
+  unsigned toUpload = 0;
+  if(UploadPercentage){
+    toUpload = (storedSeeds->size() * UploadPercentage) / 100;
+    if(toUpload == 0) toUpload = 1;
   }
 
-  for (std::vector<std::string>::iterator it = SeedOutFile.begin(),
-                                          ie = SeedOutFile.end();
-       it != ie && (!toUpload || seeds.size() <= toUpload); ++it) {
-    ExecutingSeed out(it->substr(0, it->size() - 5));
-    if (!out.input) {
-      klee_error("unable to open: %s\n", (*it).c_str());
-    } else if (ExploreCompletedSeeds || !out.isCompleted) {
-      seeds.push_back(out);
-    }
-  }
-
-  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 && (!toUpload || seeds.size() <= toUpload); ++it2) {
-      ExecutingSeed out(it2->substr(0, it2->size() - 5));
-      if (!out.input) {
-        klee_error("unable to open: %s\n", (*it2).c_str());
-      } else if (ExploreCompletedSeeds || !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());
-      std::remove((it.path + "xml").c_str());
-    }
+  while ((!toUpload || seeds.size() <= toUpload) && !storedSeeds->empty()) {
+    seeds.push_back(storedSeeds->front());
+    storedSeeds->pop_front();
   }
   return seeds;
 }
@@ -4693,8 +4578,7 @@ void Executor::initialSeed(ExecutionState &initialState,
   objectManager->updateSubscribers();
 }
 
-bool Executor::storeState(const ExecutionState &state, bool isCompleted,
-                          ExecutingSeed &res) {
+bool Executor::storeState(const ExecutionState &state, ExecutingSeed &res) {
   ref<SolverResponse> response;
   bool success =
       solver->getResponse(state.constraints.cs(), Expr::createFalse(), response,
@@ -4708,8 +4592,8 @@ bool Executor::storeState(const ExecutionState &state, bool isCompleted,
     assert(false && "terminated state must have an assignment");
     return false;
   }
-  ExecutingSeed seed(assignment, state.steppedInstructions, isCompleted,
-                     state.coveredNew, state.coveredNewError);
+  ExecutingSeed seed(assignment, state.steppedInstructions, state.coveredNew,
+                     state.coveredNewError);
   res = seed;
   return true;
 }
@@ -4882,7 +4766,9 @@ bool Executor::reachedMaxSeedInstructions(ExecutionState *state) {
 
   std::vector<ExecutingSeed>::iterator siit = it->second.begin();
   if (siit->maxInstructions &&
-      siit->maxInstructions >= state->steppedInstructions) {
+      siit->maxInstructions <= state->steppedInstructions) {
+    assert(siit->maxInstructions == state->steppedInstructions &&
+           "state stepped instructions exceeded seed max instructions");
     state->coveredNew = siit->coveredNew;
     if (siit->coveredNewError) {
       state->coveredNewError = siit->coveredNewError;
@@ -5079,15 +4965,15 @@ void Executor::terminateStateEarly(ExecutionState &state, const Twine &message,
     assert(reason > StateTerminationType::EXIT);
     ++stats::terminationEarly;
   }
-  if ((RunForever && reason == StateTerminationType::OutOfMemory) ||
+  if ((RunForever && (reason <= StateTerminationType::EARLY)) ||
       ((reason <= StateTerminationType::EARLY ||
         reason == StateTerminationType::MissedAllTargets) &&
        shouldWriteTest(state)) ||
       (AlwaysOutputSeeds && seedMap->count(&state))) {
     state.clearCoveredNew();
-    if (StoreSeedsLocally) {
+    if (RunForever && (reason <= StateTerminationType::EARLY) ) {
       ExecutingSeed seed;
-      bool success = storeState(state, !(reason <= StateTerminationType::EARLY), seed);
+      bool success = storeState(state, seed);
       if (success) {
         storedSeeds->push_back(seed);
       }
@@ -7553,7 +7439,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);
@@ -7734,18 +7620,11 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest *res) {
     }
   }
 
-  res->numArgs = interpreterHandler->argc();
-  res->args = (char **)calloc(res->numArgs, sizeof(*res->args));
-  for (unsigned i = 0; i < res->numArgs; i++) {
-    unsigned argsize = std::strlen(interpreterHandler->argv()[i]);
-    res->args[i] = (char *)calloc(argsize + 1, sizeof(*res->args[i]));
-    std::strcpy(res->args[i], interpreterHandler->argv()[i]);
-  }
-  res->symArgvs = 0;
-  res->symArgvLen = 0;
-  res->numObjects = symbolics.size();
-  res->objects = (KTestObject *)calloc(res->numObjects, sizeof(*res->objects));
-  res->uninitCoeff = uninitObjects.size() * UninitMemoryTestMultiplier;
+  res.symArgvs = 0;
+  res.symArgvLen = 0;
+  res.numObjects = symbolics.size();
+  res.objects = (KTestObject *)calloc(res.numObjects, sizeof(*res.objects));
+  res.uninitCoeff = uninitObjects.size() * UninitMemoryTestMultiplier;
 
   {
     size_t i = 0;
@@ -7753,7 +7632,7 @@ 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];
+      KTestObject *o = &res.objects[i];
       o->name = (char *)calloc(mo->name.size() + 1, sizeof(*o->name));
       std::strcpy(o->name, mo->name.c_str());
       o->address = cast<ConstantExpr>(evaluator.visit(mo->getBaseExpr()))
@@ -7770,7 +7649,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest *res) {
     }
   }
 
-  setInitializationGraph(state, symbolics, model, *res);
+  setInitializationGraph(state, symbolics, model, res);
 
   return true;
 }
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 7cd39d5062..8fd064af05 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -199,6 +199,10 @@ class Executor : public Interpreter {
   /// object.
   unsigned replayPosition;
 
+  /// When non-null a list of "seed" inputs which will be used to
+  /// drive execution.
+  std::vector<ExecutingSeed> usingInitialSeeds;
+
   /// Disables forking, instead a random path is chosen. Enabled as
   /// needed to control memory usage. \see fork()
   bool atMemoryLimit;
@@ -260,16 +264,11 @@ class Executor : public Interpreter {
 
   void executeInstruction(ExecutionState &state, KInstruction *ki);
 
-  states_ty &getSeedChanges() { return objectManager->getSeedChanges(); }
-
-  void getKTestFilesInDir(std::string directoryPath,
-                          std::vector<std::string> &results);
   std::vector<ExecutingSeed> uploadNewSeeds();
   void initialSeed(ExecutionState &initialState,
                    std::vector<ExecutingSeed> usingSeeds);
 
-  bool storeState(const ExecutionState &state, bool isCompleted,
-                           ExecutingSeed &res);
+  bool storeState(const ExecutionState &state, ExecutingSeed &res);
 
   void run(ExecutionState *initialState);
 
@@ -782,6 +781,13 @@ class Executor : public Interpreter {
 
   void setFunctionsByModule(FunctionsByModule &&functionsByModule) override;
 
+  void useSeeds(std::vector<SeedFromFile> seeds) override {
+    for (SeedFromFile seed : seeds) {
+      usingInitialSeeds.push_back(
+          ExecutingSeed(seed.ktest, seed.maxInstructions));
+    }
+  }
+
   ExecutionState *formState(llvm::Function *f);
   ExecutionState *formState(llvm::Function *f, int argc, char **argv,
                             char **envp);
@@ -850,7 +856,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;
diff --git a/lib/Core/ObjectManager.cpp b/lib/Core/ObjectManager.cpp
index 13bf6229c6..cef9b1e4e6 100644
--- a/lib/Core/ObjectManager.cpp
+++ b/lib/Core/ObjectManager.cpp
@@ -26,10 +26,6 @@ void ObjectManager::removeInitialState(ExecutionState *state) {
   delete state;
 }
 
-void ObjectManager::addFirstState(ExecutionState *state) {
-  states.insert(state);
-}
-
 void ObjectManager::setCurrentState(ExecutionState *_current) {
   assert(current == nullptr);
   current = _current;
@@ -59,20 +55,16 @@ void ObjectManager::removeState(ExecutionState *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);
@@ -93,7 +85,6 @@ 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 06ee689b76..0bfaa8cc58 100644
--- a/lib/Core/ObjectManager.h
+++ b/lib/Core/ObjectManager.h
@@ -54,7 +54,6 @@ class ObjectManager {
 
   void addInitialState(ExecutionState *state);
   void removeInitialState(ExecutionState *state);
-  void addFirstState(ExecutionState *state);
 
   void setCurrentState(ExecutionState *_current);
 
@@ -64,11 +63,6 @@ class ObjectManager {
   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();
@@ -89,8 +83,6 @@ 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 3c2c8943e4..87bc49d10c 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -657,8 +657,8 @@ class MaxCyclesMetric final : public IterativeDeepeningSearcher::Metric {
   ty maxCycles;
 
 public:
-  explicit MaxCyclesMetric(ty maxCycles) : maxCycles(maxCycles){};
-  explicit MaxCyclesMetric() : MaxCyclesMetric(1ULL){};
+  explicit MaxCyclesMetric(ty maxCycles) : maxCycles(maxCycles) {};
+  explicit MaxCyclesMetric() : MaxCyclesMetric(1ULL) {};
 
   bool exceeds(const ExecutionState &state) const final {
     return state.isCycled(maxCycles);
@@ -920,13 +920,11 @@ void DiscreteTimeFairSearcher::printName(llvm::raw_ostream &os) {
 
 //
 
-SeededSearcher::SeededSearcher(Searcher *_searcher, states_ty &_seedChanges)
-    : baseSearcher(_searcher), seedChanges(_seedChanges) {
+SeededSearcher::SeededSearcher(Searcher *_searcher) : baseSearcher(_searcher) {
   seededSearcher = std::unique_ptr<BFSSearcher>(new BFSSearcher());
 }
 
 ExecutionState &SeededSearcher::selectState() {
-  update(nullptr, {}, {});
   if (!seededSearcher->empty()) {
     return seededSearcher->selectState();
   }
@@ -936,30 +934,34 @@ ExecutionState &SeededSearcher::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;
+
+  // process seed/unseed of current
+  if (current) {
+    if (current->isSeeded) {
+      if (baseSearcherStates.count(current) != 0) {
+        baseSearcherStates.erase(current);
+        baseSearcher->update(nullptr, {}, {current});
+      }
+      if (seededSearcherStates.count(current) == 0) {
+        seededSearcherStates.insert(current);
+        seededSearcher->update(nullptr, {current}, {});
+      }
+    } else {
+      if (seededSearcherStates.count(current) != 0) {
+        seededSearcherStates.erase(current);
+        seededSearcher->update(nullptr, {}, {current});
+      }
+      if (baseSearcherStates.count(current) == 0) {
+        baseSearcherStates.insert(current);
+        baseSearcher->update(nullptr, {current}, {});
+      }
+    }
+  }
+
   for (auto state : addedStates) {
     if (state->isSeeded && seededSearcherStates.count(state) == 0) {
       addedSeededStates.push_back(state);
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index 25e35ef310..fc868bb23e 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -423,12 +423,11 @@ class DiscreteTimeFairSearcher final : public Searcher {
 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);
+  explicit SeededSearcher(Searcher *_searcher);
 
   ExecutionState &selectState() override;
 
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index b1934ccefa..4f099de3f2 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -1,5 +1,4 @@
-//===-- ExecutingSeed.cpp
-//------------------------------------------------------===//
+//===-- SeedInfo.cpp ------------------------------------------------------===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -19,22 +18,11 @@
 #include "klee/Expr/ExprUtil.h"
 #include "klee/Support/ErrorHandling.h"
 
-#include <fstream>
 #include <set>
 
 using namespace klee;
 
-void ExecutingSeed::kTestDeleter(KTest *kTest) { kTest_free(kTest); }
-
-ExecutingSeed::ExecutingSeed(std::string _path)
-    : input(kTest_fromFile((_path + "ktest").c_str()), kTestDeleter),
-      path(_path) {
-  std::ifstream seedInfoStream(_path + "seedinfo");
-  if (seedInfoStream.good()) {
-    seedInfoStream >> maxInstructions;
-    seedInfoStream >> isCompleted;
-  }
-}
+void ExecutingSeed::kTestDeleter(KTest *ktest) { kTest_free(ktest); }
 
 KTestObject *ExecutingSeed::getNextInput(const MemoryObject *mo, bool byName) {
   if (!input)
@@ -79,111 +67,3 @@ KTestObject *ExecutingSeed::getNextInput(const MemoryObject *mo, bool byName) {
     }
   }
 }
-
-void ExecutingSeed::patchSeed(const ExecutionState &state, ref<Expr> condition,
-                              TimingSolver *solver) {
-  ConstraintSet required = state.constraints.cs();
-  required.addConstraint(condition);
-
-  // Try and patch direct reads first, this is likely to resolve the
-  // problem quickly and avoids long traversal of all seed
-  // values. There are other smart ways to do this, the nicest is if
-  // we got a minimal counterexample from STP, in which case we would
-  // just inject those values back into the seed.
-  std::set<std::pair<const Array *, unsigned>> directReads;
-  std::vector<ref<ReadExpr>> reads;
-  findReads(condition, false, reads);
-  for (const auto &re : reads) {
-    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
-      directReads.insert(
-          std::make_pair(re->updates.root, (unsigned)CE->getZExtValue(32)));
-    }
-  }
-
-  for (const auto &[array, i] : directReads) {
-    ref<Expr> read = ReadExpr::create(UpdateList(array, 0),
-                                      ConstantExpr::alloc(i, Expr::Int32));
-
-    // If not in bindings then this can't be a violation?
-    Assignment::bindings_ty::iterator it2 = assignment.bindings.find(array);
-    if (it2 != assignment.bindings.end()) {
-      ref<Expr> isSeed = EqExpr::create(
-          read, ConstantExpr::alloc(it2->second.load(i), Expr::Int8));
-      bool res;
-      bool success =
-          solver->mustBeFalse(required, isSeed, res, state.queryMetaData);
-      assert(success && "FIXME: Unhandled solver failure");
-      (void)success;
-      if (res) {
-        ref<ConstantExpr> value;
-        bool success =
-            solver->getValue(required, read, value, state.queryMetaData);
-        assert(success && "FIXME: Unhandled solver failure");
-        (void)success;
-        auto s = it2->second;
-        s.store(i, value->getZExtValue(8));
-        assignment.bindings.replace({it2->first, s});
-        required.addConstraint(EqExpr::create(
-            read, ConstantExpr::alloc(it2->second.load(i), Expr::Int8)));
-      } else {
-        required.addConstraint(isSeed);
-      }
-    }
-  }
-
-  bool res;
-  bool success =
-      solver->mayBeTrue(state.constraints.cs(), assignment.evaluate(condition),
-                        res, state.queryMetaData);
-  assert(success && "FIXME: Unhandled solver failure");
-  (void)success;
-  if (res)
-    return;
-
-  // We could still do a lot better than this, for example by looking at
-  // independence. But really, this shouldn't be happening often.
-  for (Assignment::bindings_ty::iterator it = assignment.bindings.begin(),
-                                         ie = assignment.bindings.end();
-       it != ie; ++it) {
-    const Array *array = it->first;
-    ref<ConstantExpr> arrayConstantSize =
-        cast<ConstantExpr>(assignment.evaluate(array->size));
-    for (unsigned i = 0; i < arrayConstantSize->getZExtValue(); ++i) {
-      ref<Expr> read = ReadExpr::create(UpdateList(array, 0),
-                                        ConstantExpr::alloc(i, Expr::Int32));
-      ref<Expr> isSeed = EqExpr::create(
-          read, ConstantExpr::alloc(it->second.load(i), Expr::Int8));
-      bool res;
-      bool success =
-          solver->mustBeFalse(required, isSeed, res, state.queryMetaData);
-      assert(success && "FIXME: Unhandled solver failure");
-      (void)success;
-      if (res) {
-        ref<ConstantExpr> value;
-        bool success =
-            solver->getValue(required, read, value, state.queryMetaData);
-        assert(success && "FIXME: Unhandled solver failure");
-        (void)success;
-        auto s = it->second;
-        s.store(i, value->getZExtValue(8));
-        assignment.bindings.replace({it->first, s});
-        required.addConstraint(EqExpr::create(
-            read, ConstantExpr::alloc(it->second.load(i), Expr::Int8)));
-      } else {
-        required.addConstraint(isSeed);
-      }
-    }
-  }
-
-#ifndef NDEBUG
-  {
-    bool res;
-    bool success = solver->mayBeTrue(state.constraints.cs(),
-                                     assignment.evaluate(condition), res,
-                                     state.queryMetaData);
-    assert(success && "FIXME: Unhandled solver failure");
-    (void)success;
-    assert(res && "seed patching failed");
-  }
-#endif
-}
diff --git a/lib/Core/SeedInfo.h b/lib/Core/SeedInfo.h
index fc9349bbfc..c276d3e2d7 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
 //
@@ -30,9 +30,7 @@ class ExecutingSeed {
   Assignment assignment;
   std::shared_ptr<KTest> input;
   unsigned maxInstructions = 0;
-  bool isCompleted = 0;
   std::set<struct KTestObject *> used;
-  std::string path = "";
   mutable std::deque<ref<box<bool>>> coveredNew;
   mutable ref<box<bool>> coveredNewError = nullptr;
   unsigned inputPosition = 0;
@@ -43,31 +41,20 @@ class ExecutingSeed {
   ExecutingSeed() {}
 
   explicit ExecutingSeed(KTest *input, unsigned maxInstructions,
-                         bool isCompleted,
-                         std::deque<ref<box<bool>>> coveredNew,
-                         ref<box<bool>> coveredNewError)
+                         std::deque<ref<box<bool>>> coveredNew = {},
+                         ref<box<bool>> coveredNewError = 0)
       : input(input, kTestDeleter), maxInstructions(maxInstructions),
-        isCompleted(isCompleted), coveredNew(coveredNew),
-        coveredNewError(coveredNewError) {}
+        coveredNew(coveredNew), coveredNewError(coveredNewError) {}
 
   explicit ExecutingSeed(Assignment assignment, unsigned maxInstructions,
-                         bool isCompleted,
                          std::deque<ref<box<bool>>> coveredNew,
                          ref<box<bool>> coveredNewError)
       : assignment(assignment), maxInstructions(maxInstructions),
-        isCompleted(isCompleted), coveredNew(coveredNew),
-        coveredNewError(coveredNewError) {}
-
-  ExecutingSeed(std::string _path);
+        coveredNew(coveredNew), coveredNewError(coveredNewError) {}
 
   KTestObject *getNextInput(const MemoryObject *mo, bool byName);
 
-  static void kTestDeleter(KTest *kTest);
-
-  /// Patch the seed so that condition is satisfied while retaining as
-  /// many of the seed values as possible.
-  void patchSeed(const ExecutionState &state, ref<Expr> condition,
-                 TimingSolver *solver);
+  static void kTestDeleter(KTest *ktest);
 };
 } // namespace klee
 
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index 887635e459..c98f17d6e4 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -16,6 +16,8 @@
 
 #include "llvm/Support/CommandLine.h"
 
+#include <string>
+
 using namespace llvm;
 using namespace klee;
 
@@ -68,12 +70,6 @@ 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 "
@@ -95,6 +91,12 @@ cl::opt<bool> UseFairSearch(
 
 } // namespace klee
 
+namespace klee {
+extern cl::opt<bool> RunForever;
+extern cl::list<std::string> SeedOutFile;
+extern cl::list<std::string> SeedOutDir;
+} // namespace klee
+
 void klee::initializeSearchOptions() {
   // default values
   if (CoreSearch.empty()) {
@@ -205,12 +207,9 @@ Searcher *klee::constructUserSearcher(Executor &executor) {
   } else {
     searcher = constructBaseSearcher(executor);
   }
-
-  if (UseSeededSearch) {
-    states_ty &seedChandes = executor.getSeedChanges();
-    searcher = new SeededSearcher(searcher, seedChandes);
+  if(RunForever){
+    searcher = new SeededSearcher(searcher);
   }
-
   llvm::raw_ostream &os = executor.getHandler().getInfoStream();
 
   os << "BEGIN searcher description\n";
diff --git a/scripts/kleef b/scripts/kleef
index e55f46bc76..afcd5c3038 100755
--- a/scripts/kleef
+++ b/scripts/kleef
@@ -66,12 +66,8 @@ def klee_options(
         "--memory-backend=mixed",
         "--max-fixed-size-structures-size=64",
     ]
-    if True:
+    if run_forever:
         cmd += [
-            f"--seed-dir={test_output_dir}",
-            "--use-seeded-search",
-            "--explore-completed-seeds=false",
-            "--store-seeds-locally",
             "--run-forever"
             "--upload-percentage=50"
         ]
@@ -198,7 +194,7 @@ class KLEEF(object):
         use_perf=False,
         use_valgrind=False,
         write_ktests=False,
-        run_forever=False
+        run_forever=True,
     ):
         self.source = Path(source) if source else None
         self.is32 = is32
diff --git a/test/Feature/Dubois-025.c b/test/Feature/Dubois-025.c
deleted file mode 100644
index 99807c007f..0000000000
--- a/test/Feature/Dubois-025.c
+++ /dev/null
@@ -1,543 +0,0 @@
-// It requires bitwuzla because the script currently runs with bitwuzla solver backend
-// REQUIRES: bitwuzla
-// REQUIRES: target-x86_64
-// RUN: %kleef --property-file=%S/coverage-branches.prp --max-memory=7000000000 --max-cputime-soft=90 --32 --write-ktests %s 2>&1 | FileCheck %s
-
-
-// This file is part of the SV-Benchmarks collection of verification tasks:
-// https://github.com/sosy-lab/sv-benchmarks
-//
-// SPDX-FileCopyrightText: 2016 Gilles Audemard
-// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
-// SPDX-FileCopyrightText: 2020 The SV-Benchmarks Community
-//
-// SPDX-License-Identifier: MIT
-
-extern void abort(void) __attribute__((__nothrow__, __leaf__))
-__attribute__((__noreturn__));
-extern void __assert_fail(const char *, const char *, unsigned int,
-                          const char *) __attribute__((__nothrow__, __leaf__))
-__attribute__((__noreturn__));
-int __VERIFIER_nondet_int();
-void reach_error() { __assert_fail("0", "Dubois-025.c", 5, "reach_error"); }
-void assume(int cond) {
-  if (!cond)
-    abort();
-}
-int main() {
-  int cond0;
-  int dummy = 0;
-  int N;
-  int var0;
-  var0 = __VERIFIER_nondet_int();
-  assume(var0 >= 0);
-  assume(var0 <= 1);
-  int var1;
-  var1 = __VERIFIER_nondet_int();
-  assume(var1 >= 0);
-  assume(var1 <= 1);
-  int var2;
-  var2 = __VERIFIER_nondet_int();
-  assume(var2 >= 0);
-  assume(var2 <= 1);
-  int var3;
-  var3 = __VERIFIER_nondet_int();
-  assume(var3 >= 0);
-  assume(var3 <= 1);
-  int var4;
-  var4 = __VERIFIER_nondet_int();
-  assume(var4 >= 0);
-  assume(var4 <= 1);
-  int var5;
-  var5 = __VERIFIER_nondet_int();
-  assume(var5 >= 0);
-  assume(var5 <= 1);
-  int var6;
-  var6 = __VERIFIER_nondet_int();
-  assume(var6 >= 0);
-  assume(var6 <= 1);
-  int var7;
-  var7 = __VERIFIER_nondet_int();
-  assume(var7 >= 0);
-  assume(var7 <= 1);
-  int var8;
-  var8 = __VERIFIER_nondet_int();
-  assume(var8 >= 0);
-  assume(var8 <= 1);
-  int var9;
-  var9 = __VERIFIER_nondet_int();
-  assume(var9 >= 0);
-  assume(var9 <= 1);
-  int var10;
-  var10 = __VERIFIER_nondet_int();
-  assume(var10 >= 0);
-  assume(var10 <= 1);
-  int var11;
-  var11 = __VERIFIER_nondet_int();
-  assume(var11 >= 0);
-  assume(var11 <= 1);
-  int var12;
-  var12 = __VERIFIER_nondet_int();
-  assume(var12 >= 0);
-  assume(var12 <= 1);
-  int var13;
-  var13 = __VERIFIER_nondet_int();
-  assume(var13 >= 0);
-  assume(var13 <= 1);
-  int var14;
-  var14 = __VERIFIER_nondet_int();
-  assume(var14 >= 0);
-  assume(var14 <= 1);
-  int var15;
-  var15 = __VERIFIER_nondet_int();
-  assume(var15 >= 0);
-  assume(var15 <= 1);
-  int var16;
-  var16 = __VERIFIER_nondet_int();
-  assume(var16 >= 0);
-  assume(var16 <= 1);
-  int var17;
-  var17 = __VERIFIER_nondet_int();
-  assume(var17 >= 0);
-  assume(var17 <= 1);
-  int var18;
-  var18 = __VERIFIER_nondet_int();
-  assume(var18 >= 0);
-  assume(var18 <= 1);
-  int var19;
-  var19 = __VERIFIER_nondet_int();
-  assume(var19 >= 0);
-  assume(var19 <= 1);
-  int var20;
-  var20 = __VERIFIER_nondet_int();
-  assume(var20 >= 0);
-  assume(var20 <= 1);
-  int var21;
-  var21 = __VERIFIER_nondet_int();
-  assume(var21 >= 0);
-  assume(var21 <= 1);
-  int var22;
-  var22 = __VERIFIER_nondet_int();
-  assume(var22 >= 0);
-  assume(var22 <= 1);
-  int var23;
-  var23 = __VERIFIER_nondet_int();
-  assume(var23 >= 0);
-  assume(var23 <= 1);
-  int var24;
-  var24 = __VERIFIER_nondet_int();
-  assume(var24 >= 0);
-  assume(var24 <= 1);
-  int var25;
-  var25 = __VERIFIER_nondet_int();
-  assume(var25 >= 0);
-  assume(var25 <= 1);
-  int var26;
-  var26 = __VERIFIER_nondet_int();
-  assume(var26 >= 0);
-  assume(var26 <= 1);
-  int var27;
-  var27 = __VERIFIER_nondet_int();
-  assume(var27 >= 0);
-  assume(var27 <= 1);
-  int var28;
-  var28 = __VERIFIER_nondet_int();
-  assume(var28 >= 0);
-  assume(var28 <= 1);
-  int var29;
-  var29 = __VERIFIER_nondet_int();
-  assume(var29 >= 0);
-  assume(var29 <= 1);
-  int var30;
-  var30 = __VERIFIER_nondet_int();
-  assume(var30 >= 0);
-  assume(var30 <= 1);
-  int var31;
-  var31 = __VERIFIER_nondet_int();
-  assume(var31 >= 0);
-  assume(var31 <= 1);
-  int var32;
-  var32 = __VERIFIER_nondet_int();
-  assume(var32 >= 0);
-  assume(var32 <= 1);
-  int var33;
-  var33 = __VERIFIER_nondet_int();
-  assume(var33 >= 0);
-  assume(var33 <= 1);
-  int var34;
-  var34 = __VERIFIER_nondet_int();
-  assume(var34 >= 0);
-  assume(var34 <= 1);
-  int var35;
-  var35 = __VERIFIER_nondet_int();
-  assume(var35 >= 0);
-  assume(var35 <= 1);
-  int var36;
-  var36 = __VERIFIER_nondet_int();
-  assume(var36 >= 0);
-  assume(var36 <= 1);
-  int var37;
-  var37 = __VERIFIER_nondet_int();
-  assume(var37 >= 0);
-  assume(var37 <= 1);
-  int var38;
-  var38 = __VERIFIER_nondet_int();
-  assume(var38 >= 0);
-  assume(var38 <= 1);
-  int var39;
-  var39 = __VERIFIER_nondet_int();
-  assume(var39 >= 0);
-  assume(var39 <= 1);
-  int var40;
-  var40 = __VERIFIER_nondet_int();
-  assume(var40 >= 0);
-  assume(var40 <= 1);
-  int var41;
-  var41 = __VERIFIER_nondet_int();
-  assume(var41 >= 0);
-  assume(var41 <= 1);
-  int var42;
-  var42 = __VERIFIER_nondet_int();
-  assume(var42 >= 0);
-  assume(var42 <= 1);
-  int var43;
-  var43 = __VERIFIER_nondet_int();
-  assume(var43 >= 0);
-  assume(var43 <= 1);
-  int var44;
-  var44 = __VERIFIER_nondet_int();
-  assume(var44 >= 0);
-  assume(var44 <= 1);
-  int var45;
-  var45 = __VERIFIER_nondet_int();
-  assume(var45 >= 0);
-  assume(var45 <= 1);
-  int var46;
-  var46 = __VERIFIER_nondet_int();
-  assume(var46 >= 0);
-  assume(var46 <= 1);
-  int var47;
-  var47 = __VERIFIER_nondet_int();
-  assume(var47 >= 0);
-  assume(var47 <= 1);
-  int var48;
-  var48 = __VERIFIER_nondet_int();
-  assume(var48 >= 0);
-  assume(var48 <= 1);
-  int var49;
-  var49 = __VERIFIER_nondet_int();
-  assume(var49 >= 0);
-  assume(var49 <= 1);
-  int var50;
-  var50 = __VERIFIER_nondet_int();
-  assume(var50 >= 0);
-  assume(var50 <= 1);
-  int var51;
-  var51 = __VERIFIER_nondet_int();
-  assume(var51 >= 0);
-  assume(var51 <= 1);
-  int var52;
-  var52 = __VERIFIER_nondet_int();
-  assume(var52 >= 0);
-  assume(var52 <= 1);
-  int var53;
-  var53 = __VERIFIER_nondet_int();
-  assume(var53 >= 0);
-  assume(var53 <= 1);
-  int var54;
-  var54 = __VERIFIER_nondet_int();
-  assume(var54 >= 0);
-  assume(var54 <= 1);
-  int var55;
-  var55 = __VERIFIER_nondet_int();
-  assume(var55 >= 0);
-  assume(var55 <= 1);
-  int var56;
-  var56 = __VERIFIER_nondet_int();
-  assume(var56 >= 0);
-  assume(var56 <= 1);
-  int var57;
-  var57 = __VERIFIER_nondet_int();
-  assume(var57 >= 0);
-  assume(var57 <= 1);
-  int var58;
-  var58 = __VERIFIER_nondet_int();
-  assume(var58 >= 0);
-  assume(var58 <= 1);
-  int var59;
-  var59 = __VERIFIER_nondet_int();
-  assume(var59 >= 0);
-  assume(var59 <= 1);
-  int var60;
-  var60 = __VERIFIER_nondet_int();
-  assume(var60 >= 0);
-  assume(var60 <= 1);
-  int var61;
-  var61 = __VERIFIER_nondet_int();
-  assume(var61 >= 0);
-  assume(var61 <= 1);
-  int var62;
-  var62 = __VERIFIER_nondet_int();
-  assume(var62 >= 0);
-  assume(var62 <= 1);
-  int var63;
-  var63 = __VERIFIER_nondet_int();
-  assume(var63 >= 0);
-  assume(var63 <= 1);
-  int var64;
-  var64 = __VERIFIER_nondet_int();
-  assume(var64 >= 0);
-  assume(var64 <= 1);
-  int var65;
-  var65 = __VERIFIER_nondet_int();
-  assume(var65 >= 0);
-  assume(var65 <= 1);
-  int var66;
-  var66 = __VERIFIER_nondet_int();
-  assume(var66 >= 0);
-  assume(var66 <= 1);
-  int var67;
-  var67 = __VERIFIER_nondet_int();
-  assume(var67 >= 0);
-  assume(var67 <= 1);
-  int var68;
-  var68 = __VERIFIER_nondet_int();
-  assume(var68 >= 0);
-  assume(var68 <= 1);
-  int var69;
-  var69 = __VERIFIER_nondet_int();
-  assume(var69 >= 0);
-  assume(var69 <= 1);
-  int var70;
-  var70 = __VERIFIER_nondet_int();
-  assume(var70 >= 0);
-  assume(var70 <= 1);
-  int var71;
-  var71 = __VERIFIER_nondet_int();
-  assume(var71 >= 0);
-  assume(var71 <= 1);
-  int var72;
-  var72 = __VERIFIER_nondet_int();
-  assume(var72 >= 0);
-  assume(var72 <= 1);
-  int var73;
-  var73 = __VERIFIER_nondet_int();
-  assume(var73 >= 0);
-  assume(var73 <= 1);
-  int var74;
-  var74 = __VERIFIER_nondet_int();
-  assume(var74 >= 0);
-  assume(var74 <= 1);
-  int myvar0 = 1;
-  assume((var48 == 0 & var49 == 0 & var0 == 1) |
-         (var48 == 0 & var49 == 1 & var0 == 0) |
-         (var48 == 1 & var49 == 0 & var0 == 0) |
-         (var48 == 1 & var49 == 1 & var0 == 1) | 0);
-  assume((var1 == 0 & var51 == 0 & var2 == 1) |
-         (var1 == 0 & var51 == 1 & var2 == 0) |
-         (var1 == 1 & var51 == 0 & var2 == 0) |
-         (var1 == 1 & var51 == 1 & var2 == 1) | 0);
-  assume((var2 == 0 & var52 == 0 & var3 == 1) |
-         (var2 == 0 & var52 == 1 & var3 == 0) |
-         (var2 == 1 & var52 == 0 & var3 == 0) |
-         (var2 == 1 & var52 == 1 & var3 == 1) | 0);
-  assume((var3 == 0 & var53 == 0 & var4 == 1) |
-         (var3 == 0 & var53 == 1 & var4 == 0) |
-         (var3 == 1 & var53 == 0 & var4 == 0) |
-         (var3 == 1 & var53 == 1 & var4 == 1) | 0);
-  assume((var4 == 0 & var54 == 0 & var5 == 1) |
-         (var4 == 0 & var54 == 1 & var5 == 0) |
-         (var4 == 1 & var54 == 0 & var5 == 0) |
-         (var4 == 1 & var54 == 1 & var5 == 1) | 0);
-  assume((var5 == 0 & var55 == 0 & var6 == 1) |
-         (var5 == 0 & var55 == 1 & var6 == 0) |
-         (var5 == 1 & var55 == 0 & var6 == 0) |
-         (var5 == 1 & var55 == 1 & var6 == 1) | 0);
-  assume((var6 == 0 & var56 == 0 & var7 == 1) |
-         (var6 == 0 & var56 == 1 & var7 == 0) |
-         (var6 == 1 & var56 == 0 & var7 == 0) |
-         (var6 == 1 & var56 == 1 & var7 == 1) | 0);
-  assume((var7 == 0 & var57 == 0 & var8 == 1) |
-         (var7 == 0 & var57 == 1 & var8 == 0) |
-         (var7 == 1 & var57 == 0 & var8 == 0) |
-         (var7 == 1 & var57 == 1 & var8 == 1) | 0);
-  assume((var8 == 0 & var58 == 0 & var9 == 1) |
-         (var8 == 0 & var58 == 1 & var9 == 0) |
-         (var8 == 1 & var58 == 0 & var9 == 0) |
-         (var8 == 1 & var58 == 1 & var9 == 1) | 0);
-  assume((var9 == 0 & var59 == 0 & var10 == 1) |
-         (var9 == 0 & var59 == 1 & var10 == 0) |
-         (var9 == 1 & var59 == 0 & var10 == 0) |
-         (var9 == 1 & var59 == 1 & var10 == 1) | 0);
-  assume((var10 == 0 & var60 == 0 & var11 == 1) |
-         (var10 == 0 & var60 == 1 & var11 == 0) |
-         (var10 == 1 & var60 == 0 & var11 == 0) |
-         (var10 == 1 & var60 == 1 & var11 == 1) | 0);
-  assume((var11 == 0 & var61 == 0 & var12 == 1) |
-         (var11 == 0 & var61 == 1 & var12 == 0) |
-         (var11 == 1 & var61 == 0 & var12 == 0) |
-         (var11 == 1 & var61 == 1 & var12 == 1) | 0);
-  assume((var12 == 0 & var62 == 0 & var13 == 1) |
-         (var12 == 0 & var62 == 1 & var13 == 0) |
-         (var12 == 1 & var62 == 0 & var13 == 0) |
-         (var12 == 1 & var62 == 1 & var13 == 1) | 0);
-  assume((var13 == 0 & var63 == 0 & var14 == 1) |
-         (var13 == 0 & var63 == 1 & var14 == 0) |
-         (var13 == 1 & var63 == 0 & var14 == 0) |
-         (var13 == 1 & var63 == 1 & var14 == 1) | 0);
-  assume((var14 == 0 & var64 == 0 & var15 == 1) |
-         (var14 == 0 & var64 == 1 & var15 == 0) |
-         (var14 == 1 & var64 == 0 & var15 == 0) |
-         (var14 == 1 & var64 == 1 & var15 == 1) | 0);
-  assume((var15 == 0 & var65 == 0 & var16 == 1) |
-         (var15 == 0 & var65 == 1 & var16 == 0) |
-         (var15 == 1 & var65 == 0 & var16 == 0) |
-         (var15 == 1 & var65 == 1 & var16 == 1) | 0);
-  assume((var16 == 0 & var66 == 0 & var17 == 1) |
-         (var16 == 0 & var66 == 1 & var17 == 0) |
-         (var16 == 1 & var66 == 0 & var17 == 0) |
-         (var16 == 1 & var66 == 1 & var17 == 1) | 0);
-  assume((var17 == 0 & var67 == 0 & var18 == 1) |
-         (var17 == 0 & var67 == 1 & var18 == 0) |
-         (var17 == 1 & var67 == 0 & var18 == 0) |
-         (var17 == 1 & var67 == 1 & var18 == 1) | 0);
-  assume((var18 == 0 & var68 == 0 & var19 == 1) |
-         (var18 == 0 & var68 == 1 & var19 == 0) |
-         (var18 == 1 & var68 == 0 & var19 == 0) |
-         (var18 == 1 & var68 == 1 & var19 == 1) | 0);
-  assume((var19 == 0 & var69 == 0 & var20 == 1) |
-         (var19 == 0 & var69 == 1 & var20 == 0) |
-         (var19 == 1 & var69 == 0 & var20 == 0) |
-         (var19 == 1 & var69 == 1 & var20 == 1) | 0);
-  assume((var20 == 0 & var70 == 0 & var21 == 1) |
-         (var20 == 0 & var70 == 1 & var21 == 0) |
-         (var20 == 1 & var70 == 0 & var21 == 0) |
-         (var20 == 1 & var70 == 1 & var21 == 1) | 0);
-  assume((var21 == 0 & var71 == 0 & var22 == 1) |
-         (var21 == 0 & var71 == 1 & var22 == 0) |
-         (var21 == 1 & var71 == 0 & var22 == 0) |
-         (var21 == 1 & var71 == 1 & var22 == 1) | 0);
-  assume((var22 == 0 & var72 == 0 & var23 == 1) |
-         (var22 == 0 & var72 == 1 & var23 == 0) |
-         (var22 == 1 & var72 == 0 & var23 == 0) |
-         (var22 == 1 & var72 == 1 & var23 == 1) | 0);
-  assume((var0 == 0 & var50 == 0 & var1 == 1) |
-         (var0 == 0 & var50 == 1 & var1 == 0) |
-         (var0 == 1 & var50 == 0 & var1 == 0) |
-         (var0 == 1 & var50 == 1 & var1 == 1) | 0);
-  assume((var24 == 0 & var73 == 0 & var74 == 1) |
-         (var24 == 0 & var73 == 1 & var74 == 0) |
-         (var24 == 1 & var73 == 0 & var74 == 0) |
-         (var24 == 1 & var73 == 1 & var74 == 1) | 0);
-  assume((var23 == 0 & var73 == 0 & var74 == 1) |
-         (var23 == 0 & var73 == 1 & var74 == 0) |
-         (var23 == 1 & var73 == 0 & var74 == 0) |
-         (var23 == 1 & var73 == 1 & var74 == 1) | 0);
-  assume((var26 == 0 & var71 == 0 & var25 == 1) |
-         (var26 == 0 & var71 == 1 & var25 == 0) |
-         (var26 == 1 & var71 == 0 & var25 == 0) |
-         (var26 == 1 & var71 == 1 & var25 == 1) | 0);
-  assume((var27 == 0 & var70 == 0 & var26 == 1) |
-         (var27 == 0 & var70 == 1 & var26 == 0) |
-         (var27 == 1 & var70 == 0 & var26 == 0) |
-         (var27 == 1 & var70 == 1 & var26 == 1) | 0);
-  assume((var28 == 0 & var69 == 0 & var27 == 1) |
-         (var28 == 0 & var69 == 1 & var27 == 0) |
-         (var28 == 1 & var69 == 0 & var27 == 0) |
-         (var28 == 1 & var69 == 1 & var27 == 1) | 0);
-  assume((var29 == 0 & var68 == 0 & var28 == 1) |
-         (var29 == 0 & var68 == 1 & var28 == 0) |
-         (var29 == 1 & var68 == 0 & var28 == 0) |
-         (var29 == 1 & var68 == 1 & var28 == 1) | 0);
-  assume((var30 == 0 & var67 == 0 & var29 == 1) |
-         (var30 == 0 & var67 == 1 & var29 == 0) |
-         (var30 == 1 & var67 == 0 & var29 == 0) |
-         (var30 == 1 & var67 == 1 & var29 == 1) | 0);
-  assume((var31 == 0 & var66 == 0 & var30 == 1) |
-         (var31 == 0 & var66 == 1 & var30 == 0) |
-         (var31 == 1 & var66 == 0 & var30 == 0) |
-         (var31 == 1 & var66 == 1 & var30 == 1) | 0);
-  assume((var32 == 0 & var65 == 0 & var31 == 1) |
-         (var32 == 0 & var65 == 1 & var31 == 0) |
-         (var32 == 1 & var65 == 0 & var31 == 0) |
-         (var32 == 1 & var65 == 1 & var31 == 1) | 0);
-  assume((var33 == 0 & var64 == 0 & var32 == 1) |
-         (var33 == 0 & var64 == 1 & var32 == 0) |
-         (var33 == 1 & var64 == 0 & var32 == 0) |
-         (var33 == 1 & var64 == 1 & var32 == 1) | 0);
-  assume((var34 == 0 & var63 == 0 & var33 == 1) |
-         (var34 == 0 & var63 == 1 & var33 == 0) |
-         (var34 == 1 & var63 == 0 & var33 == 0) |
-         (var34 == 1 & var63 == 1 & var33 == 1) | 0);
-  assume((var35 == 0 & var62 == 0 & var34 == 1) |
-         (var35 == 0 & var62 == 1 & var34 == 0) |
-         (var35 == 1 & var62 == 0 & var34 == 0) |
-         (var35 == 1 & var62 == 1 & var34 == 1) | 0);
-  assume((var36 == 0 & var61 == 0 & var35 == 1) |
-         (var36 == 0 & var61 == 1 & var35 == 0) |
-         (var36 == 1 & var61 == 0 & var35 == 0) |
-         (var36 == 1 & var61 == 1 & var35 == 1) | 0);
-  assume((var37 == 0 & var60 == 0 & var36 == 1) |
-         (var37 == 0 & var60 == 1 & var36 == 0) |
-         (var37 == 1 & var60 == 0 & var36 == 0) |
-         (var37 == 1 & var60 == 1 & var36 == 1) | 0);
-  assume((var38 == 0 & var59 == 0 & var37 == 1) |
-         (var38 == 0 & var59 == 1 & var37 == 0) |
-         (var38 == 1 & var59 == 0 & var37 == 0) |
-         (var38 == 1 & var59 == 1 & var37 == 1) | 0);
-  assume((var39 == 0 & var58 == 0 & var38 == 1) |
-         (var39 == 0 & var58 == 1 & var38 == 0) |
-         (var39 == 1 & var58 == 0 & var38 == 0) |
-         (var39 == 1 & var58 == 1 & var38 == 1) | 0);
-  assume((var40 == 0 & var57 == 0 & var39 == 1) |
-         (var40 == 0 & var57 == 1 & var39 == 0) |
-         (var40 == 1 & var57 == 0 & var39 == 0) |
-         (var40 == 1 & var57 == 1 & var39 == 1) | 0);
-  assume((var41 == 0 & var56 == 0 & var40 == 1) |
-         (var41 == 0 & var56 == 1 & var40 == 0) |
-         (var41 == 1 & var56 == 0 & var40 == 0) |
-         (var41 == 1 & var56 == 1 & var40 == 1) | 0);
-  assume((var42 == 0 & var55 == 0 & var41 == 1) |
-         (var42 == 0 & var55 == 1 & var41 == 0) |
-         (var42 == 1 & var55 == 0 & var41 == 0) |
-         (var42 == 1 & var55 == 1 & var41 == 1) | 0);
-  assume((var43 == 0 & var54 == 0 & var42 == 1) |
-         (var43 == 0 & var54 == 1 & var42 == 0) |
-         (var43 == 1 & var54 == 0 & var42 == 0) |
-         (var43 == 1 & var54 == 1 & var42 == 1) | 0);
-  assume((var44 == 0 & var53 == 0 & var43 == 1) |
-         (var44 == 0 & var53 == 1 & var43 == 0) |
-         (var44 == 1 & var53 == 0 & var43 == 0) |
-         (var44 == 1 & var53 == 1 & var43 == 1) | 0);
-  assume((var45 == 0 & var52 == 0 & var44 == 1) |
-         (var45 == 0 & var52 == 1 & var44 == 0) |
-         (var45 == 1 & var52 == 0 & var44 == 0) |
-         (var45 == 1 & var52 == 1 & var44 == 1) | 0);
-  assume((var46 == 0 & var51 == 0 & var45 == 1) |
-         (var46 == 0 & var51 == 1 & var45 == 0) |
-         (var46 == 1 & var51 == 0 & var45 == 0) |
-         (var46 == 1 & var51 == 1 & var45 == 1) | 0);
-  assume((var47 == 0 & var50 == 0 & var46 == 1) |
-         (var47 == 0 & var50 == 1 & var46 == 0) |
-         (var47 == 1 & var50 == 0 & var46 == 0) |
-         (var47 == 1 & var50 == 1 & var46 == 1) | 0);
-  assume((var25 == 0 & var72 == 0 & var24 == 1) |
-         (var25 == 0 & var72 == 1 & var24 == 0) |
-         (var25 == 1 & var72 == 0 & var24 == 0) |
-         (var25 == 1 & var72 == 1 & var24 == 1) | 0);
-  assume((var48 == 0 & var49 == 0 & var47 == 0) |
-         (var48 == 0 & var49 == 1 & var47 == 1) |
-         (var48 == 1 & var49 == 0 & var47 == 1) |
-         (var48 == 1 & var49 == 1 & var47 == 0) | 0);
-  reach_error();
-  return 0; /* 0 x[0]1 x[1]2 x[2]3 x[3]4 x[4]5 x[5]6 x[6]7 x[7]8 x[8]9 x[9]10
-               x[10]11 x[11]12 x[12]13 x[13]14 x[14]15 x[15]16 x[16]17 x[17]18
-               x[18]19 x[19]20 x[20]21 x[21]22 x[22]23 x[23]24 x[24]25 x[25]26
-               x[26]27 x[27]28 x[28]29 x[29]30 x[30]31 x[31]32 x[32]33 x[33]34
-               x[34]35 x[35]36 x[36]37 x[37]38 x[38]39 x[39]40 x[40]41 x[41]42
-               x[42]43 x[43]44 x[44]45 x[45]46 x[46]47 x[47]48 x[48]49 x[49]50
-               x[50]51 x[51]52 x[52]53 x[53]54 x[54]55 x[55]56 x[56]57 x[57]58
-               x[58]59 x[59]60 x[60]61 x[61]62 x[62]63 x[63]64 x[64]65 x[65]66
-               x[66]67 x[67]68 x[68]69 x[69]70 x[70]71 x[71]72 x[72]73 x[73]74
-               x[74] */
-}
diff --git a/test/Feature/TestSeeding.c b/test/Feature/TestSeeding.c
index 765c055f4b..f31de53a83 100644
--- a/test/Feature/TestSeeding.c
+++ b/test/Feature/TestSeeding.c
@@ -6,8 +6,8 @@
 // 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 --seed-dir=%t1.klee-out --output-dir=%t3.klee-out  %t1.bc
+// RUN: %klee --seed-dir=%t2.klee-out --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
diff --git a/test/Feature/coverage-branches.prp b/test/Feature/coverage-branches.prp
deleted file mode 100644
index dd5d55f2a6..0000000000
--- a/test/Feature/coverage-branches.prp
+++ /dev/null
@@ -1 +0,0 @@
-CHECK( init(main()), LTL(G ! call(reach_error())) )
\ No newline at end of file
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 38ee2f7451..5eb134739f 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -177,12 +177,6 @@ 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)"),
@@ -424,6 +418,16 @@ cl::opt<SAMultiplexKind> MultiplexForStaticAnalysis(
 } // namespace
 
 namespace klee {
+
+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));
+
 extern cl::opt<std::string> MaxTime;
 extern cl::opt<std::string> FunctionCallReproduce;
 extern cl::opt<HaltExecution::Reason> DumpStatesOnHalt;
@@ -449,9 +453,6 @@ class KleeHandler : public InterpreterHandler {
   int m_argc;
   char **m_argv;
 
-  int argc() override { return m_argc; }
-  char **argv() override { return m_argv; }
-
 public:
   KleeHandler(int argc, char **argv);
   ~KleeHandler();
@@ -465,8 +466,7 @@ class KleeHandler : public InterpreterHandler {
   void incPathsExplored(std::uint32_t num = 1) override {
     m_pathsExplored += num;
   }
-  bool seedInfoToFile(unsigned instructions, unsigned isCompleted,
-                      std::string path);
+  bool seedInfoToFile(unsigned instructions, std::string path);
 
   void setInterpreter(Interpreter *i);
 
@@ -487,6 +487,9 @@ 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,14 +676,12 @@ KleeHandler::openTestFile(const std::string &suffix, unsigned id,
   return openOutputFile(getTestFilename(suffix, id, version));
 }
 
-bool KleeHandler::seedInfoToFile(unsigned instructions, unsigned isCompleted,
-                                 std::string path) {
+bool KleeHandler::seedInfoToFile(unsigned instructions, std::string path) {
   std::ofstream out(path + "seedinfo");
   if (!out.good()) {
     return false;
   }
   out << instructions << "\n";
-  out << isCompleted;
   return true;
 }
 
@@ -692,9 +693,12 @@ void KleeHandler::processTestCase(const ExecutionState &state,
   if (!WriteNone &&
       (FunctionCallReproduce == "" || strcmp(suffix, "assert.err") == 0 ||
        strcmp(suffix, "reachable.err") == 0)) {
-    KTest *ktest = 0;
-    ktest = (KTest *)calloc(1, sizeof(*ktest));
-    bool isCompleted = strcmp(suffix, "early") != 0;
+    KTest ktest;
+    ktest.numArgs = m_argc;
+    ktest.args = m_argv;
+    ktest.symArgvs = 0;
+    ktest.symArgvLen = 0;
+
     bool success = m_interpreter->getSymbolicSolution(state, ktest);
 
     if (!success)
@@ -705,9 +709,9 @@ void KleeHandler::processTestCase(const ExecutionState &state,
 
     if (success) {
       if (WriteKTests) {
-        for (unsigned i = 0; i < ktest->uninitCoeff + 1; ++i) {
+        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 {
@@ -722,26 +726,29 @@ 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;
         }
       }
 
       if (WriteSeedInfo) {
-        for (unsigned i = 0; i < ktest->uninitCoeff + 1; ++i) {
+        for (unsigned i = 0; i < ktest.uninitCoeff + 1; ++i) {
           unsigned steppedInstructions;
           m_interpreter->getSteppedInstructions(state, steppedInstructions);
-          if (!seedInfoToFile(steppedInstructions, isCompleted,
+          if (!seedInfoToFile(steppedInstructions,
                               getOutputFilename(getTestFilename("", id, i)))) {
             klee_warning("unable to write seedinfo for test case");
           }
         }
       }
 
-      kTest_free(ktest);
-    } else {
-      free(ktest);
+      for (unsigned i = 0; i < ktest.numObjects; i++) {
+        free(ktest.objects[i].name);
+        free(ktest.objects[i].bytes);
+        free(ktest.objects[i].pointers);
+      }
+      free(ktest.objects);
     }
 
     if (message) {
@@ -929,6 +936,24 @@ 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");
@@ -1533,6 +1558,47 @@ static int run_klee_on_function(int pArgc, char **pArgv, char **pEnvp,
     }
   }
 
+  std::vector<SeedFromFile> seeds;
+  for (std::vector<std::string>::iterator it = SeedOutFile.begin(),
+                                          ie = SeedOutFile.end();
+       it != ie; ++it) {
+    SeedFromFile out(it->substr(0, it->size() - 5));
+    if (!out.ktest) {
+      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) {
+      SeedFromFile out(it2->substr(0, it2->size() - 5));
+      if (!out.ktest) {
+        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);
 
   auto endTime = std::time(nullptr);