From 6ee39415235ce7b8a329192ab445e3529b3fc1ef Mon Sep 17 00:00:00 2001
From: nilsbecker <nbecker@student.ethz.ch>
Date: Sat, 23 Feb 2019 12:08:08 +0100
Subject: [PATCH] more cleanup

---
 src/ast/bv_decl_plugin.cpp      |  24 +++---
 src/ast/bv_decl_plugin.h        |  18 ++--
 src/smt/smt_quantifier.cpp      |   8 +-
 src/smt/smt_quantifier.h        |   3 -
 src/smt/theory_arith_core.h     |   6 +-
 src/smt/theory_arith_int.h      |  12 ++-
 src/smt/theory_arith_nl.h       |   6 +-
 src/smt/theory_array_base.cpp   |  12 ++-
 src/smt/theory_bv.cpp           |  24 +++++-
 src/smt/theory_datatype.cpp     |  28 +++---
 src/smt/theory_diff_logic_def.h |   6 +-
 src/smt/theory_dl.cpp           |   6 +-
 src/smt/theory_jobscheduler.cpp |  57 +++++++++---
 src/smt/theory_lra.cpp          | 148 ++++++++++++++++++++++++++------
 src/smt/theory_recfun.cpp       |  24 +++++-
 src/smt/theory_seq.cpp          |  49 ++++++++---
 src/util/mpz.cpp                |   1 -
 17 files changed, 328 insertions(+), 104 deletions(-)

diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index 29b3fd8a8..738444b3b 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -866,24 +866,20 @@ app * bv_util::mk_numeral(rational const & val, sort* s) const {
     return mk_numeral(val, bv_size);
 }
 
- void bv_util::log_mk_numeral(rational const & val, unsigned bv_size) const {
-    if (bv_size % 4 == 0) {
-        m_manager.trace_stream() << "#x";
-        val.display_hex(m_manager.trace_stream(), bv_size);
-        m_manager.trace_stream() << "\n";
-    } else {
-        m_manager.trace_stream() << "#b";
-        val.display_bin(m_manager.trace_stream(), bv_size);
-        m_manager.trace_stream() << "\n";
-    }
- }
-
 app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const {
     parameter p[2] = { parameter(val), parameter(static_cast<int>(bv_size)) };
     app * r = m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, nullptr);
 
     if (m_plugin->log_constant_meaning_prelude(r)) {
-        log_mk_numeral(val, bv_size);
+        if (bv_size % 4 == 0) {
+            m_manager.trace_stream() << "#x";
+            val.display_hex(m_manager.trace_stream(), bv_size);
+            m_manager.trace_stream() << "\n";
+        } else {
+            m_manager.trace_stream() << "#b";
+            val.display_bin(m_manager.trace_stream(), bv_size);
+            m_manager.trace_stream() << "\n";
+        }
     }
 
     return r;
@@ -904,4 +900,4 @@ app * bv_util::mk_bv2int(expr* e) {
     sort* s = m_manager.mk_sort(m_manager.mk_family_id("arith"), INT_SORT);
     parameter p(s);
     return m_manager.mk_app(get_fid(), OP_BV2INT, 1, &p, 1, &e);
-}
\ No newline at end of file
+}
diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index f69ce1c02..f15f5abd9 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -126,6 +126,7 @@ inline func_decl * get_div0_decl(ast_manager & m, func_decl * decl) {
 }
 
 class bv_decl_plugin : public decl_plugin {
+    friend class bv_util;
 protected:
     symbol m_bv_sym;
     symbol m_concat_sym;
@@ -239,7 +240,6 @@ protected:
 
     void get_offset_term(app * a, expr * & t, rational & offset) const;
 
-    friend class bv_util;
 public:
     bv_decl_plugin();
 
@@ -381,8 +381,6 @@ class bv_util : public bv_recognizers {
     ast_manager &    m_manager;
     bv_decl_plugin * m_plugin;
 
-    void log_mk_numeral(rational const & val, unsigned bv_size) const;
-
 public:
     bv_util(ast_manager & m);
 
@@ -436,13 +434,12 @@ public:
     app * mk_bvsmul_no_udfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_UDFL, n, m); }
     app * mk_bvumul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_NO_OVFL, n, m); }
 
