From aa5b4b8c77a1d273d297336e21a43c8e2dd6bc0d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Oct 2021 09:49:38 +0200 Subject: [PATCH] strengthen contract for log_axiom_instantiation #5621 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_theory.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp index 69eecffd6b7..0c876e8bc26 100644 --- a/src/smt/smt_theory.cpp +++ b/src/smt/smt_theory.cpp @@ -236,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(nullptr) << " " << family_name << "#" << axiom_id << " " << family_name << "#" << pattern_id;