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

fix assertion failure when printing stats

Browse source 
It would crash when number of bin_lemmas == 0
This commit is contained in:
Nuno Lopes 2024-05-18 16:30:26 +01:00
parent cb50dcabda
commit 18a95d89c6
1 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/smt/smt_context_pp.cpp
View file

@ -712,14 +712,14 @@ namespace smt {
}; };
std::stringstream strm; std::stringstream strm;
strm << "(smt.stats " strm << "(smt.stats "
<< std::setw(4) << m_stats.m_num_restarts << " " << std::setw(4) << m_stats.m_num_restarts << ' '
<< std::setw(6) << m_stats.m_num_conflicts << " " << std::setw(6) << m_stats.m_num_conflicts << ' '
<< std::setw(6) << m_stats.m_num_decisions << " " << std::setw(6) << m_stats.m_num_decisions << ' '
<< std::setw(6) << m_stats.m_num_propagations << " " << std::setw(6) << m_stats.m_num_propagations << ' '
<< std::setw(5) << (m_aux_clauses.size() + bin_clauses) << "/" << bin_clauses << "/" << num_units() << std::setw(5) << (m_aux_clauses.size() + bin_clauses) << '/' << bin_clauses << '/' << num_units() << ' '
<< std::setw(7) << m_lemmas.size(); if (bin_lemmas > 0) strm << "/" << bin_lemmas << " "; << std::setw(7) << m_lemmas.size() << '/' << bin_lemmas << ' '
strm << std::setw(5) << m_stats.m_num_simplifications << " " << std::setw(5) << m_stats.m_num_simplifications << ' '
<< std::setw(4) << m_stats.m_num_del_clauses << " " << std::setw(4) << m_stats.m_num_del_clauses << ' '
<< std::setw(7) << mem_stat() << ")\n"; << std::setw(7) << mem_stat() << ")\n";
std::string str = std::move(strm).str(); std::string str = std::move(strm).str();
@ -745,7 +745,7 @@ namespace smt {
m_last_position_log = m_stats.m_num_restarts; m_last_position_log = m_stats.m_num_restarts;
// restarts decisions clauses simplifications memory // restarts decisions clauses simplifications memory
// conflicts propagations lemmas deletions // conflicts propagations lemmas deletions
int adjust[9] = { -3, -3, -3, -3, -3, -4, -4, -4, -1 }; const int adjust[9] = { -3, -3, -3, -3, -3, -4, -4, -4, -1 };
char const* tag[9] = { ":restarts ", ":conflicts ", ":decisions ", ":propagations ", ":clauses/bin/units ", ":lemmas ", ":simplify ", ":deletions", ":memory" }; char const* tag[9] = { ":restarts ", ":conflicts ", ":decisions ", ":propagations ", ":clauses/bin/units ", ":lemmas ", ":simplify ", ":deletions", ":memory" };
std::stringstream l1, l2; std::stringstream l1, l2;