mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 13:53:39 +00:00
Code Activity

fixing smt code ending up in log files (verbose logging)

Browse source
This commit is contained in:
nilsbecker 2018-04-29 13:08:57 +02:00
parent 4d4497674f
commit 7a03f19456
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_context_pp.cpp
View file

@ -580,20 +580,20 @@ namespace smt {
case b_justification::BIN_CLAUSE: { case b_justification::BIN_CLAUSE: {
literal l2 = j.get_literal(); literal l2 = j.get_literal();
out << "bin-clause "; out << "bin-clause ";
display_literal_verbose(out, l2); display_literal(out, l2);
break; break;
} }
case b_justification::CLAUSE: { case b_justification::CLAUSE: {
clause * cls = j.get_clause(); clause * cls = j.get_clause();
out << "clause "; out << "clause ";
if (cls) display_literals_verbose(out, cls->get_num_literals(), cls->begin_literals()); if (cls) display_literals(out, cls->get_num_literals(), cls->begin_literals());
break; break;
} }
case b_justification::JUSTIFICATION: { case b_justification::JUSTIFICATION: {
out << "justification " << j.get_justification()->get_from_theory() << ": "; out << "justification " << j.get_justification()->get_from_theory() << ": ";
literal_vector lits; literal_vector lits;
const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits); const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
display_literals_verbose(out, lits); display_literals(out, lits);
break; break;
} }
default: default: