From 7585f28dec4e460cee54665585b25cd02bfbf532 Mon Sep 17 00:00:00 2001
From: Nils Becker <nbecker@student.ethz.ch>
Date: Sun, 8 Apr 2018 18:16:38 +0200
Subject: [PATCH 01/15] Improved quantifier instantiation logging

---
 src/smt/mam.cpp               | 27 ++++++------
 src/smt/mam.h                 |  3 +-
 src/smt/smt_context.cpp       |  5 ++-
 src/smt/smt_context.h         |  3 +-
 src/smt/smt_enode.cpp         |  1 +
 src/smt/smt_enode.h           |  6 +++
 src/smt/smt_model_checker.cpp |  3 +-
 src/smt/smt_quantifier.cpp    | 78 ++++++++++++++++++++++++++++++++---
 src/smt/smt_quantifier.h      |  3 +-
 src/smt/smt_quick_checker.cpp |  3 +-
 10 files changed, 108 insertions(+), 24 deletions(-)

diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index 5c881684f..acd21f9a2 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -1866,7 +1866,7 @@ namespace smt {
         enode *             m_n2;
         enode *             m_app;
         const bind *        m_b;
-        ptr_vector<enode>   m_used_enodes;
+        vector<std::tuple<enode *, enode *>> m_used_enodes;
         unsigned            m_curr_used_enodes_size;
         ptr_vector<enode>   m_pattern_instances; // collect the pattern instances... used for computing min_top_generation and max_top_generation
         unsigned_vector     m_min_top_generation, m_max_top_generation;
@@ -1883,11 +1883,11 @@ namespace smt {
             m_pool.recycle(v);
         }
 
-        void update_max_generation(enode * n) {
+        void update_max_generation(enode * n, enode * prev) {
             m_max_generation = std::max(m_max_generation, n->get_generation());
 
             if (m_ast_manager.has_trace_stream())
-                m_used_enodes.push_back(n);
+                m_used_enodes.push_back(std::make_tuple(prev, n));
         }
 
         // We have to provide the number of expected arguments because we have flat-assoc applications such as +.
@@ -1896,7 +1896,7 @@ namespace smt {
             enode * first = curr;
             do {
                 if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) {
-                    update_max_generation(curr);
+                    update_max_generation(curr, first);
                     return curr;
                 }
                 curr = curr->get_next();
@@ -1909,7 +1909,7 @@ namespace smt {
             curr = curr->get_next();
             while (curr != first) {
                 if (curr->get_decl() == lbl && curr->is_cgr() && curr->get_num_args() == num_expected_args) {
-                    update_max_generation(curr);
+                    update_max_generation(curr, first);
                     return curr;
                 }
                 curr = curr->get_next();
@@ -1933,7 +1933,7 @@ namespace smt {
                 do {
                     if (n->get_decl() == f &&
                         n->get_arg(0)->get_root() == m_args[0]) {
-                        update_max_generation(n);
+                        update_max_generation(n, first);
                         return true;
                     }
                     n = n->get_next();
@@ -1948,7 +1948,7 @@ namespace smt {
                     if (n->get_decl() == f &&
                         n->get_arg(0)->get_root() == m_args[0] &&
                         n->get_arg(1)->get_root() == m_args[1]) {
-                        update_max_generation(n);
+                        update_max_generation(n, first);
                         return true;
                     }
                     n = n->get_next();
@@ -1968,7 +1968,7 @@ namespace smt {
                                 break;
                         }
                         if (i == num_args) {
-                            update_max_generation(n);
+                            update_max_generation(n, first);
                             return true;
                         }
                     }
@@ -2213,7 +2213,7 @@ namespace smt {
         if (bp.m_it == bp.m_end)
             return nullptr;
         m_top++;
-        update_max_generation(*(bp.m_it));
+        update_max_generation(*(bp.m_it), nullptr);
         return *(bp.m_it);
     }
 
@@ -2294,7 +2294,7 @@ namespace smt {
 
         if (m_ast_manager.has_trace_stream()) {
             m_used_enodes.reset();
-            m_used_enodes.push_back(n);
+            m_used_enodes.push_back(std::make_tuple(nullptr, n));
         }
 
         m_pc             = t->get_root();
@@ -2399,6 +2399,9 @@ namespace smt {
             SASSERT(m_n2 != 0);
             if (m_n1->get_root() != m_n2->get_root())
                 goto backtrack;
+            
+            m_used_enodes.push_back(std::make_tuple(m_n1, m_n2));
+
             m_pc = m_pc->m_next;
             goto main_loop;
 
@@ -2793,7 +2796,7 @@ namespace smt {
                     m_pattern_instances.pop_back();
                     m_pattern_instances.push_back(m_app);
                     // continue succeeded
-                    update_max_generation(m_app);
+                    update_max_generation(m_app, nullptr);
                     TRACE("mam_int", tout << "continue next candidate:\n" << mk_ll_pp(m_app->get_owner(), m_ast_manager););
                     m_num_args = c->m_num_args;
                     m_oreg     = c->m_oreg;
@@ -3932,7 +3935,7 @@ namespace smt {
         }
 #endif
 
-        void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, ptr_vector<enode> & used_enodes) override {
+        void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, vector<std::tuple<enode *, enode *>> & used_enodes) override {
             TRACE("trigger_bug", tout << "found match " << mk_pp(qa, m_ast_manager) << "\n";);
 #ifdef Z3DEBUG
             if (m_check_missing_instances) {
diff --git a/src/smt/mam.h b/src/smt/mam.h
index 635cb30e7..f6b2958c5 100644
--- a/src/smt/mam.h
+++ b/src/smt/mam.h
@@ -21,6 +21,7 @@ Revision History:
 
 #include "ast/ast.h"
 #include "smt/smt_types.h"
+#include <tuple>
 
 namespace smt {
     /**
@@ -57,7 +58,7 @@ namespace smt {
 
         virtual void display(std::ostream& out) = 0;
         
-        virtual void on_match(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, ptr_vector<enode> & used_enodes) = 0;
+        virtual void on_match(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation, vector<std::tuple<enode *, enode *>> & used_enodes) = 0;
         
         virtual bool is_shared(enode * n) const = 0;
 
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index dd38776bc..8a37ba61e 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -558,6 +558,7 @@ namespace smt {
             invert_trans(n1);
             n1->m_trans.m_target        = n2;
             n1->m_trans.m_justification = js;
+            n1->m_proof_is_logged       = false;
             SASSERT(r1->trans_reaches(n1));
             // ---------------
             // r1 -> ..  -> n1 -> n2 -> ... -> r2
@@ -749,6 +750,7 @@ namespace smt {
             eq_justification new_js       = curr->m_trans.m_justification;
             curr->m_trans.m_target        = prev;
             curr->m_trans.m_justification = js;
+            curr->m_proof_is_logged       = false;
             prev                          = curr;
             js                            = new_js;
             curr                          = new_curr;
@@ -1045,6 +1047,7 @@ namespace smt {
         SASSERT(r1->trans_reaches(n1));
         n1->m_trans.m_target        = nullptr;
         n1->m_trans.m_justification = null_eq_justification;
+        n1->m_proof_is_logged       = false;
         invert_trans(r1);
         // ---------------
         // n1 -> ... -> r1
@@ -1809,7 +1812,7 @@ namespace smt {
     }
 
     bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation,
-                               unsigned min_top_generation, unsigned max_top_generation, ptr_vector<enode> & used_enodes) {
+                               unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode *>> & used_enodes) {
         return m_qmanager->add_instance(q, pat, num_bindings, bindings, max_generation, min_top_generation, max_top_generation, used_enodes);
     }
 
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index a4581b020..f4e7b72e0 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -49,6 +49,7 @@ Revision History:
 #include "util/timer.h"
 #include "util/statistics.h"
 #include "solver/progress_callback.h"
+#include <tuple>
 
 // there is a significant space overhead with allocating 1000+ contexts in
 // the case that each context only references a few expressions.
@@ -946,7 +947,7 @@ namespace smt {
         bool contains_instance(quantifier * q, unsigned num_bindings, enode * const * bindings);
 
         bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation,
-                          unsigned min_top_generation, unsigned max_top_generation, ptr_vector<enode> & used_enodes);
+                          unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode*>> & used_enodes);
 
         void set_global_generation(unsigned generation) { m_generation = generation; }
 
diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp
index e09e83f6b..d14c37906 100644
--- a/src/smt/smt_enode.cpp
+++ b/src/smt/smt_enode.cpp
@@ -47,6 +47,7 @@ namespace smt {
         n->m_cgc_enabled      = cgc_enabled;
         n->m_iscope_lvl       = iscope_lvl;
         n->m_lbl_hash         = -1;
+        n->m_proof_is_logged  = false;
         unsigned num_args     = n->get_num_args();
         for (unsigned i = 0; i < num_args; i++) {
             enode * arg  = app2enode[owner->get_arg(i)->get_id()];
diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
index b216665e5..d4aebd56b 100644
--- a/src/smt/smt_enode.h
+++ b/src/smt/smt_enode.h
@@ -105,6 +105,7 @@ namespace smt {
         enode_vector        m_parents;          //!< Parent enodes of the equivalence class.
         theory_var_list     m_th_var_list;      //!< List of theories that 'care' about this enode.
         trans_justification m_trans;            //!< A justification for the enode being equal to its root.
+        bool                m_proof_is_logged;  //!< Indicates that the proof for the enode being equal to its root is in the log.
         signed char         m_lbl_hash;         //!< It is different from -1, if enode is used in a pattern
         approx_set          m_lbls;
         approx_set          m_plbls;
@@ -113,6 +114,7 @@ namespace smt {
         friend class context;
         friend class euf_manager;
         friend class conflict_resolution;
+        friend class quantifier_manager;
         
 
         theory_var_list * get_th_var_list() { 
@@ -317,6 +319,10 @@ namespace smt {
 
         theory_var get_th_var(theory_id th_id) const;
 
+        trans_justification get_trans_justification() {
+            return m_trans;
+        }
+
         unsigned get_generation() const {
             return m_generation;
         }
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 765cc87f5..549c15148 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -26,6 +26,7 @@ Revision History:
 #include "smt/smt_context.h"
 #include "smt/smt_model_finder.h"
 #include "model/model_pp.h"
+#include <tuple>
 
 namespace smt {
 
@@ -476,7 +477,7 @@ namespace smt {
     void model_checker::assert_new_instances() {
         TRACE("model_checker_bug_detail", tout << "assert_new_instances, inconsistent: " << m_context->inconsistent() << "\n";);
         ptr_buffer<enode> bindings;
-        ptr_vector<enode> dummy;
+        vector<std::tuple<enode *, enode *>> dummy;
         for (instance* inst : m_new_instances) {
             quantifier * q  = inst->m_q;
             if (m_context->b_internalized(q)) {
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 0ca244185..19fe2c14a 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -104,13 +104,64 @@ namespace smt {
             return m_plugin->is_shared(n);
         }
 
+        inline void log_transitive_justification(std::ostream & log, enode *en) {
+            enode *root = en->get_root();
+            for (enode *it = en; it != root; it = it->get_trans_justification().m_target) {
+                if (!it->m_proof_is_logged) {
+                    it->m_proof_is_logged = true;
+                    print_justification(log, it);
+                }
+            }
+            if (!root->m_proof_is_logged) {
+                root->m_proof_is_logged = true;
+                log << "[eq-expl] #" << root->get_owner_id() << " root\n";
+            }
+        }
+
+        inline void print_justification(std::ostream & out, enode *en) {
+            smt::literal lit;
+            unsigned num_args;
+            enode *target = en->get_trans_justification().m_target;
+
+            switch (en->get_trans_justification().m_justification.get_kind()) {
+            case smt::eq_justification::kind::EQUATION:
+                lit = en->get_trans_justification().m_justification.get_literal();
+                out << "[eq-expl] #" << en->get_owner_id() << " lit #" << m_context.bool_var2expr(lit.var())->get_id() << " ; #" << target->get_owner_id() << "\n";
+                break;
+            case smt::eq_justification::kind::AXIOM:
+                out << "[eq-expl] #" << en->get_owner_id() << " ax ; #" << target->get_owner_id() << "\n";
+                break;
+            case smt::eq_justification::kind::CONGRUENCE:
+                if (!en->get_trans_justification().m_justification.used_commutativity()) {
+                    num_args = en->get_num_args();
+
+                    for (unsigned i = 0; i < num_args; i++) {
+                        
+                        log_transitive_justification(out, en->get_arg(i));
+                        log_transitive_justification(out, target->get_arg(i));
+                    }
+
+                    out << "[eq-expl] #" << en->get_owner_id() << " cg";
+                    for (unsigned i = 0; i < num_args; i++) {
+                        out << " (#" << en->get_arg(i)->get_owner_id() << " #" << target->get_arg(i)->get_owner_id() << ")";
+                    }
+                    out << " ; #" << target->get_owner_id() << "\n";
+                    
+                    break;
+                }
+            default:
+                out << "[eq-expl] #" << en->get_owner_id() << " nyi ; #" << target->get_owner_id() << "\n";
+                break;
+            }
+        }
+
         bool add_instance(quantifier * q, app * pat,
                           unsigned num_bindings,
                           enode * const * bindings,
                           unsigned max_generation,
                           unsigned min_top_generation,
                           unsigned max_top_generation,
-                          ptr_vector<enode> & used_enodes) {
+                          vector<std::tuple<enode *, enode *>> & used_enodes) {
             max_generation = std::max(max_generation, get_generation(q));
             if (m_num_instances > m_params.m_qi_max_instances) {
                 return false;
@@ -120,15 +171,30 @@ namespace smt {
             if (f) {
                 if (has_trace_stream()) {
                     std::ostream & out = trace_stream();
-                    out << "[new-match] " << static_cast<void*>(f) << " #" << q->get_id();
+                    for (auto n : used_enodes) {
+                        enode *orig = std::get<0>(n);
+                        enode *substituted = std::get<1>(n);
+                        if (orig != nullptr) {
+                            log_transitive_justification(out, orig);
+                            log_transitive_justification(out, substituted);
+                        }
+                    }
+                    out << "[new-match] " << static_cast<void*>(f) << " #" << q->get_id() << " #" << pat->get_id();
                     for (unsigned i = 0; i < num_bindings; i++) {
                         // I don't want to use mk_pp because it creates expressions for pretty printing.
                         // This nasty side-effect may change the behavior of Z3.
                         out << " #" << bindings[i]->get_owner_id();
                     }
                     out << " ;";
-                    for (enode* n : used_enodes) 
-                        out << " #" << n->get_owner_id();
+                    for (auto n : used_enodes) {
+                        enode *orig = std::get<0>(n);
+                        enode *substituted = std::get<1>(n);
+                        if (orig == nullptr)
+                            out << " #" << substituted->get_owner_id();
+                        else {
+                            out << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")";
+                        }
+                    }
                     out << "\n";
                 }
                 m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO
@@ -294,12 +360,12 @@ namespace smt {
                                           unsigned max_generation,
                                           unsigned min_top_generation,
                                           unsigned max_top_generation,
-                                          ptr_vector<enode> & used_enodes) {
+                                          vector<std::tuple<enode *, enode *>> & used_enodes) {
         return m_imp->add_instance(q, pat, num_bindings, bindings, max_generation, min_top_generation, max_generation, used_enodes);
     }
 
     bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation) {
-        ptr_vector<enode> tmp;
+        vector<std::tuple<enode *, enode *>> tmp;
         return add_instance(q, nullptr, num_bindings, bindings, generation, generation, generation, tmp);
     }
 
diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h
index ad5f58e49..1b1c3547e 100644
--- a/src/smt/smt_quantifier.h
+++ b/src/smt/smt_quantifier.h
@@ -23,6 +23,7 @@ Revision History:
 #include "util/statistics.h"
 #include "util/params.h"
 #include "smt/smt_types.h"
+#include <tuple>
 
 class proto_model;
 struct smt_params;
@@ -57,7 +58,7 @@ namespace smt {
                           unsigned max_generation,
                           unsigned min_top_generation,
                           unsigned max_top_generation,
-                          ptr_vector<enode> & used_enodes);
+                          vector<std::tuple<enode *, enode *>> & used_enodes);
         bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation = 0);
 
         void init_search_eh();
diff --git a/src/smt/smt_quick_checker.cpp b/src/smt/smt_quick_checker.cpp
index 64c791a0e..ab75d2dea 100644
--- a/src/smt/smt_quick_checker.cpp
+++ b/src/smt/smt_quick_checker.cpp
@@ -19,6 +19,7 @@ Revision History:
 #include "smt/smt_context.h"
 #include "smt/smt_quick_checker.h"
 #include "ast/ast_pp.h"
+#include <tuple>
 
 namespace smt {
 
@@ -211,7 +212,7 @@ namespace smt {
     }
 
     bool quick_checker::process_candidates(quantifier * q, bool unsat) {
-        ptr_vector<enode> empty_used_enodes;
+        vector<std::tuple<enode *, enode *>> empty_used_enodes;
         buffer<unsigned> szs;
         buffer<unsigned> it;
         for (unsigned i = 0; i < m_num_bindings; i++) {

From 7a03f194567f1322dc0b6548c29fe102a92cea87 Mon Sep 17 00:00:00 2001
From: nilsbecker <nbecker@student.ethz.ch>
Date: Sun, 29 Apr 2018 13:08:57 +0200
Subject: [PATCH 02/15] fixing smt code ending up in log files (verbose
 logging)

---
 src/smt/smt_context_pp.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index f4f56df5d..f072a1d13 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -580,20 +580,20 @@ namespace smt {
         case b_justification::BIN_CLAUSE: {
             literal l2 = j.get_literal();
             out << "bin-clause ";
-            display_literal_verbose(out, l2);
+            display_literal(out, l2);
             break;
         }
         case b_justification::CLAUSE: {
             clause * cls = j.get_clause();
             out << "clause ";
-            if (cls) display_literals_verbose(out, cls->get_num_literals(), cls->begin_literals());
+            if (cls) display_literals(out, cls->get_num_literals(), cls->begin_literals());
             break;
         }
         case b_justification::JUSTIFICATION: {
             out << "justification " << j.get_justification()->get_from_theory() << ": ";
             literal_vector lits;
             const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
-            display_literals_verbose(out, lits);
+            display_literals(out, lits);
             break;
         }
         default:

From 9bc7d5de0f25728c9fd850b6329e4091283d07ab Mon Sep 17 00:00:00 2001
From: nilsbecker <nbecker@student.ethz.ch>
Date: Sun, 29 Apr 2018 16:39:32 +0200
Subject: [PATCH 03/15] making sure equality explanations for bound terms are
 logged

---
 src/smt/smt_quantifier.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 5d7c82415..2b134a23f 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -171,6 +171,9 @@ namespace smt {
             if (f) {
                 if (has_trace_stream()) {
                     std::ostream & out = trace_stream();
+                    for (unsigned i = 0; i < num_bindings; ++i) {
+                        log_transitive_justification(out, bindings[i]);
+                    }
                     for (auto n : used_enodes) {
                         enode *orig = std::get<0>(n);
                         enode *substituted = std::get<1>(n);

From 1aeffa2e013e7b0d9ec00bf914ee7ad4e16cea1d Mon Sep 17 00:00:00 2001
From: nilsbecker <nbecker@student.ethz.ch>
Date: Thu, 24 May 2018 19:25:59 +0200
Subject: [PATCH 04/15] fixing issue where argument equalities for congruence
 explanations were not updated explaining equalities added by theories

---
 src/smt/smt_context.cpp    |  7 ++++---
 src/smt/smt_enode.cpp      |  2 +-
 src/smt/smt_enode.h        | 11 +++++++++-
 src/smt/smt_quantifier.cpp | 42 ++++++++++++++++++++++++++++++--------
 4 files changed, 49 insertions(+), 13 deletions(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index c378c401b..5b0b3eacd 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -562,7 +562,7 @@ namespace smt {
             invert_trans(n1);
             n1->m_trans.m_target        = n2;
             n1->m_trans.m_justification = js;
-            n1->m_proof_is_logged       = false;
+            n1->m_proof_logged_status   = smt::logged_status::NOT_LOGGED;
             SASSERT(r1->trans_reaches(n1));
             // ---------------
             // r1 -> ..  -> n1 -> n2 -> ... -> r2
@@ -748,13 +748,14 @@ namespace smt {
         eq_justification js               = n->m_trans.m_justification;
         prev->m_trans.m_target            = nullptr;
         prev->m_trans.m_justification     = null_eq_justification;
+        prev->m_proof_logged_status       = smt::logged_status::NOT_LOGGED;
         while (curr != nullptr) {
             SASSERT(prev->trans_reaches(n));
             enode * new_curr              = curr->m_trans.m_target;
             eq_justification new_js       = curr->m_trans.m_justification;
             curr->m_trans.m_target        = prev;
             curr->m_trans.m_justification = js;
-            curr->m_proof_is_logged       = false;
+            curr->m_proof_logged_status   = smt::logged_status::NOT_LOGGED;
             prev                          = curr;
             js                            = new_js;
             curr                          = new_curr;
@@ -1051,7 +1052,7 @@ namespace smt {
         SASSERT(r1->trans_reaches(n1));
         n1->m_trans.m_target        = nullptr;
         n1->m_trans.m_justification = null_eq_justification;
-        n1->m_proof_is_logged       = false;
+        n1->m_proof_logged_status   = smt::logged_status::NOT_LOGGED;
         invert_trans(r1);
         // ---------------
         // n1 -> ... -> r1
diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp
index d14c37906..ca646974d 100644
--- a/src/smt/smt_enode.cpp
+++ b/src/smt/smt_enode.cpp
@@ -47,7 +47,7 @@ namespace smt {
         n->m_cgc_enabled      = cgc_enabled;
         n->m_iscope_lvl       = iscope_lvl;
         n->m_lbl_hash         = -1;
-        n->m_proof_is_logged  = false;
+        n->m_proof_logged_status = smt::logged_status::NOT_LOGGED;
         unsigned num_args     = n->get_num_args();
         for (unsigned i = 0; i < num_args; i++) {
             enode * arg  = app2enode[owner->get_arg(i)->get_id()];
diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
index 7c1bb3e4d..3e7f0984d 100644
--- a/src/smt/smt_enode.h
+++ b/src/smt/smt_enode.h
@@ -38,6 +38,15 @@ namespace smt {
         }
     };
 
+    /**
+       \brief Indicates whether the proof for membership in an equivalence class is already logged.
+    */
+    enum logged_status {
+        NOT_LOGGED,
+        BEING_LOGGED,
+        LOGGED
+    };
+
     /** \ brief Use sparse maps in SMT solver.
 
     Define this to use hash maps rather than vectors over ast
@@ -105,7 +114,7 @@ namespace smt {
         enode_vector        m_parents;          //!< Parent enodes of the equivalence class.
         theory_var_list     m_th_var_list;      //!< List of theories that 'care' about this enode.
         trans_justification m_trans;            //!< A justification for the enode being equal to its root.
-        bool                m_proof_is_logged;  //!< Indicates that the proof for the enode being equal to its root is in the log.
+        logged_status       m_proof_logged_status;  //!< Indicates that the proof for the enode being equal to its root is in the log.
         signed char         m_lbl_hash;         //!< It is different from -1, if enode is used in a pattern
         approx_set          m_lbls;
         approx_set          m_plbls;
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 2b134a23f..d8795c0cf 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -104,24 +104,38 @@ namespace smt {
             return m_plugin->is_shared(n);
         }
 
-        inline void log_transitive_justification(std::ostream & log, enode *en) {
+        void log_transitive_justification(std::ostream & log, enode *en) {
             enode *root = en->get_root();
             for (enode *it = en; it != root; it = it->get_trans_justification().m_target) {
-                if (!it->m_proof_is_logged) {
-                    it->m_proof_is_logged = true;
+                if (it->m_proof_logged_status == smt::logged_status::NOT_LOGGED) {
+                    it->m_proof_logged_status = smt::logged_status::BEING_LOGGED;
                     print_justification(log, it);
+                    it->m_proof_logged_status = smt::logged_status::LOGGED;
+                } else if (it->m_proof_logged_status != smt::logged_status::BEING_LOGGED && it->get_trans_justification().m_justification.get_kind() == smt::eq_justification::kind::CONGRUENCE) {
+
+                    // When the justification of an argument changes m_proof_logged_status is not reset => We need to check if the proofs of all arguments are logged.
+                    it->m_proof_logged_status = smt::logged_status::BEING_LOGGED;
+                    const unsigned num_args = it->get_num_args();
+                    enode *target = it->get_trans_justification().m_target;
+
+                    for (unsigned i = 0; i < num_args; ++i) {
+                        log_transitive_justification(log, it->get_arg(i));
+                        log_transitive_justification(log, target->get_arg(i));
+                    }
+                    it->m_proof_logged_status = smt::logged_status::LOGGED;
                 }
             }
-            if (!root->m_proof_is_logged) {
-                root->m_proof_is_logged = true;
+            if (root->m_proof_logged_status == smt::logged_status::NOT_LOGGED) {
                 log << "[eq-expl] #" << root->get_owner_id() << " root\n";
+                root->m_proof_logged_status = smt::logged_status::LOGGED;
             }
         }
 
-        inline void print_justification(std::ostream & out, enode *en) {
+        void print_justification(std::ostream & out, enode *en) {
             smt::literal lit;
             unsigned num_args;
             enode *target = en->get_trans_justification().m_target;
+            theory_id th_id;
 
             switch (en->get_trans_justification().m_justification.get_kind()) {
             case smt::eq_justification::kind::EQUATION:
@@ -142,15 +156,27 @@ namespace smt {
                     }
 
                     out << "[eq-expl] #" << en->get_owner_id() << " cg";
-                    for (unsigned i = 0; i < num_args; i++) {
+                    for (unsigned i = 0; i < num_args; ++i) {
                         out << " (#" << en->get_arg(i)->get_owner_id() << " #" << target->get_arg(i)->get_owner_id() << ")";
                     }
                     out << " ; #" << target->get_owner_id() << "\n";
                     
+                    break;
+                } else {
+                    out << "[eq-expl] #" << en->get_owner_id() << " nyi ; #" << target->get_owner_id() << "\n";
                     break;
                 }
+            case smt::eq_justification::kind::JUSTIFICATION:
+                th_id = en->get_trans_justification().m_justification.get_justification()->get_from_theory();
+                if (th_id != null_theory_id) {
+                    symbol const theory = m().get_family_name(th_id);
+                    out << "[eq-expl] #" << en->get_owner_id() << " th:" << theory.str() << " ; #" << target->get_owner_id() << "\n";
+                } else {
+                    out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n";    
+                }
+                break;
             default:
-                out << "[eq-expl] #" << en->get_owner_id() << " nyi ; #" << target->get_owner_id() << "\n";
+                out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n";
                 break;
             }
         }

From f3a627b02620c425765d99693cfa0dceeca819fa Mon Sep 17 00:00:00 2001
From: nilsbecker <nbecker@student.ethz.ch>
Date: Sun, 27 May 2018 15:29:57 +0200
Subject: [PATCH 05/15] making theory explantions easier to parse

---
 src/smt/smt_quantifier.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index d8795c0cf..0951ab913 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -170,7 +170,7 @@ namespace smt {
                 th_id = en->get_trans_justification().m_justification.get_justification()->get_from_theory();
                 if (th_id != null_theory_id) {
                     symbol const theory = m().get_family_name(th_id);
-                    out << "[eq-expl] #" << en->get_owner_id() << " th:" << theory.str() << " ; #" << target->get_owner_id() << "\n";
+                    out << "[eq-expl] #" << en->get_owner_id() << " th " << theory.str() << " ; #" << target->get_owner_id() << "\n";
                 } else {
                     out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n";    
                 }

From 3c464071f7cde63ec67c36039fbe6155b90388b1 Mon Sep 17 00:00:00 2001
From: nilsbecker <nbecker@student.ethz.ch>
Date: Wed, 6 Jun 2018 19:22:01 +0200
Subject: [PATCH 06/15] adding comments

---
 src/smt/mam.cpp            |  2 +-
 src/smt/smt_enode.h        |  6 +++---
 src/smt/smt_quantifier.cpp | 35 +++++++++++++++++++++--------------
 3 files changed, 25 insertions(+), 18 deletions(-)

diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index 4e8c3b922..caf677a85 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -2399,7 +2399,7 @@ namespace smt {
             SASSERT(m_n2 != 0);
             if (m_n1->get_root() != m_n2->get_root())
                 goto backtrack;
-            
+
             m_used_enodes.push_back(std::make_tuple(m_n1, m_n2));
 
             m_pc = m_pc->m_next;
diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
index 14f78e265..61fed786b 100644
--- a/src/smt/smt_enode.h
+++ b/src/smt/smt_enode.h
@@ -42,9 +42,9 @@ namespace smt {
        \brief Indicates whether the proof for membership in an equivalence class is already logged.
     */
     enum logged_status {
-        NOT_LOGGED,
-        BEING_LOGGED,
-        LOGGED
+        NOT_LOGGED, //!< Proof is not logged or logged information is not up-to-date.
+        BEING_LOGGED, //!< We are currently in the process of logging all relevant information. This is used to prevent looping when logging congruence steps.
+        LOGGED //!< Proof is logged and logged information is still up-to-date.
     };
 
     /** \ brief Use sparse maps in SMT solver.
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 0951ab913..63297f829 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -104,12 +104,16 @@ namespace smt {
             return m_plugin->is_shared(n);
         }
 
-        void log_transitive_justification(std::ostream & log, enode *en) {
+        /**
+           \brief Ensures that all relevant proof steps to explain why the enode is equal to the root of its
+           equivalence class are in the log and up-to-date.
+        */
+        void log_justification_to_root(std::ostream & log, enode *en) {
             enode *root = en->get_root();
             for (enode *it = en; it != root; it = it->get_trans_justification().m_target) {
                 if (it->m_proof_logged_status == smt::logged_status::NOT_LOGGED) {
                     it->m_proof_logged_status = smt::logged_status::BEING_LOGGED;
-                    print_justification(log, it);
+                    log_single_justification(log, it);
                     it->m_proof_logged_status = smt::logged_status::LOGGED;
                 } else if (it->m_proof_logged_status != smt::logged_status::BEING_LOGGED && it->get_trans_justification().m_justification.get_kind() == smt::eq_justification::kind::CONGRUENCE) {
 
@@ -119,8 +123,8 @@ namespace smt {
                     enode *target = it->get_trans_justification().m_target;
 
                     for (unsigned i = 0; i < num_args; ++i) {
-                        log_transitive_justification(log, it->get_arg(i));
-                        log_transitive_justification(log, target->get_arg(i));
+                        log_justification_to_root(log, it->get_arg(i));
+                        log_justification_to_root(log, target->get_arg(i));
                     }
                     it->m_proof_logged_status = smt::logged_status::LOGGED;
                 }
@@ -131,7 +135,11 @@ namespace smt {
             }
         }
 
-        void print_justification(std::ostream & out, enode *en) {
+        /**
+          \brief Logs a single equality explanation step and, if necessary, recursively calls log_justification_to_root to log
+          equalities needed by the step (e.g. argument equalities for congruence steps).
+        */
+        void log_single_justification(std::ostream & out, enode *en) {
             smt::literal lit;
             unsigned num_args;
             enode *target = en->get_trans_justification().m_target;
@@ -149,10 +157,9 @@ namespace smt {
                 if (!en->get_trans_justification().m_justification.used_commutativity()) {
                     num_args = en->get_num_args();
 
-                    for (unsigned i = 0; i < num_args; i++) {
-                        
-                        log_transitive_justification(out, en->get_arg(i));
-                        log_transitive_justification(out, target->get_arg(i));
+                    for (unsigned i = 0; i < num_args; ++i) {
+                        log_justification_to_root(out, en->get_arg(i));
+                        log_justification_to_root(out, target->get_arg(i));
                     }
 
                     out << "[eq-expl] #" << en->get_owner_id() << " cg";
@@ -160,7 +167,7 @@ namespace smt {
                         out << " (#" << en->get_arg(i)->get_owner_id() << " #" << target->get_arg(i)->get_owner_id() << ")";
                     }
                     out << " ; #" << target->get_owner_id() << "\n";
-                    
+
                     break;
                 } else {
                     out << "[eq-expl] #" << en->get_owner_id() << " nyi ; #" << target->get_owner_id() << "\n";
@@ -172,7 +179,7 @@ namespace smt {
                     symbol const theory = m().get_family_name(th_id);
                     out << "[eq-expl] #" << en->get_owner_id() << " th " << theory.str() << " ; #" << target->get_owner_id() << "\n";
                 } else {
-                    out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n";    
+                    out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n";
                 }
                 break;
             default:
@@ -198,14 +205,14 @@ namespace smt {
                 if (has_trace_stream()) {
                     std::ostream & out = trace_stream();
                     for (unsigned i = 0; i < num_bindings; ++i) {
-                        log_transitive_justification(out, bindings[i]);
+                        log_justification_to_root(out, bindings[i]);
                     }
                     for (auto n : used_enodes) {
                         enode *orig = std::get<0>(n);
                         enode *substituted = std::get<1>(n);
                         if (orig != nullptr) {
-                            log_transitive_justification(out, orig);
-                            log_transitive_justification(out, substituted);
+                            log_justification_to_root(out, orig);
+                            log_justification_to_root(out, substituted);
                         }
                     }
                     out << "[new-match] " << static_cast<void*>(f) << " #" << q->get_id() << " #" << pat->get_id();

From a4057420372ec269b6356d6309f0ecd2bdf9459f Mon Sep 17 00:00:00 2001
From: nilsbecker <nbecker@student.ethz.ch>
Date: Fri, 6 Jul 2018 12:43:46 +0200
Subject: [PATCH 07/15] Adding comments

---
 src/smt/mam.cpp            | 8 ++++++--
 src/smt/smt_context.h      | 2 +-
 src/smt/smt_quantifier.cpp | 6 ++++++
 src/smt/smt_quantifier.h   | 2 +-
 4 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index 51c39f9e2..a39fe96ed 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -1847,6 +1847,9 @@ namespace smt {
         enode *             m_n2;
         enode *             m_app;
         const bind *        m_b;
+
+        // equalities used for pattern match. The first element of the tuple gives the argument (or null) of some term that was matched against some higher level
+        // structure of the trigger, the second element gives the term that argument is replaced with in order to match the trigger. Used for logging purposes only.
         vector<std::tuple<enode *, enode *>> m_used_enodes;
         unsigned            m_curr_used_enodes_size;
         ptr_vector<enode>   m_pattern_instances; // collect the pattern instances... used for computing min_top_generation and max_top_generation
@@ -2275,7 +2278,7 @@ namespace smt {
 
         if (m_ast_manager.has_trace_stream()) {
             m_used_enodes.reset();
-            m_used_enodes.push_back(std::make_tuple(nullptr, n));
+            m_used_enodes.push_back(std::make_tuple(nullptr, n)); // null indicates that n was matched against the trigger at the top-level
         }
 
         m_pc             = t->get_root();
@@ -2381,6 +2384,7 @@ namespace smt {
             if (m_n1->get_root() != m_n2->get_root())
                 goto backtrack;
 
+            // we used the equality m_n1 = m_n2 for the match and need to make sure it ends up in the log
             m_used_enodes.push_back(std::make_tuple(m_n1, m_n2));
 
             m_pc = m_pc->m_next;
@@ -2777,7 +2781,7 @@ namespace smt {
                     m_pattern_instances.pop_back();
                     m_pattern_instances.push_back(m_app);
                     // continue succeeded
-                    update_max_generation(m_app, nullptr);
+                    update_max_generation(m_app, nullptr); // null indicates a top-level match
                     TRACE("mam_int", tout << "continue next candidate:\n" << mk_ll_pp(m_app->get_owner(), m_ast_manager););
                     m_num_args = c->m_num_args;
                     m_oreg     = c->m_oreg;
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 45d5f15d3..f3c3fc69f 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -959,7 +959,7 @@ namespace smt {
         bool contains_instance(quantifier * q, unsigned num_bindings, enode * const * bindings);
 
         bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation,
-                          unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode*>> & used_enodes);
+                          unsigned min_top_generation, unsigned max_top_generation, vector<std::tuple<enode *, enode*>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/);
 
         void set_global_generation(unsigned generation) { m_generation = generation; }
 
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 63297f829..0a522c072 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -204,9 +204,13 @@ namespace smt {
             if (f) {
                 if (has_trace_stream()) {
                     std::ostream & out = trace_stream();
+
+                    // In the term produced by the quantifier instantiation the root of the equivalence class of the terms bound to the quantified variables
+                    // is used. We need to make sure that all of these equalities appear in the log.
                     for (unsigned i = 0; i < num_bindings; ++i) {
                         log_justification_to_root(out, bindings[i]);
                     }
+
                     for (auto n : used_enodes) {
                         enode *orig = std::get<0>(n);
                         enode *substituted = std::get<1>(n);
@@ -215,6 +219,8 @@ namespace smt {
                             log_justification_to_root(out, substituted);
                         }
                     }
+
+                    // At this point all relevant equalities for the match are logged.
                     out << "[new-match] " << static_cast<void*>(f) << " #" << q->get_id() << " #" << pat->get_id();
                     for (unsigned i = 0; i < num_bindings; i++) {
                         // I don't want to use mk_pp because it creates expressions for pretty printing.
diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h
index 1b1c3547e..3c95d1e23 100644
--- a/src/smt/smt_quantifier.h
+++ b/src/smt/smt_quantifier.h
@@ -58,7 +58,7 @@ namespace smt {
                           unsigned max_generation,
                           unsigned min_top_generation,
                           unsigned max_top_generation,
-                          vector<std::tuple<enode *, enode *>> & used_enodes);
+                          vector<std::tuple<enode *, enode *>> & used_enodes /*gives the equalities used for the pattern match, see mam.cpp for more info*/);
         bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation = 0);
 
         void init_search_eh();

From 1de0f8fe5e8ffbd6643738a6c0ab7994f15eec94 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Sat, 7 Jul 2018 19:10:16 +0300
Subject: [PATCH 08/15] Fix bug in proof checking

---
 src/ast/proofs/proof_checker.cpp | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/ast/proofs/proof_checker.cpp b/src/ast/proofs/proof_checker.cpp
index fd6ea43e1..404551178 100644
--- a/src/ast/proofs/proof_checker.cpp
+++ b/src/ast/proofs/proof_checker.cpp
@@ -389,14 +389,14 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
             match_fact(p, fact) &&
             match_fact(p1, fml) &&
             match_and(fml, terms)) {
-            for (expr* t : terms) 
+            for (expr* t : terms)
                 if (t == fact) return true;
         }
         UNREACHABLE();
         return false;
     }
     case PR_NOT_OR_ELIM: {
-        
+
         if (match_proof(p, p1) &&
             match_fact(p, fact) &&
             match_fact(p1, fml) &&
@@ -605,6 +605,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
                         bool found = false;
                         for (expr* term2 : terms2) {
                             found = term1 == term2;
+                            if (found) break;
                         }
                         if (!found) {
                             IF_VERBOSE(0, verbose_stream() << "Premise not found:" << mk_pp(term1, m) << "\n";);
@@ -738,9 +739,9 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
             }
             if (is_quantifier(e)) {
                 SASSERT(!is_lambda(e));
-                q = to_quantifier(e);                
+                q = to_quantifier(e);
                 // TBD check that quantifier is properly instantiated
-                return is_forall == ::is_forall(q);                
+                return is_forall == ::is_forall(q);
             }
         }
         UNREACHABLE();
@@ -1004,7 +1005,7 @@ bool proof_checker::match_op(expr const* e, decl_kind k, ptr_vector<expr>& terms
     if (e->get_kind() == AST_APP &&
         to_app(e)->get_family_id() == m.get_basic_family_id() &&
         to_app(e)->get_decl_kind() == k) {
-        for (expr* arg : *to_app(e)) 
+        for (expr* arg : *to_app(e))
             terms.push_back(arg);
         return true;
     }

From d2b77b11704b3efd3d8a9851c6a13f1e9863f135 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Sat, 7 Jul 2018 19:07:13 +0100
Subject: [PATCH 09/15] remove dead code

---
 src/tactic/smtlogics/qfbv_tactic.cpp | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp
index bc93b4e7b..a8ad95319 100644
--- a/src/tactic/smtlogics/qfbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfbv_tactic.cpp
@@ -89,14 +89,6 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat
     params_ref solver_p;
     solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed.
 
-    params_ref no_flat_p;
-    no_flat_p.set_bool("flat", false);
-
-    params_ref ctx_simp_p;
-    ctx_simp_p.set_uint("max_depth", 32);
-    ctx_simp_p.set_uint("max_steps", 50000000);
-
-
     params_ref big_aig_p;
     big_aig_p.set_bool("aig_per_assertion", false);
 

From fd75eccfec8dcbefad560c978fcfcf5ca21a0721 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Sun, 8 Jul 2018 13:21:16 +0100
Subject: [PATCH 10/15] don't even bother allocating traces in release mode

---
 src/util/trace.cpp |  7 ++-----
 src/util/trace.h   | 16 ++++++++++++----
 2 files changed, 14 insertions(+), 9 deletions(-)

diff --git a/src/util/trace.cpp b/src/util/trace.cpp
index 9571e99e6..68437ab92 100644
--- a/src/util/trace.cpp
+++ b/src/util/trace.cpp
@@ -21,7 +21,6 @@ Revision History:
 
 #ifdef _TRACE
 std::ofstream tout(".z3-trace"); 
-#endif
 
 static bool g_enable_all_trace_tags = false;
 static str_hashtable* g_enabled_trace_tags = nullptr;
@@ -56,13 +55,11 @@ bool is_trace_enabled(const char * tag) {
 }
 
 void close_trace() {
-#ifdef _TRACE
     tout.close();
-#endif
 }
 
 void open_trace() {
-#ifdef _TRACE
     tout.open(".z3-trace");
-#endif
 }
+
+#endif
diff --git a/src/util/trace.h b/src/util/trace.h
index 789beafc1..be652a620 100644
--- a/src/util/trace.h
+++ b/src/util/trace.h
@@ -33,9 +33,6 @@ Revision History:
 #ifdef _TRACE
 extern std::ofstream tout; 
 #define TRACE_CODE(CODE) { CODE } ((void) 0 )
-#else
-#define TRACE_CODE(CODE) ((void) 0)
-#endif
 
 void enable_trace(const char * tag);
 void enable_all_trace(bool flag);
@@ -48,6 +45,18 @@ void finalize_trace();
   ADD_FINALIZER('finalize_trace();')
 */
 
+#else
+#define TRACE_CODE(CODE) ((void) 0)
+
+static inline void enable_trace(const char * tag) {}
+static inline void enable_all_trace(bool flag) {}
+static inline void disable_trace(const char * tag) {}
+static inline bool is_trace_enabled(const char * tag) {}
+static inline void close_trace() {}
+static inline void open_trace() {}
+static inline void finalize_trace() {}
+#endif
+
 #define TRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE tout << "------------------------------------------------\n"; tout.flush(); })
 
 #define STRACE(TAG, CODE) TRACE_CODE(if (is_trace_enabled(TAG)) { CODE tout.flush(); })
@@ -55,4 +64,3 @@ void finalize_trace();
 #define CTRACE(TAG, COND, CODE) TRACE_CODE(if (is_trace_enabled(TAG) && (COND)) { tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE tout << "------------------------------------------------\n"; tout.flush(); })
 
 #endif /* TRACE_H_ */
-

From a85a4f41c71136eef3c9eab7baad3548a31116b6 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Sun, 8 Jul 2018 15:32:01 +0100
Subject: [PATCH 11/15] ast_exception: remove str copies

---
 src/ast/ast.cpp | 18 +++++++++---------
 src/ast/ast.h   |  2 +-
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index ac7ce156d..f164d6a4f 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1057,7 +1057,7 @@ sort* basic_decl_plugin::join(sort* s1, sort* s2) {
     }
     std::ostringstream buffer;
     buffer << "Sorts " << mk_pp(s1, *m_manager) << " and " << mk_pp(s2, *m_manager) << " are incompatible";
-    throw ast_exception(buffer.str().c_str());
+    throw ast_exception(buffer.str());
 }
 
 
@@ -1086,7 +1086,7 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
             if (domain[i] != domain[0]) {
                 std::ostringstream buffer;
                 buffer << "Sort mismatch between first argument and argument " << (i+1);
-                throw ast_exception(buffer.str().c_str());
+                throw ast_exception(buffer.str());
             }
         }
         return m_manager->mk_func_decl(symbol("distinct"), arity, domain, m_bool_sort, info);
@@ -1701,9 +1701,9 @@ ast * ast_manager::register_node_core(ast * n) {
         SASSERT(m_ast_table.contains(n));
         if (is_func_decl(r) && to_func_decl(r)->get_range() != to_func_decl(n)->get_range()) {
             std::ostringstream buffer;
-            buffer << "Recycling of declaration for the same name '" << to_func_decl(r)->get_name().str().c_str() << "'"
-                   << " and domain, but different range type is not permitted";
-            throw ast_exception(buffer.str().c_str());
+            buffer << "Recycling of declaration for the same name '" << to_func_decl(r)->get_name().str()
+                   << "' and domain, but different range type is not permitted";
+            throw ast_exception(buffer.str());
         }
         deallocate_node(n, ::get_node_size(n));
         return r;
@@ -1992,7 +1992,7 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c
                 buff << "invalid function application for " << decl->get_name() << ", ";
                 buff << "sort mismatch on argument at position " << (i+1) << ", ";
                 buff << "expected " << mk_pp(expected, m) << " but given " << mk_pp(given, m);
-                throw ast_exception(buff.str().c_str());
+                throw ast_exception(buff.str());
             }
         }
     }
@@ -2008,7 +2008,7 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c
                 buff << "invalid function application for " << decl->get_name() << ", ";
                 buff << "sort mismatch on argument at position " << (i+1) << ", ";
                 buff << "expected " << mk_pp(expected, m) << " but given " << mk_pp(given, m);
-                throw ast_exception(buff.str().c_str());
+                throw ast_exception(buff.str());
             }
         }
     }
@@ -2170,7 +2170,7 @@ void ast_manager::check_args(func_decl* f, unsigned n, expr* const* es) {
                    << " for function " << mk_pp(f,*this)
                    << " supplied sort is "
                    << mk_pp(actual_sort, *this);
-            throw ast_exception(buffer.str().c_str());
+            throw ast_exception(buffer.str());
         }
     }
 }
@@ -2194,7 +2194,7 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar
         std::ostringstream buffer;
         buffer << "Wrong number of arguments (" << num_args
                << ") passed to function " << mk_pp(decl, *this);
-        throw ast_exception(buffer.str().c_str());
+        throw ast_exception(buffer.str());
     }
     app * r = nullptr;
     if (num_args == 1 && decl->is_chainable() && decl->get_arity() == 2) {
diff --git a/src/ast/ast.h b/src/ast/ast.h
index aa8669def..7cd1dff93 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -69,7 +69,7 @@ class ast_manager;
 */
 class ast_exception : public default_exception {
 public:
-    ast_exception(char const * msg):default_exception(msg) {}
+    ast_exception(std::string && msg) : default_exception(std::move(msg)) {}
 };
 
 typedef int     family_id;

From c5a282dadbaa2149d5d2f339bfa2c5348e903507 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Sun, 8 Jul 2018 18:04:32 +0100
Subject: [PATCH 12/15] sat_allocator: align allocation size with page boundary
 to reduce memory consumption

---
 src/sat/sat_allocator.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/sat/sat_allocator.h b/src/sat/sat_allocator.h
index 06585ebed..e588c8478 100644
--- a/src/sat/sat_allocator.h
+++ b/src/sat/sat_allocator.h
@@ -23,7 +23,7 @@ Revision History:
 #include "util/machine.h"
 
 class sat_allocator {
-    static const unsigned CHUNK_SIZE     = (1 << 16);
+    static const unsigned CHUNK_SIZE     = (1 << 16) - sizeof(char*);
     static const unsigned SMALL_OBJ_SIZE = 512;
     static const unsigned MASK = ((1 << PTR_ALIGNMENT) - 1);
     static const unsigned NUM_FREE = 1 + (SMALL_OBJ_SIZE >> PTR_ALIGNMENT);

From d6a3afd2a136de53856109b63716e528311b95b1 Mon Sep 17 00:00:00 2001
From: alexanderjsummers <alexander.summers@inf.ethz.ch>
Date: Mon, 9 Jul 2018 11:30:24 +0200
Subject: [PATCH 13/15] Added return value to bool-typed function

It seems that without this, the build fails with a default Visual C++ on Windows; see https://docs.microsoft.com/en-gb/cpp/error-messages/compiler-warnings/compiler-warning-level-1-c4716

Another option would be to add the #pragma directive mentioned there.
---
 src/util/trace.h | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/util/trace.h b/src/util/trace.h
index be652a620..c0dc90f23 100644
--- a/src/util/trace.h
+++ b/src/util/trace.h
@@ -51,7 +51,8 @@ void finalize_trace();
 static inline void enable_trace(const char * tag) {}
 static inline void enable_all_trace(bool flag) {}
 static inline void disable_trace(const char * tag) {}
-static inline bool is_trace_enabled(const char * tag) {}
+// On a default Visual C++ build on Windows, a non-void function either needs to return a value, or we have to add: #pragma warning(default:4716)  
+static inline bool is_trace_enabled(const char * tag) { return false; }
 static inline void close_trace() {}
 static inline void open_trace() {}
 static inline void finalize_trace() {}

From 6f7271a5e8b292965c25f54712c5980f8eefb3ec Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Mon, 9 Jul 2018 10:37:26 +0100
Subject: [PATCH 14/15] remove virtual destructor from api::pmanager

---
 src/api/api_polynomial.cpp | 11 -----------
 src/api/api_polynomial.h   |  6 +++---
 2 files changed, 3 insertions(+), 14 deletions(-)

diff --git a/src/api/api_polynomial.cpp b/src/api/api_polynomial.cpp
index 8c5fc99c9..93a23cb04 100644
--- a/src/api/api_polynomial.cpp
+++ b/src/api/api_polynomial.cpp
@@ -26,17 +26,6 @@ Notes:
 #include "util/scoped_timer.h"
 #include "ast/expr2var.h"
 
-namespace api {
-
-    pmanager::pmanager(reslimit& lim):
-        m_pm(lim, m_nm) {
-    }
-
-    pmanager::~pmanager() {
-    }
-
-};
-
 extern "C" {
 
     Z3_ast_vector Z3_API Z3_polynomial_subresultants(Z3_context c, Z3_ast p, Z3_ast q, Z3_ast x) {
diff --git a/src/api/api_polynomial.h b/src/api/api_polynomial.h
index fbb1e7e13..a31f6c2b8 100644
--- a/src/api/api_polynomial.h
+++ b/src/api/api_polynomial.h
@@ -23,13 +23,13 @@ Notes:
 
 namespace api {
     
-    class pmanager {
+    class pmanager final {
         unsynch_mpz_manager m_nm;
         polynomial::manager m_pm;
         // TODO: add support for caching expressions -> polynomial and back
     public:
-        pmanager(reslimit& limx);
-        virtual ~pmanager();
+        pmanager(reslimit& lim) : m_pm(lim, m_nm) {}
+        ~pmanager() {}
         polynomial::manager & pm() { return m_pm; }
     };
 

From 009708ed07c487f6ec031f6f4d47ad00fa459b80 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Mon, 9 Jul 2018 10:52:27 +0100
Subject: [PATCH 15/15] remove unneeded creation of tmp mpz_manager

---
 src/math/polynomial/algebraic_numbers.cpp | 20 ++++++++------------
 src/util/mpq.h                            |  6 ++++++
 2 files changed, 14 insertions(+), 12 deletions(-)

diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp
index 5811811fc..aa4fc5a39 100644
--- a/src/math/polynomial/algebraic_numbers.cpp
+++ b/src/math/polynomial/algebraic_numbers.cpp
@@ -2629,17 +2629,15 @@ namespace algebraic_numbers {
             }
             else if (a.is_basic()) {
                 mpq const & v = basic_value(a);
-                scoped_mpz neg_n(qm());
+                mpz neg_n;
                 qm().set(neg_n, v.numerator());
                 qm().neg(neg_n);
-                unsynch_mpz_manager zmgr;
-                // FIXME: remove these copies
-                mpz coeffs[2] = { zmgr.dup(neg_n.get()), zmgr.dup(v.denominator()) };
+                mpz coeffs[2] = { std::move(neg_n), qm().dup(v.denominator()) };
                 out << "(";
                 upm().display(out, 2, coeffs, "#");
                 out << ", 1)"; // first root of the polynomial d*# - n
-                zmgr.del(coeffs[0]);
-                zmgr.del(coeffs[1]);
+                qm().del(coeffs[0]);
+                qm().del(coeffs[1]);
             }
             else {
                 algebraic_cell * c = a.to_algebraic();
@@ -2679,17 +2677,15 @@ namespace algebraic_numbers {
             }
             else if (a.is_basic()) {
                 mpq const & v = basic_value(a);
-                scoped_mpz neg_n(qm());
+                mpz neg_n;
                 qm().set(neg_n, v.numerator());
                 qm().neg(neg_n);
-                unsynch_mpz_manager zmgr;
-                // FIXME: remove these copies
-                mpz coeffs[2] = { zmgr.dup(neg_n.get()), zmgr.dup(v.denominator()) };
+                mpz coeffs[2] = { std::move(neg_n), qm().dup(v.denominator()) };
                 out << "(root-obj ";
                 upm().display_smt2(out, 2, coeffs, "x");
                 out << " 1)"; // first root of the polynomial d*# - n
-                zmgr.del(coeffs[0]);
-                zmgr.del(coeffs[1]);
+                qm().del(coeffs[0]);
+                qm().del(coeffs[1]);
             }
             else {
                 algebraic_cell * c = a.to_algebraic();
diff --git a/src/util/mpq.h b/src/util/mpq.h
index 1bccabc74..b7bdbf400 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -714,6 +714,12 @@ public:
         return temp;
     }
 
+    mpz dup(const mpz & source) {
+        mpz temp;
+        set(temp, source);
+        return temp;
+    }
+
     void swap(mpz & a, mpz & b) { mpz_manager<SYNCH>::swap(a, b); }
 
     void swap(mpq & a, mpq & b) {