From 97076694644846ffd4ae376c1e94eb17f669ec07 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 24 May 2017 18:56:43 +0100
Subject: [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.

---
 lib/Solver/Z3Solver.cpp | 13 +++++++++++++
 1 file changed, 13 insertions(+)

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