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 #6488

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-12 11:04:46 -08:00
parent a3e6885680
commit 4598af70c8
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -199,6 +199,8 @@ void elim_unconstrained::freeze(expr* t) {
return; return;
if (m_nodes.size() <= t->get_id()) if (m_nodes.size() <= t->get_id())
return; return;
if (m_nodes.size() <= root(t))
return;
node& n = get_node(t); node& n = get_node(t);
if (!n.m_term) if (!n.m_term)
return; return;