about summary refs log tree commit diff homepage
path: root/lib/Solver/Z3Builder.h
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Solver/Z3Builder.h')
-rw-r--r--lib/Solver/Z3Builder.h14
1 files changed, 4 insertions, 10 deletions
diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h
index f3b2732b..a3473f82 100644
--- a/lib/Solver/Z3Builder.h
+++ b/lib/Solver/Z3Builder.h
@@ -81,19 +81,13 @@ template <> inline ::Z3_ast Z3NodeHandle<Z3_sort>::as_ast() {
   // instead to simplify our implementation but this seems cleaner.
   return ::Z3_sort_to_ast(context, node);
 }
-template <> inline void Z3NodeHandle<Z3_sort>::dump() {
-  llvm::errs() << "Z3SortHandle:\n" << ::Z3_sort_to_string(context, node)
-               << "\n";
-}
 typedef Z3NodeHandle<Z3_sort> Z3SortHandle;
+template <> void Z3NodeHandle<Z3_sort>::dump() __attribute__((used));
 
 // Specialise for Z3_ast
 template <> inline ::Z3_ast Z3NodeHandle<Z3_ast>::as_ast() { return node; }
-template <> inline void Z3NodeHandle<Z3_ast>::dump() {
-  llvm::errs() << "Z3ASTHandle:\n" << ::Z3_ast_to_string(context, as_ast())
-               << "\n";
-}
 typedef Z3NodeHandle<Z3_ast> Z3ASTHandle;
+template <> void Z3NodeHandle<Z3_ast>::dump() __attribute__((used));
 
 class Z3ArrayExprHash : public ArrayExprHash<Z3ASTHandle> {
 
@@ -171,11 +165,11 @@ private:
   Z3SortHandle getBvSort(unsigned width);
   Z3SortHandle getArraySort(Z3SortHandle domainSort, Z3SortHandle rangeSort);
   bool autoClearConstructCache;
+  std::string z3LogInteractionFile;
 
 public:
   Z3_context ctx;
-
-  Z3Builder(bool autoClearConstructCache = true);
+  Z3Builder(bool autoClearConstructCache, const char *z3LogInteractionFile);
   ~Z3Builder();
 
   Z3ASTHandle getTrue();