mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 00:48:45 +00:00
Code Activity

fix infinite loop in internalize

Browse source
This commit is contained in:
Nuno Lopes 2022-09-14 11:50:53 +01:00
parent 34969b71ee
commit 16ef89905d
2 changed files with 18 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_stats.cpp
View file

@ -28,7 +28,7 @@ extern "C" {
RESET_ERROR_CODE(); RESET_ERROR_CODE();
std::ostringstream buffer; std::ostringstream buffer;
to_stats_ref(s).display_smt2(buffer); to_stats_ref(s).display_smt2(buffer);
std::string result = buffer.str(); std::string result = std::move(buffer).str();
// Hack for removing the trailing '\n' // Hack for removing the trailing '\n'
SASSERT(result.size() > 0); SASSERT(result.size() > 0);
result.resize(result.size()-1); result.resize(result.size()-1);

13
src/smt/smt_context.cpp
View file

@ -3207,8 +3207,12 @@ namespace smt {
reduce_assertions(); reduce_assertions();
if (get_cancel_flag()) if (get_cancel_flag())
return; return;
if (m_asserted_formulas.inconsistent()) {
if (!inconsistent())
asserted_inconsistent();
break;
}
qhead = m_asserted_formulas.get_qhead(); qhead = m_asserted_formulas.get_qhead();
if (!m_asserted_formulas.inconsistent()) {
unsigned sz = m_asserted_formulas.get_num_formulas(); unsigned sz = m_asserted_formulas.get_num_formulas();
while (qhead < sz) { while (qhead < sz) {
if (get_cancel_flag()) { if (get_cancel_flag()) {
@ -3219,15 +3223,10 @@ namespace smt {
proof * pr = m_asserted_formulas.get_formula_proof(qhead); proof * pr = m_asserted_formulas.get_formula_proof(qhead);
SASSERT(!pr || f == m.get_fact(pr)); SASSERT(!pr || f == m.get_fact(pr));
internalize_assertion(f, pr, 0); internalize_assertion(f, pr, 0);
qhead++; ++qhead;
} }
m_asserted_formulas.commit(); m_asserted_formulas.commit();
} }
if (m_asserted_formulas.inconsistent() && !inconsistent()) {
asserted_inconsistent();
break;
}
}
while (qhead < m_asserted_formulas.get_num_formulas()); while (qhead < m_asserted_formulas.get_num_formulas());
TRACE("internalize_assertions", tout << "after internalize_assertions()...\n"; TRACE("internalize_assertions", tout << "after internalize_assertions()...\n";