[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.

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