Merge branch 'MartinNowack-fix_bfs2'

1 files changed, 22 insertions, 0 deletions

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;
+}