diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index f15f5abd9..03600131e 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -239,7 +239,6 @@ protected:
     func_decl * mk_num_decl(unsigned num_parameters, parameter const * parameters, unsigned arity);
 
     void get_offset_term(app * a, expr * & t, rational & offset) const;
-
 public:
     bv_decl_plugin();
 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index d0625d705..49656b05c 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1076,7 +1076,9 @@ public:
             mk_axiom(mk_literal(lo));
             if (m.has_trace_stream()) {
                 m.trace_stream() << "[end-of-instance]\n";
-                th.log_axiom_instantiation(m.mk_not(hi));
+                expr_ref body(m);
+                body = m.mk_not(hi);
+                th.log_axiom_instantiation(body);
             }
             mk_axiom(~mk_literal(hi));
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";