mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

fix crash when api_solver sets reset_tracked_assertions

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-11-19 12:48:33 -08:00
parent ac105b7d8c
commit d272acc3ac
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/cmd_context/cmd_context.cpp
View file

@ -1678,6 +1678,8 @@ void cmd_context::restore_assertions(unsigned old_sz) {
SASSERT(m_assertions.empty()); SASSERT(m_assertions.empty());
return; return;
} }
if (m_assertions.empty())
return;
if (old_sz == m_assertions.size()) if (old_sz == m_assertions.size())
return; return;
SASSERT(old_sz < m_assertions.size()); SASSERT(old_sz < m_assertions.size());
@ -2296,6 +2298,8 @@ vector<std::pair<expr*,expr*>> cmd_context::tracked_assertions() {
} }
void cmd_context::reset_tracked_assertions() { void cmd_context::reset_tracked_assertions() {
for (expr* a : m_assertion_names)
m().dec_ref(a);
m_assertion_names.reset(); m_assertion_names.reset();
for (expr* a : m_assertions) for (expr* a : m_assertions)
m().dec_ref(a); m().dec_ref(a);