Merge branch 'fix_bfs2' of https://github.com/MartinNowack/klee into MartinNowack-fix_bfs2

2 files changed, 32 insertions, 0 deletions

diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 47f300d1..c787382f 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;
+}