mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 12:58:44 +00:00
Code Activity

strengthen contract for log_axiom_instantiation #5621

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-10-26 09:49:38 +02:00
parent bdecc25619
commit aa5b4b8c77
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_theory.cpp
View file

@ -236,8 +236,8 @@ namespace smt {
enode *orig = std::get<0>(n); enode *orig = std::get<0>(n);
enode *substituted = std::get<1>(n); enode *substituted = std::get<1>(n);
if (orig != nullptr) { if (orig != nullptr) {
// quantifier_manager::log_justification_to_root(out, orig, 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()); 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; out << "[new-match] " << static_cast<void *>(nullptr) << " " << family_name << "#" << axiom_id << " " << family_name << "#" << pattern_id;