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 memory smash in euf completion

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-05 13:04:49 -07:00
parent 14f69c6c01
commit f4b87b3763
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/simplifiers/euf_completion.cpp
View file

@ -307,7 +307,7 @@ namespace euf {
} }
}; };
SASSERT(e); SASSERT(e);
if (num_scopes() > 0) if (num_scopes() > 0 && m_canonical.size() > n->get_id())
m_trail.push(vtrail(m_canonical, n->get_id())); m_trail.push(vtrail(m_canonical, n->get_id()));
m_canonical.setx(n->get_id(), e); m_canonical.setx(n->get_id(), e);
m_epochs.setx(n->get_id(), m_epoch, 0); m_epochs.setx(n->get_id(), m_epoch, 0);