tests: add STPDumpDebugQueries.c

1 files changed, 19 insertions, 0 deletions

diff --git a/test/Solver/STPDumpDebugQueries.c b/test/Solver/STPDumpDebugQueries.c
new file mode 100644
index 00000000..c87d01c5
--- /dev/null
+++ b/test/Solver/STPDumpDebugQueries.c
@@ -0,0 +1,19 @@
+// REQUIRES: stp
+// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee -solver-backend=stp --output-dir=%t.klee-out -debug-dump-stp-queries %t1.bc
+// RUN: cat %t.klee-out/warnings.txt | FileCheck %s
+
+// Objective: test -debug-dump-stp-queries (just invocation and header in warnings.txt)
+
+#include "klee/klee.h"
+
+int main(int argc, char **argv) {
+  unsigned i;
+  klee_make_symbolic(&i, sizeof i, "i");
+  if (i)
+    return 0;
+  else
+    return 1;
+  // CHECK: KLEE: WARNING: STP query:
+}