diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 5f6e0dd02f..0af0be600d 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -234,7 +234,14 @@ 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::list<std::string>
+    SeedOutDir("seed-dir",
+               cl::desc("Directory with .ktest files to be used as seeds"),
+               cl::cat(SeedingCat));
+
+cl::list<std::string> SeedOutFile("seed-file",
+                                  cl::desc(".ktest file to be used as seed"),
+                                  cl::cat(SeedingCat));
 } // namespace klee
 
 namespace {
@@ -1222,18 +1229,16 @@ void Executor::branch(ExecutionState &state,
   }
 
   if (state.isSeeded) {
-    std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
-        seedMap->find(&state);
+    std::map<ExecutionState *, seeds_ty>::iterator it = seedMap->find(&state);
     assert(it != seedMap->end());
     assert(!it->second.empty());
-    std::vector<ExecutingSeed> seeds = it->second;
+    seeds_ty 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<ExecutingSeed>::iterator siit = seeds.begin(),
-                                              siie = seeds.end();
+    for (seeds_ty::iterator siit = seeds.begin(), siie = seeds.end();
          siit != siie; ++siit) {
       unsigned i;
       for (i = 0; i < N; ++i) {
@@ -1254,7 +1259,7 @@ void Executor::branch(ExecutionState &state,
 
       // Extra check in case we're replaying seeds with a max-fork
       if (result[i]) {
-        seedMap->at(result[i]).push_back(*siit);
+        seedMap->at(result[i]).insert(*siit);
       }
     }
   }
@@ -1360,8 +1365,8 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
   bool isInternal = ifTrueBlock == ifFalseBlock;
   PartialValidity res = PartialValidity::None;
   bool isSeeding = current.isSeeded;
-  std::vector<ExecutingSeed> trueSeeds;
-  std::vector<ExecutingSeed> falseSeeds;
+  seeds_ty trueSeeds;
+  seeds_ty falseSeeds;
   time::Span timeout = coreSolverTimeout;
   bool shouldCheckTrueBlock = true, shouldCheckFalseBlock = true;
 
@@ -1385,13 +1390,11 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
       }
     }
   } else {
-    std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
-        seedMap->find(&current);
+    std::map<ExecutionState *, seeds_ty>::iterator it = seedMap->find(&current);
     assert(it != seedMap->end());
     assert(!it->second.empty());
     timeout *= static_cast<unsigned>(it->second.size());
-    for (std::vector<ExecutingSeed>::iterator siit = it->second.begin(),
-                                              siie = it->second.end();
+    for (seeds_ty::iterator siit = it->second.begin(), siie = it->second.end();
          siit != siie; ++siit) {
       ref<ConstantExpr> result;
       bool success = solver->getValue(current.constraints.cs(),
@@ -1400,9 +1403,9 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
       assert(success && "FIXME: Unhandled solver failure");
       (void)success;
       if (result->isTrue()) {
-        trueSeeds.push_back(*siit);
+        trueSeeds.insert(*siit);
       } else if (result->isFalse()) {
-        falseSeeds.push_back(*siit);
+        falseSeeds.insert(*siit);
       }
     }
     if (!trueSeeds.empty() && falseSeeds.empty()) {
@@ -1737,13 +1740,11 @@ void Executor::executeGetValue(ExecutionState &state, ref<Expr> e,
     (void)success;
     bindLocal(target, state, value);
   } else {
-    std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
-        seedMap->find(&state);
+    std::map<ExecutionState *, seeds_ty>::iterator it = seedMap->find(&state);
     assert(it != seedMap->end());
     assert(!it->second.empty());
     std::set<ref<Expr>> values;
-    for (std::vector<ExecutingSeed>::iterator siit = it->second.begin(),
-                                              siie = it->second.end();
+    for (seeds_ty::iterator siit = it->second.begin(), siie = it->second.end();
          siit != siie; ++siit) {
       ref<Expr> cond = siit->assignment.evaluate(e);
       cond = optimizer.optimizeExpr(cond, true);
@@ -4562,16 +4563,14 @@ std::vector<ExecutingSeed> Executor::uploadNewSeeds() {
 
 void Executor::initialSeed(ExecutionState &initialState,
                            std::vector<ExecutingSeed> usingSeeds) {
-  // FIX: better file managment when seeding + flag if all seeds are completed
-
   if (usingSeeds.empty()) {
     return;
   }
-  std::vector<ExecutingSeed> &v = seedMap->at(&initialState);
+  seeds_ty &v = seedMap->at(&initialState);
   for (std::vector<ExecutingSeed>::const_iterator it = usingSeeds.begin(),
                                                   ie = usingSeeds.end();
        it != ie; ++it) {
-    v.push_back(*it);
+    v.insert(*it);
   }
   klee_message("Seeding began using %ld seeds!\n", usingSeeds.size());
   objectManager->seed(&initialState);
@@ -4760,27 +4759,38 @@ 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();
+  seeds_ty &seeds = it->second;
+
+  assert(!seeds.empty());
+  assert(seeds.begin()->maxInstructions >= state->steppedInstructions &&
+         "state stepped instructions exceeded seed max instructions");
+
+  seeds_ty::iterator siit = seeds.begin();
   if (siit->maxInstructions &&
-      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;
-    }
-    seedMap->erase(state);
-    objectManager->unseed(state);
-    if (seedMap->size() == 0) {
-      klee_message("Seeding done!\n");
+      siit->maxInstructions == state->steppedInstructions) {
+    if (seeds.size() == 1) {
+      state->coveredNew = siit->coveredNew;
+      if (siit->coveredNewError) {
+        state->coveredNewError = siit->coveredNewError;
+      }
     }
-    return true;
+    seeds.erase(seeds.begin());
   }
-  return false;
+
+  assert(seeds.empty() ||
+         seeds.begin()->maxInstructions != state->steppedInstructions);
+
+  if (!seeds.empty()) {
+    return false;
+  }
+
+  seedMap->erase(state);
+  objectManager->unseed(state);
+  if (seedMap->size() == 0) {
+    klee_message("Seeding done!\n");
+  }
+  return true;
 }
 
 void Executor::goForward(ref<ForwardAction> action) {
@@ -4799,7 +4809,6 @@ void Executor::goForward(ref<ForwardAction> action) {
   if (targetManager) {
     targetManager->pullGlobal(state);
   }
-
   if (targetCalculator && TrackCoverage != TrackCoverageBy::None &&
       state.multiplexKF && functionsByModule.modules.size() > 1 &&
       targetCalculator->isCovered(state.multiplexKF)) {
@@ -4815,7 +4824,7 @@ void Executor::goForward(ref<ForwardAction> action) {
   } else if (state.isSymbolicCycled(MaxSymbolicCycles)) {
     terminateStateEarly(state, "max-sym-cycles exceeded.",
                         StateTerminationType::MaxCycles);
-  } else if (!fa->state->isSeeded || !reachedMaxSeedInstructions(fa->state)) {
+  } else if (!state.isSeeded || !reachedMaxSeedInstructions(&state)) {
     maxNewWriteableOSSize = 0;
     maxNewStateStackSize = 0;
 
@@ -6801,14 +6810,13 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
 
     if (state.isSeeded) { // In seed mode we need to add this as a
                           // binding.
-      std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it =
-          seedMap->find(&state);
+      std::map<ExecutionState *, seeds_ty>::iterator it = seedMap->find(&state);
       assert(it != seedMap->end());
       assert(!it->second.empty());
-      for (std::vector<ExecutingSeed>::iterator siit = it->second.begin(),
-                                                siie = it->second.end();
+      for (seeds_ty::iterator siit = it->second.begin(),
+                              siie = it->second.end();
            siit != siie; ++siit) {
-        ExecutingSeed &si = *siit;
+        const ExecutingSeed &si = *siit;
         KTestObject *obj = si.getNextInput(mo, NamedSeedMatching);
 
         if (!obj) {
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index 4f099de3f2..54b2f34ff4 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -24,7 +24,8 @@ using namespace klee;
 
 void ExecutingSeed::kTestDeleter(KTest *ktest) { kTest_free(ktest); }
 
-KTestObject *ExecutingSeed::getNextInput(const MemoryObject *mo, bool byName) {
+KTestObject *ExecutingSeed::getNextInput(const MemoryObject *mo,
+                                         bool byName) const {
   if (!input)
     return nullptr;
 
diff --git a/lib/Core/SeedInfo.h b/lib/Core/SeedInfo.h
index c276d3e2d7..db6dc999cf 100644
--- a/lib/Core/SeedInfo.h
+++ b/lib/Core/SeedInfo.h
@@ -27,13 +27,13 @@ class MemoryObject;
 
 class ExecutingSeed {
 public:
-  Assignment assignment;
+  mutable Assignment assignment;
   std::shared_ptr<KTest> input;
   unsigned maxInstructions = 0;
-  std::set<struct KTestObject *> used;
+  mutable std::set<struct KTestObject *> used;
   mutable std::deque<ref<box<bool>>> coveredNew;
   mutable ref<box<bool>> coveredNewError = nullptr;
-  unsigned inputPosition = 0;
+  mutable unsigned inputPosition = 0;
 
 public:
   ~ExecutingSeed() {}
@@ -52,7 +52,7 @@ class ExecutingSeed {
       : assignment(assignment), maxInstructions(maxInstructions),
         coveredNew(coveredNew), coveredNewError(coveredNewError) {}
 
-  KTestObject *getNextInput(const MemoryObject *mo, bool byName);
+  KTestObject *getNextInput(const MemoryObject *mo, bool byName) const;
 
   static void kTestDeleter(KTest *ktest);
 };
diff --git a/lib/Core/SeedMap.cpp b/lib/Core/SeedMap.cpp
index 8fb28804eb..c319e649a6 100644
--- a/lib/Core/SeedMap.cpp
+++ b/lib/Core/SeedMap.cpp
@@ -8,8 +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<ExecutingSeed>>::iterator it =
-          seedMap.find(state);
+      std::map<ExecutionState *, seeds_ty>::iterator it = seedMap.find(state);
       if (it != seedMap.end()) {
         seedMap.erase(it);
       }
@@ -17,45 +16,39 @@ void SeedMap::update(ref<ObjectManager::Event> e) {
   }
 }
 
-std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator
+std::map<ExecutionState *, seeds_ty>::iterator
 SeedMap::upper_bound(ExecutionState *state) {
   return seedMap.upper_bound(state);
 }
 
-std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator
+std::map<ExecutionState *, seeds_ty>::iterator
 SeedMap::find(ExecutionState *state) {
   return seedMap.find(state);
 }
 
-std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator
-SeedMap::begin() {
+std::map<ExecutionState *, seeds_ty>::iterator SeedMap::begin() {
   return seedMap.begin();
 }
 
-std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator
-SeedMap::end() {
+std::map<ExecutionState *, seeds_ty>::iterator SeedMap::end() {
   return seedMap.end();
 }
 
-void SeedMap::erase(
-    std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator it) {
+void SeedMap::erase(std::map<ExecutionState *, seeds_ty>::iterator it) {
   seedMap.erase(it);
 }
 
 void SeedMap::erase(ExecutionState *state) { seedMap.erase(state); }
 
-void SeedMap::push_back(ExecutionState *state,
-                        std::vector<ExecutingSeed>::iterator siit) {
-  seedMap[state].push_back(*siit);
+void SeedMap::insert(ExecutionState *state, seeds_ty::iterator siit) {
+  seedMap[state].insert(*siit);
 }
 
 std::size_t SeedMap::count(ExecutionState *state) {
   return seedMap.count(state);
 }
 
-std::vector<ExecutingSeed> &SeedMap::at(ExecutionState *state) {
-  return seedMap[state];
-}
+seeds_ty &SeedMap::at(ExecutionState *state) { return seedMap[state]; }
 
 bool SeedMap::empty() { return seedMap.empty(); }
 
diff --git a/lib/Core/SeedMap.h b/lib/Core/SeedMap.h
index 75f5235320..c6b97afd9d 100644
--- a/lib/Core/SeedMap.h
+++ b/lib/Core/SeedMap.h
@@ -6,30 +6,36 @@
 #include "SeedInfo.h"
 
 #include <map>
-
+#include <set>
 namespace klee {
+
+struct SeedLess {
+  bool operator()(const ExecutingSeed &a, const ExecutingSeed &b) const {
+    return a.maxInstructions <= b.maxInstructions;
+  }
+};
+
+using seeds_ty = std::multiset<ExecutingSeed, SeedLess>;
+
 class SeedMap : public Subscriber {
 private:
-  std::map<ExecutionState *, std::vector<ExecutingSeed>> seedMap;
+  std::map<ExecutionState *, seeds_ty> seedMap;
 
 public:
   SeedMap();
 
   void update(ref<ObjectManager::Event> e) override;
 
-  std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator
+  std::map<ExecutionState *, seeds_ty>::iterator
   upper_bound(ExecutionState *state);
-  std::map<ExecutionState *, std::vector<ExecutingSeed>>::iterator
-  find(ExecutionState *state);
-  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);
+  std::map<ExecutionState *, seeds_ty>::iterator find(ExecutionState *state);
+  std::map<ExecutionState *, seeds_ty>::iterator end();
+  std::map<ExecutionState *, seeds_ty>::iterator begin();
+  void erase(std::map<ExecutionState *, seeds_ty>::iterator it);
   void erase(ExecutionState *state);
-  void push_back(ExecutionState *state,
-                 std::vector<ExecutingSeed>::iterator siit);
+  void insert(ExecutionState *state, seeds_ty::iterator siit);
   std::size_t count(ExecutionState *state);
-  std::vector<ExecutingSeed> &at(ExecutionState *state);
+  seeds_ty &at(ExecutionState *state);
   unsigned size() { return seedMap.size(); }
   bool empty();
 
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index c98f17d6e4..fe09c64fe7 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -16,8 +16,6 @@
 
 #include "llvm/Support/CommandLine.h"
 
-#include <string>
-
 using namespace llvm;
 using namespace klee;
 
@@ -207,7 +205,8 @@ Searcher *klee::constructUserSearcher(Executor &executor) {
   } else {
     searcher = constructBaseSearcher(executor);
   }
-  if(RunForever){
+  if (RunForever || SeedOutFile.begin() != SeedOutFile.end() ||
+      SeedOutDir.begin() != SeedOutDir.end()) {
     searcher = new SeededSearcher(searcher);
   }
   llvm::raw_ostream &os = executor.getHandler().getInfoStream();
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 5eb134739f..dadcdd4e6f 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -419,18 +419,12 @@ cl::opt<SAMultiplexKind> MultiplexForStaticAnalysis(
 
 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::list<std::string> SeedOutFile;
+extern cl::list<std::string> SeedOutDir;
 extern cl::opt<std::string> MaxTime;
 extern cl::opt<std::string> FunctionCallReproduce;
 extern cl::opt<HaltExecution::Reason> DumpStatesOnHalt;
+
 class ExecutionState;
 } // namespace klee