Ensured program reliably has 3 paths to be explored, and removed unnecessary options. Make klee_abort() call abort() in replay, and removed trivial test which cannot be easily integrated into the test suite.

2 files changed, 4 insertions, 23 deletions

diff --git a/test/Replay/libkleeruntest/replay_klee_abort.c b/test/Replay/libkleeruntest/replay_klee_abort.c
deleted file mode 100644
index 6d195423..00000000
--- a/test/Replay/libkleeruntest/replay_klee_abort.c
+++ /dev/null
@@ -1,21 +0,0 @@
-// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
-// RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --search=dfs %t.bc
-// RUN: test -f %t.klee-out/test000001.ktest
-// RUN: test -f %t.klee-out/test000001.abort.err
-// RUN: test ! -f %t.klee-out/test000002.ktest
-
-// Now try to replay with libkleeRuntest
-// RUN: %cc %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner
-
-// Check that the default is to exit with an error
-// RUN: not env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner 2>&1
-
-// Check that setting `KLEE_RUN_TEST_ERRORS_NON_FATAL` will still exit with an error
-// RUN: not env KTEST_FILE=%t.klee-out/test000001.ktest KLEE_RUN_TEST_ERRORS_NON_FATAL=1 %t_runner 2>&1
-
-#include "klee/klee.h"
-
-int main(int argc, char** argv) {
-  klee_abort();
-}
diff --git a/test/Replay/libkleeruntest/replay_klee_prefer_cex.c b/test/Replay/libkleeruntest/replay_klee_prefer_cex.c
index de494975..df441ea8 100644
--- a/test/Replay/libkleeruntest/replay_klee_prefer_cex.c
+++ b/test/Replay/libkleeruntest/replay_klee_prefer_cex.c
@@ -1,6 +1,6 @@
-// RUN: %llvmgcc -DPREFER_VALUE=33 %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --search=dfs %t.bc
+// RUN: %klee --output-dir=%t.klee-out %t.bc
 
 // This should produce three test cases.
 // RUN: test -f %t.klee-out/test000001.ktest
@@ -32,10 +32,12 @@ int main(int argc, char** argv) {
       // It's fine if the prefered value cannot be used
       // CHECK_3: x=1, y=0
     } else {
+      printf("x is allowed to be 33\n");
       // The prefered value should be used if it can be
       // CHECK_2: x=33
     }
   } else {
+    printf("x is not allowed to be 33\n");
     // CHECK_1-NOT: x=33
   }