STP: add option to switch SAT solver: --stp-sat-solver and set default to CryptoMinisat

1 files changed, 31 insertions, 0 deletions

diff --git a/test/Solver/STPswitchSAT.c b/test/Solver/STPswitchSAT.c
new file mode 100644
index 00000000..f205aca7
--- /dev/null
+++ b/test/Solver/STPswitchSAT.c
@@ -0,0 +1,31 @@
+// REQUIRES: stp
+// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc
+//
+// RUN: rm -rf %t.klee-out-minisat
+// RUN: %klee --output-dir=%t.klee-out-minisat -solver-backend=stp --stp-sat-solver=minisat %t1.bc
+// RUN: cat %t.klee-out-minisat/messages.txt %t.klee-out-minisat/warnings.txt > %t.klee-out-minisat/all.txt
+// RUN: FileCheck --input-file=%t.klee-out-minisat/all.txt --check-prefix=MINISAT %s
+//
+// RUN: rm -rf %t.klee-out-riss
+// RUN: %klee --output-dir=%t.klee-out-riss -solver-backend=stp --stp-sat-solver=riss %t1.bc
+// RUN: cat %t.klee-out-riss/messages.txt %t.klee-out-riss/warnings.txt > %t.klee-out-riss/all.txt
+// RUN: FileCheck --input-file=%t.klee-out-riss/all.txt --check-prefix=RISS %s
+
+#include "klee/klee.h"
+
+int main(void) {
+	int foo;
+	int bar = 42;
+	klee_make_symbolic(&foo, sizeof(foo), "foo");
+
+	if (foo) bar -= 17;
+	else bar += 5;
+
+	return bar;
+}
+
+// MINISAT: KLEE: Using STP solver backend
+// MINISAT: {{KLEE: SAT solver: MiniSat|KLEE: Fallback SAT solver}}
+
+// RISS: KLEE: Using STP solver backend
+// RISS: {{KLEE: SAT solver: RISS|KLEE: Fallback SAT solver}}