mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-26 22:17:54 +00:00
Code Activity

fix crash on EBxzQox7raUO.smt2

Browse source
This commit is contained in:
Jakob Rath 2024-03-25 13:20:24 +01:00
parent ac6554eb92
commit 8a23523f20
1 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/sat/smt/polysat/project_interval.cpp
View file

@ -131,6 +131,12 @@ namespace polysat {
break; break;
if (m_fixed[i].length != m_fixed[j].length) if (m_fixed[i].length != m_fixed[j].length)
break; break;
if (m_fixed[i].value != m_fixed[j].value) {
// same subslice, but with different values;
// this should not happen in a fully saturated egraph (wrt. bv_plugin).
break;
}
VERIFY(m_fixed[j].child != null_var);
SASSERT(m_fixed[i].value == m_fixed[j].value); SASSERT(m_fixed[i].value == m_fixed[j].value);
i = j; i = j;