From 2eec409061b6f3f107ba3679e9d4745e64451952 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Wed, 24 Oct 2012 14:28:21 +0000 Subject: Patch by Dan Liew: "Added SMTLIBLoggingSolver for logging queries in SMT-LIBv2 format." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166564 91177308-0d34-0410-b5e6-96231b3b80d8 --- include/klee/Solver.h | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'include') diff --git a/include/klee/Solver.h b/include/klee/Solver.h index b87b6dc3..4cedf47d 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -215,6 +215,11 @@ namespace klee { /// after writing them to the given path in .pc format. Solver *createPCLoggingSolver(Solver *s, std::string path); + /// createSMTLIBLoggingSolver - Create a solver which will forward all queries + /// after writing them to the given path in .smt2 format. + Solver *createSMTLIBLoggingSolver(Solver *s, std::string path); + + /// createDummySolver - Create a dummy solver implementation which always /// fails. Solver *createDummySolver(); -- cgit 1.4.1