about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2017-05-24 18:56:43 +0100
committerDan Liew <delcypher@gmail.com>2017-06-01 11:36:09 +0100
commit97076694644846ffd4ae376c1e94eb17f669ec07 (patch)
treec7308092cae8de58cc0e2c01cbceb781e550375d /lib
parent1d9b6096e68eda51b95ae92b69b1f91c4cff0f7b (diff)
downloadklee-97076694644846ffd4ae376c1e94eb17f669ec07.tar.gz
[Z3] Add `-debug-z3-verbosity=<N>` option which behaves like Z3's `-v:<N>` option.
This lets us see what Z3 is doing execution (e.g. which tactic is being
applied) which is very useful for debugging.
Diffstat (limited to 'lib')
-rw-r--r--lib/Solver/Z3Solver.cpp13
1 files changed, 13 insertions, 0 deletions
diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
index 4443c246..c8af7e9e 100644
--- a/lib/Solver/Z3Solver.cpp
+++ b/lib/Solver/Z3Solver.cpp
@@ -33,6 +33,10 @@ llvm::cl::opt<std::string> Z3QueryDumpFile(
 llvm::cl::opt<bool> Z3ValidateModels(
     "debug-z3-validate-models", llvm::cl::init(false),
     llvm::cl::desc("When generating Z3 models validate these against the query"));
+
+llvm::cl::opt<unsigned>
+    Z3VerbosityLevel("debug-z3-verbosity", llvm::cl::init(0),
+                     llvm::cl::desc("Z3 verbosity level (default=0)"));
 }
 
 #include "llvm/Support/ErrorHandling.h"
@@ -108,6 +112,15 @@ Z3SolverImpl::Z3SolverImpl()
     }
     klee_message("Dumping Z3 queries to \"%s\"", Z3QueryDumpFile.c_str());
   }
+
+  // Set verbosity
+  if (Z3VerbosityLevel > 0) {
+    std::string underlyingString;
+    llvm::raw_string_ostream ss(underlyingString);
+    ss << Z3VerbosityLevel;
+    ss.flush();
+    Z3_global_param_set("verbose", underlyingString.c_str());
+  }
 }
 
 Z3SolverImpl::~Z3SolverImpl() {