From a52050202a53161615e1d088e61ff19d82aeef50 Mon Sep 17 00:00:00 2001
From: Frank Busse <bb0xfb@gmail.com>
Date: Fri, 17 Mar 2023 13:11:58 +0000
Subject: STP: add option to switch SAT solver: --stp-sat-solver and set
 default to CryptoMinisat

---
 test/Solver/STPswitchSAT.c | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 test/Solver/STPswitchSAT.c

(limited to 'test')

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}}
-- 
cgit 1.4.1