-    app * mk_bv(unsigned n, expr* const* es) {
-        app * r = m_manager.mk_app(get_fid(), OP_MKBV, n, es);
-
+    private:
+    void log_bv_from_exprs(app * r, unsigned n, expr* const* es) {
         if (m_manager.has_trace_stream()) {
             for (unsigned i = 0; i < n; ++i) {
                 if (!m_manager.is_true(es[i]) && !m_manager.is_true(es[i]))
-                    return r;
+                    return;
             } 
 
             if (m_plugin->log_constant_meaning_prelude(r)) {
@@ -474,6 +471,13 @@ public:
                 m_manager.trace_stream() << ")\n";
             }
         }
+    }
+
+public:
+    app * mk_bv(unsigned n, expr* const* es) {
+        app * r = m_manager.mk_app(get_fid(), OP_MKBV, n, es);
+
+        log_bv_from_exprs(r, n, es);
 
         return r;
     }
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index cb7d12d2e..008da06ec 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -32,6 +32,8 @@ namespace smt {
 
     quantifier_manager_plugin * mk_default_plugin();
 
+    void log_single_justification(std::ostream & out, enode *en, obj_hashtable<enode> &visited, context &ctx, ast_manager &m);
+
     /**
          \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.
@@ -68,7 +70,7 @@ namespace smt {
          \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 quantifier_manager::log_single_justification(std::ostream & out, enode *en, obj_hashtable<enode> &visited, context &ctx, ast_manager &m) {
+    void log_single_justification(std::ostream & out, enode *en, obj_hashtable<enode> &visited, context &ctx, ast_manager &m) {
         smt::literal lit;
         unsigned num_args;
         enode *target = en->get_trans_justification().m_target;
@@ -87,8 +89,8 @@ namespace smt {
                 num_args = en->get_num_args();
 
                 for (unsigned i = 0; i < num_args; ++i) {
-                    log_justification_to_root(out, en->get_arg(i), visited, ctx, m);
-                    log_justification_to_root(out, target->get_arg(i), visited, ctx, m);
+                    quantifier_manager::log_justification_to_root(out, en->get_arg(i), visited, ctx, m);
+                    quantifier_manager::log_justification_to_root(out, target->get_arg(i), visited, ctx, m);
                 }
 
                 out << "[eq-expl] #" << en->get_owner_id() << " cg";
diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h
index a126407d7..a25ada87e 100644
--- a/src/smt/smt_quantifier.h
+++ b/src/smt/smt_quantifier.h
@@ -53,9 +53,6 @@ namespace smt {
         unsigned get_generation(quantifier * q) const;
 
         static void log_justification_to_root(std::ostream & log, enode *en, obj_hashtable<enode> &already_visited, context &ctx, ast_manager &m);
-      private:
-         static void log_single_justification(std::ostream & out, enode *en, obj_hashtable<enode> &already_visited, context &ctx, ast_manager &m);
-      public:
 
         bool add_instance(quantifier * q, app * pat,
                           unsigned num_bindings,
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 283085ae3..effc0677b 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -447,7 +447,11 @@ namespace smt {
               tout << l_ante << "\n" << l_conseq << "\n";);
 
         // literal lits[2] = {l_ante, l_conseq};
-        if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(ante, conseq));
+        if (m.has_trace_stream()) {
+            app_ref body(m);
+            body = m.mk_or(ante, conseq);
+            log_axiom_instantiation(body);
+        }
         mk_clause(l_ante, l_conseq, 0, nullptr);
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
 
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index f4e901de4..ffbb9770d 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -210,7 +210,11 @@ namespace smt {
         expr_ref bound(m);
         expr* e = get_enode(v)->get_owner();
         bound  = m_util.mk_ge(e, m_util.mk_numeral(_k, m_util.is_int(e)));
-        if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(to_app(bound), m.mk_not(to_app(bound))));
+        if (m.has_trace_stream()) {
+            app_ref body(m);
+            body = m.mk_or(to_app(bound), m.mk_not(to_app(bound)));
+            log_axiom_instantiation(body);
+        }
         TRACE("arith_int", tout << mk_bounded_pp(bound, m) << "\n";);
         context & ctx = get_context();
         ctx.internalize(bound, true);
@@ -368,7 +372,11 @@ namespace smt {
         mk_polynomial_ge(pol.size(), pol.c_ptr(), unsat_row[0]+rational(1), p2);
         
         context& ctx = get_context();
-        if (get_manager().has_trace_stream()) log_axiom_instantiation(get_manager().mk_or(p1, p2));
+        if (get_manager().has_trace_stream()) {
+            app_ref body(get_manager());
+            body = get_manager().mk_or(p1, p2);
+            log_axiom_instantiation(body);
+        }
         ctx.internalize(p1, false);
         ctx.internalize(p2, false);
         literal l1(ctx.get_literal(p1)), l2(ctx.get_literal(p2));
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index 457c6e068..80687dd18 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -790,7 +790,11 @@ namespace smt {
         TRACE("non_linear", tout << "new bound:\n" << mk_pp(bound, get_manager()) << "\n";);
         context & ctx = get_context();
         ast_manager & m = get_manager();
-        if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(bound, m.mk_not(bound)));
+        if (m.has_trace_stream()) {
+            app_ref body(m);
+            body = m.mk_or(bound, m.mk_not(bound));
+            log_axiom_instantiation(body);
+        }
         ctx.internalize(bound, true);
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
         ctx.mark_as_relevant(bound);
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index 9ba520c9d..9706f7160 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -191,7 +191,11 @@ namespace smt {
             TRACE("array_map_bug", tout << "axiom2:\n";
                   tout << mk_ismt2_pp(idx1->get_owner(), m) << "\n=\n" << mk_ismt2_pp(idx2->get_owner(), m);
                   tout << "\nimplies\n" << mk_ismt2_pp(conseq_expr, m) << "\n";);
-            if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(ctx.bool_var2expr(ante.var()), conseq_expr));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_or(ctx.bool_var2expr(ante.var()), conseq_expr);
+                log_axiom_instantiation(body);
+            }
             assert_axiom(ante, conseq);
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
         }
@@ -335,7 +339,11 @@ namespace smt {
         literal sel1_eq_sel2 = mk_eq(sel1, sel2, true);
         ctx.mark_as_relevant(n1_eq_n2);
         ctx.mark_as_relevant(sel1_eq_sel2);
-        if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_not(ctx.bool_var2expr(n1_eq_n2.var())), m.mk_not(ctx.bool_var2expr(sel1_eq_sel2.var()))));
+        if (m.has_trace_stream()) {
+            app_ref body(m);
+            body = m.mk_implies(m.mk_not(ctx.bool_var2expr(n1_eq_n2.var())), m.mk_not(ctx.bool_var2expr(sel1_eq_sel2.var())));
+            log_axiom_instantiation(body);
+        }
         assert_axiom(n1_eq_n2, ~sel1_eq_sel2);
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
     }
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 0301a86e1..2383f62cc 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -255,7 +255,11 @@ namespace smt {
         context & ctx    = get_context();
         ast_manager & m  = get_manager();
         expr * eq    = ctx.bool_var2expr(l.var());
-        if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_eq(mk_bit2bool(get_enode(v1)->get_owner(), idx), m.mk_not(mk_bit2bool(get_enode(v2)->get_owner(), idx))), m.mk_not(eq)));
+        if (m.has_trace_stream()) {
+            app_ref body(m);
+            body = m.mk_implies(m.mk_eq(mk_bit2bool(get_enode(v1)->get_owner(), idx), m.mk_not(mk_bit2bool(get_enode(v2)->get_owner(), idx))), m.mk_not(eq));
+            log_axiom_instantiation(body);
+        }
         ctx.mk_th_axiom(get_id(), 1, &l);
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
         if (ctx.relevancy()) {
@@ -472,7 +476,11 @@ namespace smt {
             e1 = mk_bit2bool(o1, i);
             e2 = mk_bit2bool(o2, i);
             literal eq = mk_eq(e1, e2, true);
-            if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_not(ctx.bool_var2expr(oeq.var()))));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_not(ctx.bool_var2expr(oeq.var())));
+                log_axiom_instantiation(body);
+            }
             ctx.mk_th_axiom(get_id(),  l1, ~l2, ~eq);
             ctx.mk_th_axiom(get_id(), ~l1,  l2, ~eq);
             ctx.mk_th_axiom(get_id(),  l1,  l2,  eq);
@@ -1228,7 +1236,11 @@ namespace smt {
             exprs.push_back(diff);
         }
         m_stats.m_num_diseq_dynamic++;
-        if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_or(exprs.size(), exprs.c_ptr())));
+        if (m.has_trace_stream()) {
+            app_ref body(m);
+            body = m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_or(exprs.size(), exprs.c_ptr()));
+            log_axiom_instantiation(body);
+        }
         ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
     }
@@ -1341,7 +1353,11 @@ namespace smt {
             lits.push_back(antecedent);
             literal eq = mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), false);
             lits.push_back(~eq);
-            if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_implies(ctx.bool_var2expr(consequent.var()), ctx.bool_var2expr(antecedent.var()))));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_implies(ctx.bool_var2expr(consequent.var()), ctx.bool_var2expr(antecedent.var())));
+                log_axiom_instantiation(body);
+            }
             ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
      
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index 0fac42501..2ae4dad20 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -140,12 +140,14 @@ namespace smt {
             args.push_back(acc);
         }
         expr * mk       = m.mk_app(c, args.size(), args.c_ptr());
-        app_ref ax(m);
-        ax = m.mk_eq(n->get_owner(), mk);
-        if (antecedent != null_literal) {
-            ax = m.mk_implies(get_context().bool_var2expr(antecedent.var()), ax);
+        if (m.has_trace_stream()) {
+            app_ref body(m);
+            body = m.mk_eq(n->get_owner(), mk);
+            if (antecedent != null_literal) {
+                body = m.mk_implies(get_context().bool_var2expr(antecedent.var()), body);
+            }
+            log_axiom_instantiation(body, 1, &n);
         }
-        if (m.has_trace_stream()) log_axiom_instantiation(ax, 1, &n);
         assert_eq_axiom(n, mk, antecedent);
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
     }
@@ -175,9 +177,11 @@ namespace smt {
         for (func_decl * acc : accessors) {
             app * acc_app     = m.mk_app(acc, n->get_owner());
             enode * arg       = n->get_arg(i);
-            app_ref eq(m);
-            eq = m.mk_eq(arg->get_owner(), acc_app);
-            if (m.has_trace_stream()) log_axiom_instantiation(eq, base_id + 3*i, bindings.size(), bindings.c_ptr(), base_id - 3, used_enodes);
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_eq(arg->get_owner(), acc_app);
+                log_axiom_instantiation(body, base_id + 3*i, bindings.size(), bindings.c_ptr(), base_id - 3, used_enodes);
+            }
             assert_eq_axiom(arg, acc_app, null_literal);
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
             ++i;
@@ -236,9 +240,11 @@ namespace smt {
                 arg = ctx.get_enode(acc_app);
             }
             app * acc_own = m.mk_app(acc1, own);
-            app_ref imp(m);
-            imp = m.mk_implies(rec_app, m.mk_eq(arg->get_owner(), acc_own));
-            if (m.has_trace_stream()) log_axiom_instantiation(imp, 1, &n);
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_implies(rec_app, m.mk_eq(arg->get_owner(), acc_own));
+                log_axiom_instantiation(body, 1, &n);
+            }
             assert_eq_axiom(arg, acc_own, is_con); 
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
         }
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index b7bd9adf1..3a9553f95 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -1009,7 +1009,11 @@ void theory_diff_logic<Ext>::new_eq_or_diseq(bool is_eq, theory_var v1, theory_v
         t2 = m_util.mk_numeral(k, m.get_sort(s2.get()));
         // t1 - s1 = k
         eq = m.mk_eq(s2.get(), t2.get());
-        if (m.has_trace_stream()) log_axiom_instantiation(m.mk_eq(m.mk_eq(m_util.mk_add(s1, t2), t1), eq));
+        if (m.has_trace_stream()) {
+            app_ref body(m);
+            body = m.mk_eq(m.mk_eq(m_util.mk_add(s1, t2), t1), eq);
+            log_axiom_instantiation(body);
+        }
         
         TRACE("diff_logic", 
               tout << v1 << " .. " << v2 << "\n";
diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp
index be99b1234..6bbc8d03d 100644
--- a/src/smt/theory_dl.cpp
+++ b/src/smt/theory_dl.cpp
@@ -256,7 +256,11 @@ namespace smt {
             lt = u().mk_lt(x,y);
             le = b().mk_ule(m().mk_app(r,y),m().mk_app(r,x)); 
             context& ctx = get_context();
-            if (m().has_trace_stream()) log_axiom_instantiation(m().mk_eq(lt, le));
+            if (m().has_trace_stream()) {
+                app_ref body(m());
+                body = m().mk_eq(lt, le);
+                log_axiom_instantiation(body);
+            }
             ctx.internalize(lt, false);
             ctx.internalize(le, false);
             literal lit1(ctx.get_literal(lt));
diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp
index 6b1034ab6..031988bc6 100644
--- a/src/smt/theory_jobscheduler.cpp
+++ b/src/smt/theory_jobscheduler.cpp
@@ -307,7 +307,9 @@ namespace smt {
             // Initialization ensures that satisfiable states have completion time below end.
             ast_manager& m = get_manager();
             if (m.has_trace_stream()) {
-                log_axiom_instantiation(m.mk_implies(m.mk_and(m.mk_eq(eq.first->get_owner(), eq.second->get_owner()), ctx.bool_var2expr(start_ge_lo.var())), ctx.bool_var2expr(end_ge_lo.var())));
+                app_ref body(m);
+                body = m.mk_implies(m.mk_and(m.mk_eq(eq.first->get_owner(), eq.second->get_owner()), ctx.bool_var2expr(start_ge_lo.var())), ctx.bool_var2expr(end_ge_lo.var()));
+                log_axiom_instantiation(body);
                 m.trace_stream() << "[end-of-instance]\n";
             }
             region& r = ctx.get_region();
@@ -386,7 +388,9 @@ namespace smt {
         ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, CLS_AUX_LEMMA, nullptr);
         ast_manager& m = get_manager();
         if (m.has_trace_stream()) {
-            log_axiom_instantiation(m.mk_implies(m.mk_and(ctx.bool_var2expr(lits[0].var()), ctx.bool_var2expr(lits[1].var()), ctx.bool_var2expr(lits[2].var())), ctx.bool_var2expr(lits[3].var())));
+            app_ref body(m);
+            body = m.mk_implies(m.mk_and(ctx.bool_var2expr(lits[0].var()), ctx.bool_var2expr(lits[1].var()), ctx.bool_var2expr(lits[2].var())), ctx.bool_var2expr(lits[3].var()));
+            log_axiom_instantiation(body);
             m.trace_stream() << "[end-of-instance]\n";
         }
         return true;
@@ -810,7 +814,11 @@ namespace smt {
         job_info const& ji = m_jobs[j];
         literal l2 = mk_le(ji.m_end, jr.m_finite_capacity_end);
         context& ctx = get_context();
-        if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(l2.var())));
+        if (m.has_trace_stream()) {
+            app_ref body(m);
+            body = m.mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(l2.var()));
+            log_axiom_instantiation(body);
+        }
         ctx.mk_th_axiom(get_id(), ~eq, l2);
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
 #endif
@@ -822,13 +830,21 @@ namespace smt {
         time_t t;
         if (lst(j, r, t)) {
             literal le = mk_le(m_jobs[j].m_start, t);
-            if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(le.var())));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(le.var()));
+                log_axiom_instantiation(body);
+            }
             ctx.mk_th_axiom(get_id(), ~eq, le);
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
         }
         else {
             eq.neg();
-            if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_not(ctx.bool_var2expr(eq.var())));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_not(ctx.bool_var2expr(eq.var()));
+                log_axiom_instantiation(body);
+            }
             ctx.mk_th_axiom(get_id(), 1, &eq);
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
         }
@@ -842,7 +858,11 @@ namespace smt {
         vector<res_available>& available = m_resources[r].m_available;
         literal l2 = mk_ge(m_jobs[j].m_start, available[idx].m_start);
         context& ctx = get_context();
-        if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(l2.var())));
+        if (m.has_trace_stream()) {
+            app_ref body(m);
+            body = m.mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(l2.var()));
+            log_axiom_instantiation(body);
+        }
         ctx.mk_th_axiom(get_id(), ~eq, l2);
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
     }
@@ -856,8 +876,11 @@ namespace smt {
         literal l2 = mk_ge(m_jobs[j].m_start, available[idx1].m_start);
         literal l3 = mk_le(m_jobs[j].m_start, available[idx].m_end);
         context& ctx = get_context();
-        ast_manager& m = get_manager();
-        if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_or(ctx.bool_var2expr(l2.var()), ctx.bool_var2expr(l3.var()))));
+        if (m.has_trace_stream()) {
+            app_ref body(m);
+            body = m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_or(ctx.bool_var2expr(l2.var()), ctx.bool_var2expr(l3.var())));
+            log_axiom_instantiation(body);
+        }
         ctx.mk_th_axiom(get_id(), ~eq, l2, l3);        
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
     }
@@ -871,8 +894,11 @@ namespace smt {
         literal l2 = mk_le(m_jobs[j].m_end, available[idx].m_end);
         literal l3 = mk_ge(m_jobs[j].m_start, available[idx1].m_start);
         context& ctx = get_context();
-        ast_manager& m = get_manager();
-        if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_or(ctx.bool_var2expr(l2.var()), ctx.bool_var2expr(l3.var()))));
+        if (m.has_trace_stream()) {
+            app_ref body(m);
+            body = m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_or(ctx.bool_var2expr(l2.var()), ctx.bool_var2expr(l3.var())));
+            log_axiom_instantiation(body);
+        }
         ctx.mk_th_axiom(get_id(), ~eq, l2, l3);
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
     }    
@@ -883,7 +909,6 @@ namespace smt {
     bool theory_jobscheduler::split_job2resource(unsigned j) {
         job_info const& ji = m_jobs[j];
         context& ctx = get_context();
-        ast_manager& m = get_manager();
         if (ji.m_is_bound) return false;
         auto const& jrs = ji.m_resources;
         for (job_resource const& jr : jrs) {
@@ -895,7 +920,9 @@ namespace smt {
                 continue;
             literal eq = mk_eq_lit(e1, e2);
             if (m.has_trace_stream()) {
-                log_axiom_instantiation(m.mk_or(ctx.bool_var2expr(eq.var()), m.mk_not(ctx.bool_var2expr(eq.var()))));
+                app_ref body(m);
+                body = m.mk_or(ctx.bool_var2expr(eq.var()), m.mk_not(ctx.bool_var2expr(eq.var())));
+                log_axiom_instantiation(body);
                 m.trace_stream() << "[end-of-instance]\n";
             }
             if (ctx.get_assignment(eq) != l_false) {
@@ -916,7 +943,11 @@ namespace smt {
             lits.push_back(eq);
             exprs.push_back(ctx.bool_var2expr(eq.var()));
         }
-        if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(exprs.size(), exprs.c_ptr()));
+        if (m.has_trace_stream()) {
+            app_ref body(m);
+            body = m.mk_or(exprs.size(), exprs.c_ptr());
+            log_axiom_instantiation(body);
+        }
         ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
         return true;
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 5703e34dd..d0625d705 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1030,7 +1030,11 @@ public:
         literal dgez = mk_literal(degz_expr);
         literal pos = th.mk_eq(rem, mod,  false);
         literal neg = th.mk_eq(rem, mmod, false);
-        if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_ite(degz_expr, ctx().bool_var2expr(pos.var()), ctx().bool_var2expr(neg.var())));
+        if (m.has_trace_stream()) {
+            app_ref body(m);
+            body = m.mk_ite(degz_expr, ctx().bool_var2expr(pos.var()), ctx().bool_var2expr(neg.var()));
+            th.log_axiom_instantiation(body);
+        }
         mk_axiom(~dgez, pos);
         mk_axiom( dgez, neg);                    
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
@@ -1041,7 +1045,11 @@ public:
         if (a.is_zero(q)) return;
         literal eqz = th.mk_eq(q, a.mk_real(0), false);
         literal eq  = th.mk_eq(a.mk_mul(q, a.mk_div(p, q)), p, false);
-        if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(ctx().bool_var2expr(eqz.var())), ctx().bool_var2expr(eq.var())));
+        if (m.has_trace_stream()) {
+            app_ref body(m);
+            body = m.mk_implies(m.mk_not(ctx().bool_var2expr(eqz.var())), ctx().bool_var2expr(eq.var()));
+            th.log_axiom_instantiation(body);
+        }
         mk_axiom(eqz, eq);
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
     }
@@ -1052,7 +1060,11 @@ public:
         expr* x = nullptr, *y = nullptr;
         VERIFY (a.is_to_int(n, x));            
         if (a.is_to_real(x, y)) {
-            if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_eq(n, y));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_eq(n, y);
+                th.log_axiom_instantiation(body);
+            }
             mk_axiom(th.mk_eq(y, n, false));
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
         }
@@ -1077,7 +1089,11 @@ public:
         VERIFY(a.is_is_int(n, x));
         literal eq = th.mk_eq(a.mk_to_real(a.mk_to_int(x)), x, false);
         literal is_int = ctx().get_literal(n);
-        if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_iff(n, ctx().bool_var2expr(eq.var())));
+        if (m.has_trace_stream()) {
+            app_ref body(m);
+            body = m.mk_iff(n, ctx().bool_var2expr(eq.var()));
+            th.log_axiom_instantiation(body);
+        }
         mk_axiom(~is_int, eq);
         mk_axiom(is_int, ~eq);
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
@@ -1134,28 +1150,56 @@ public:
 
         context& c = ctx();
         if (!k.is_zero()) {
-            if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var())));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var()));
+                th.log_axiom_instantiation(body);
+            }
             mk_axiom(eq);
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
-            if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var())));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var()));
+                th.log_axiom_instantiation(body);
+            }
             mk_axiom(mod_ge_0);
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
-            if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), a.mk_le(mod, upper)));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), a.mk_le(mod, upper));
+                th.log_axiom_instantiation(body);
+            }
             mk_axiom(mk_literal(a.mk_le(mod, upper)));
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
             if (k.is_pos()) {
-                if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var())));
+                if (m.has_trace_stream()) {
+                    app_ref body(m);
+                    body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var()));
+                    th.log_axiom_instantiation(body);
+                }
                 mk_axiom(~p_ge_0, div_ge_0);
                 if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
-                if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var())));
+                if (m.has_trace_stream()) {
+                    app_ref body(m);
+                    body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var()));
+                    th.log_axiom_instantiation(body);
+                }
                 mk_axiom(~p_le_0, div_le_0);
                 if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
             }
             else {
-                if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var())));
+                if (m.has_trace_stream()) {
+                    app_ref body(m);
+                    body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var()));
+                    th.log_axiom_instantiation(body);
+                }
                 mk_axiom(~p_ge_0, div_le_0);
                 if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
-                if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var())));
+                if (m.has_trace_stream()) {
+                    app_ref body(m);
+                    body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var()));
+                    th.log_axiom_instantiation(body);
+                }
                 mk_axiom(~p_le_0, div_ge_0);
                 if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
             }
@@ -1169,30 +1213,62 @@ public:
             // q >= 0 or (p mod q) < -q
             literal q_ge_0 = mk_literal(a.mk_ge(q, zero));
             literal q_le_0 = mk_literal(a.mk_le(q, zero));
-            if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var())));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var()));
+                th.log_axiom_instantiation(body);
+            }
             mk_axiom(q_ge_0, eq);
             mk_axiom(q_le_0, eq);
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
-            if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var())));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var()));
+                th.log_axiom_instantiation(body);
+            }
             mk_axiom(q_ge_0, mod_ge_0);
             mk_axiom(q_le_0, mod_ge_0);
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
-            if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_sub(mod, q), zero)));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_sub(mod, q), zero));
+                th.log_axiom_instantiation(body);
+            }
             mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero)));
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
-            if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero)));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero));
+                th.log_axiom_instantiation(body);
+            }
             mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero)));        
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
-            if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var())));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var()));
+                th.log_axiom_instantiation(body);
+            }
             mk_axiom(q_le_0, ~p_ge_0, div_ge_0); 
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
-            if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var())));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var()));
+                th.log_axiom_instantiation(body);
+            }
             mk_axiom(q_le_0, ~p_le_0, div_le_0); 
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
-            if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var())));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var()));
+                th.log_axiom_instantiation(body);
+            }
             mk_axiom(q_ge_0, ~p_ge_0, div_le_0); 
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
-            if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var())));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var()));
+                th.log_axiom_instantiation(body);
+            }
             mk_axiom(q_ge_0, ~p_le_0, div_ge_0); 
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
         }
@@ -1206,7 +1282,11 @@ public:
                 exprs.push_back(c.bool_var2expr(mod_j.var()));
                 ctx().mark_as_relevant(mod_j);
             }
-            if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_or(exprs.size(), exprs.c_ptr()));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_or(exprs.size(), exprs.c_ptr());
+                th.log_axiom_instantiation(body);
+            }
             ctx().mk_th_axiom(get_id(), lits.size(), lits.begin());                
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
         }            
@@ -1643,10 +1723,18 @@ public:
                 literal p_ge_r1  = mk_literal(a.mk_ge(p, a.mk_numeral(lo, true)));
                 literal n_le_div = mk_literal(a.mk_le(n, a.mk_numeral(div_r, true)));
                 literal n_ge_div = mk_literal(a.mk_ge(n, a.mk_numeral(div_r, true)));
-                if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(ctx().bool_var2expr(p_le_r1.var()), ctx().bool_var2expr(n_le_div.var())));
+                if (m.has_trace_stream()) {
+                    app_ref body(m);
+                    body = m.mk_implies(ctx().bool_var2expr(p_le_r1.var()), ctx().bool_var2expr(n_le_div.var()));
+                    th.log_axiom_instantiation(body);
+                }
                 mk_axiom(~p_le_r1, n_le_div); 
                 if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
-                if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(ctx().bool_var2expr(p_ge_r1.var()), ctx().bool_var2expr(n_ge_div.var())));
+                if (m.has_trace_stream()) {
+                    app_ref body(m);
+                    body = m.mk_implies(ctx().bool_var2expr(p_ge_r1.var()), ctx().bool_var2expr(n_ge_div.var()));
+                    th.log_axiom_instantiation(body);
+                }
                 mk_axiom(~p_ge_r1, n_ge_div);
                 if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
 
@@ -1687,10 +1775,18 @@ public:
             literal pq_rhs   = ~mk_literal(a.mk_ge(pqr, zero));
             literal n_le_div = mk_literal(a.mk_le(n, divc));
             literal n_ge_div = mk_literal(a.mk_ge(n, divc)); 
-            if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(ctx().bool_var2expr(pq_lhs.var()), ctx().bool_var2expr(n_le_div.var())));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_implies(ctx().bool_var2expr(pq_lhs.var()), ctx().bool_var2expr(n_le_div.var()));
+                th.log_axiom_instantiation(body);
+            }
             mk_axiom(pq_lhs, n_le_div); 
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
-            if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(ctx().bool_var2expr(pq_rhs.var()), ctx().bool_var2expr(n_ge_div.var())));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_implies(ctx().bool_var2expr(pq_rhs.var()), ctx().bool_var2expr(n_ge_div.var()));
+                th.log_axiom_instantiation(body);
+            }
             mk_axiom(pq_rhs, n_ge_div);
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
             TRACE("arith",
@@ -1808,7 +1904,9 @@ public:
             TRACE("arith", tout << "branch\n";);
             app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper());
             if (m.has_trace_stream()) {
-                th.log_axiom_instantiation(m.mk_or(b, m.mk_not(b)));
+                app_ref body(m);
+                body = m.mk_or(b, m.mk_not(b));
+                th.log_axiom_instantiation(body);
                 m.trace_stream() << "[end-of-instance]\n";
             }
             IF_VERBOSE(2, verbose_stream() << "branch " << b << "\n";);
diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
index 08434b0d0..46cb3896a 100644
--- a/src/smt/theory_recfun.cpp
+++ b/src/smt/theory_recfun.cpp
@@ -360,17 +360,29 @@ namespace smt {
                 guards.push_back(~guard);
                 exprs.push_back(m.mk_not(ga));
                 literal c[2] = {~concl, guard};
-                if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(pred_applied, ga));
+                if (m.has_trace_stream()) {
+                    app_ref body(m);
+                    body = m.mk_implies(pred_applied, ga);
+                    log_axiom_instantiation(body);
+                }
                 ctx().mk_th_axiom(get_id(), 2, c);
                 if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
             }
-            if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_not(pred_applied), m.mk_or(exprs.size(), exprs.c_ptr())));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_implies(m.mk_not(pred_applied), m.mk_or(exprs.size(), exprs.c_ptr()));
+                log_axiom_instantiation(body);
+            }
             ctx().mk_th_axiom(get_id(), guards);
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
         }
         // the disjunction of branches is asserted
         // to close the available cases. 
-        if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(pred_exprs.size(), pred_exprs.c_ptr()));
+        if (m.has_trace_stream()) {
+            app_ref body(m);
+            body = m.mk_or(pred_exprs.size(), pred_exprs.c_ptr());
+            log_axiom_instantiation(body);
+        }
         ctx().mk_th_axiom(get_id(), preds);
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
     }
@@ -407,7 +419,11 @@ namespace smt {
             }
         }        
         clause.push_back(mk_eq_lit(lhs, rhs));
-        if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_and(exprs.size(), exprs.c_ptr()), m.mk_eq(lhs, rhs)));
+        if (m.has_trace_stream()) {
+            app_ref body(m);
+            body = m.mk_implies(m.mk_and(exprs.size(), exprs.c_ptr()), m.mk_eq(lhs, rhs));
+            log_axiom_instantiation(body);
+        }
         ctx().mk_th_axiom(get_id(), clause);
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
         TRACEFN("body   " << pp_body_expansion(e,m));
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 72aea5909..488d3913e 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2167,8 +2167,9 @@ void theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits
     m_new_propagation = true;
     ctx.assign(lit, js);    
     if (m.has_trace_stream()) {
-        expr* expr = ctx.bool_var2expr(lit.var());
-        if (lit.sign()) expr = get_manager().mk_not(expr);
+        expr_ref expr(m);
+        expr = ctx.bool_var2expr(lit.var());
+        if (lit.sign()) expr = m.mk_not(expr);
         log_axiom_instantiation(expr);
         m.trace_stream() << "[end-of-instance]\n";
     }
@@ -2205,7 +2206,11 @@ void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) {
     justification* js = ctx.mk_justification(
         ext_theory_eq_propagation_justification(
             get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2));
-    if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_eq(n1->get_owner(), n2->get_owner()));
+    if (m.has_trace_stream()) {
+        app_ref body(m);
+        body = m.mk_eq(n1->get_owner(), n2->get_owner());
+        log_axiom_instantiation(body);
+    }
     ctx.assign_eq(n1, n2, eq_justification(js));
     if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
     m_new_propagation = true;
@@ -3184,10 +3189,12 @@ bool theory_seq::solve_nc(unsigned idx) {
             ptr_vector<expr> exprs;
             for (literal l : lits) {
                 expr* e = ctx.bool_var2expr(l.var());
-                if (l.sign()) e = get_manager().mk_not(e);
+                if (l.sign()) e = m.mk_not(e);
                 exprs.push_back(e);
             }
-            log_axiom_instantiation(get_manager().mk_or(exprs.size(), exprs.c_ptr()));
+            app_ref body(m);
+            body = m.mk_or(exprs.size(), exprs.c_ptr());
+            log_axiom_instantiation(body);
             m.trace_stream() << "[end-of-instance]\n";
         }
         return true;
@@ -4647,7 +4654,11 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
     }
     else {
         TRACE("seq", ctx.display_literals_verbose(tout, lits) << "\n";);
-        if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(n, get_manager().mk_or(exprs.size(), exprs.c_ptr())));
+        if (m.has_trace_stream()) {
+            app_ref body(m);
+            body = m.mk_implies(n, m.mk_or(exprs.size(), exprs.c_ptr()));
+            log_axiom_instantiation(body);
+        }
         ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
     }
@@ -5096,7 +5107,7 @@ literal theory_seq::mk_eq_empty(expr* _e, bool phase) {
 
 void theory_seq::push_lit_as_expr(literal l, ptr_vector<expr>& buf) {
     expr* e = get_context().bool_var2expr(l.var());
-    if (l.sign()) e = get_manager().mk_not(e);
+    if (l.sign()) e = m.mk_not(e);
     buf.push_back(e);
 }
 
@@ -5113,7 +5124,11 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
     TRACE("seq", ctx.display_literals_verbose(tout << "assert:\n", lits) << "\n";);
     m_new_propagation = true;
     ++m_stats.m_add_axiom;
-    if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_or(exprs.size(), exprs.c_ptr()));
+    if (m.has_trace_stream()) {
+        app_ref body(m);
+        body = m.mk_or(exprs.size(), exprs.c_ptr());
+        log_axiom_instantiation(body);
+    }
     ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
     if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
 }
@@ -5240,7 +5255,11 @@ void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
                 get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2));
 
     m_new_propagation = true;
-    if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_eq(e1, e2));
+    if (m.has_trace_stream()) {
+        app_ref body(m);
+        body = m.mk_eq(e1, e2);
+        log_axiom_instantiation(body);
+    }
     ctx.assign_eq(n1, n2, eq_justification(js));
     if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
 }
@@ -5288,7 +5307,11 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
                 lits.push_back(mk_literal(d));
             }
             ++m_stats.m_add_axiom;            
-            if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(e, get_manager().mk_or(disj.size(), disj.c_ptr())));
+            if (m.has_trace_stream()) {
+                app_ref body(m);
+                body = m.mk_implies(e, m.mk_or(disj.size(), disj.c_ptr()));
+                log_axiom_instantiation(body);
+            }
             ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
             for (expr* d : disj) {
@@ -5659,7 +5682,11 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
         lits.push_back(step);
         exprs.push_back(step_e);
     }
-    if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(acc, get_manager().mk_or(exprs.size(), exprs.c_ptr())));
+    if (m.has_trace_stream()) {
+        app_ref body(m);
+        body = m.mk_implies(acc, m.mk_or(exprs.size(), exprs.c_ptr()));
+        log_axiom_instantiation(body);
+    }
     ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
     if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
 
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 27d3c882c..6776acf65 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -1768,7 +1768,6 @@ void mpz_manager<SYNCH>::display_hex(std::ostream & out, mpz const & a, unsigned
 #endif
     }
     out.copyfmt(fmt);
-    out << std::dec;
 }
 
 void display_binary_data(std::ostream &out, unsigned val, unsigned numBits) {