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

fix #5236

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-05-05 13:50:53 -07:00
parent 85bd4b5242
commit 2b1b10be69
1 changed files with 7 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/mam.cpp
View file

@ -1843,7 +1843,7 @@ namespace {
enode_vector m_bindings; enode_vector m_bindings;
enode_vector m_args; enode_vector m_args;
backtrack_stack m_backtrack_stack; backtrack_stack m_backtrack_stack;
unsigned m_top; unsigned m_top { 0 };
const instruction * m_pc; const instruction * m_pc;
// auxiliary temporary variables // auxiliary temporary variables
@ -2210,8 +2210,13 @@ namespace {
if (curr->get_num_args() == expected_num_args && m_context.is_relevant(curr)) if (curr->get_num_args() == expected_num_args && m_context.is_relevant(curr))
break; break;
} }
if (bp.m_it == bp.m_end) if (bp.m_it == bp.m_end) {
if (best_v) {
bp.m_to_recycle = nullptr;
recycle_enode_vector(best_v);
}
return nullptr; return nullptr;
}
m_top++; m_top++;
update_max_generation(*(bp.m_it), nullptr); update_max_generation(*(bp.m_it), nullptr);
return *(bp.m_it); return *(bp.m_it);