strengthen contract for log_axiom_instantiation #5621

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Oct 26, 2021 · bdecc25 · bdecc25
1 parent efcad5f
commit bdecc25
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 5 deletions.
diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp
@@ -208,10 +208,11 @@ namespace smt {
     }
 
     void theory::log_axiom_instantiation(app * r, unsigned axiom_id, unsigned num_bindings, app * const * bindings, unsigned pattern_id, const vector<std::tuple<enode *, enode *>> & used_enodes) {
-        ast_manager & m = get_manager();
-        app_ref _r(r, m);
+        ast_manager & m = get_manager();   
+        SASSERT(r->get_ref_count() > 0);
         std::ostream& out = m.trace_stream();
         symbol const & family_name = m.get_family_name(get_family_id());
+
         if (pattern_id == UINT_MAX) {
             out << "[inst-discovered] theory-solving " << static_cast<void *>(nullptr) << " " << family_name << "#";
             if (axiom_id != UINT_MAX)
@@ -235,8 +236,8 @@ namespace smt {
                 enode *orig = std::get<0>(n);
                 enode *substituted = std::get<1>(n);
                 if (orig != nullptr) {
-                    quantifier_manager::log_justification_to_root(out, orig, already_visited, ctx, get_manager());
-                    quantifier_manager::log_justification_to_root(out, substituted, already_visited, ctx, get_manager());
+//                    quantifier_manager::log_justification_to_root(out, orig, already_visited, ctx, get_manager());
+//                    quantifier_manager::log_justification_to_root(out, substituted, already_visited, ctx, get_manager());
                 }
             }
             out << "[new-match] " << static_cast<void *>(nullptr) << " " << family_name << "#" << axiom_id << " " << family_name << "#" << pattern_id;

diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
@@ -215,11 +215,12 @@ namespace smt {
     }
 
     void theory_fpa::assert_cnstr(expr * e) {
+        expr_ref _e(e, m);
         if (m.is_true(e)) return;
         TRACE("t_fpa_detail", tout << "asserting " << mk_ismt2_pp(e, m) << "\n";);
         if (m.has_trace_stream()) log_axiom_instantiation(e);
         ctx.internalize(e, false);
-        if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+        if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";        
         literal lit(ctx.get_literal(e));
         ctx.mark_as_relevant(lit);
         ctx.mk_th_axiom(get_id(), 1, &lit);