diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 74c759510..73d822fb4 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -613,7 +613,7 @@ namespace smt { out << "justification "; literal_vector lits; const_cast(*m_conflict_resolution).justification2literals(j.get_justification(), lits); - display_literals_verbose(out, lits.size(), lits.c_ptr()); + display_literals(out, lits.size(), lits.c_ptr()); break; } default: