Fix BFS searcher

For performance reasons, if KLEE branches, one state is reused
and it is progressed by adding new constraints.
Make sure both new states end up at the end of the BFS searcher queue.

2 files changed, 32 insertions, 0 deletions

diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 3bfcd6b3..f61ae6ec 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -104,6 +104,16 @@ ExecutionState &BFSSearcher::selectState() {
 void BFSSearcher::update(ExecutionState *current,
                          const std::vector<ExecutionState *> &addedStates,
                          const std::vector<ExecutionState *> &removedStates) {
+  // Assumption: If new states were added KLEE forked, therefore states evolved.
+  // constraints were added to the current state, it evolved.
+  if (!addedStates.empty() && current &&
+      std::find(removedStates.begin(), removedStates.end(), current) ==
+          removedStates.end()) {
+    assert(states.front() == current);
+    states.pop_front();
+    states.push_back(current);
+  }
+
   states.insert(states.end(),
                 addedStates.begin(),
                 addedStates.end());
diff --git a/test/Feature/BFSSearcher.c b/test/Feature/BFSSearcher.c
new file mode 100644
index 00000000..313791d5
--- /dev/null
+++ b/test/Feature/BFSSearcher.c
@@ -0,0 +1,22 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --stop-after-n-instructions=500 --search=bfs %t1.bc 2>%t2.log
+// RUN: FileCheck -input-file=%t2.log %s
+#include "assert.h"
+#include "klee/klee.h"
+
+int nd() {
+  int r;
+  klee_make_symbolic(&r, sizeof(r), "r");
+  return r;
+}
+
+int main() {
+  int x = 1;
+  while (nd() != 0) {
+    x *= 2;
+  }
+  // CHECK: ASSERTION FAIL
+  klee_assert(0);
+  return x;
+}