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

1 files changed, 5 insertions, 0 deletions

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();