strengthen contract for log_axiom_instantiation #5621

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Oct 26, 2021 · aa5b4b8 · aa5b4b8
1 parent bdecc25
commit aa5b4b8
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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<void *>(nullptr) << " " << family_name << "#" << axiom_id << " " << family_name << "#" << pattern_id;