mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

disable assertion for now

Browse source
This commit is contained in:
Jakob Rath 2022-11-28 18:15:24 +01:00
parent a3767b177c
commit c1f9a26f09
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/viable.cpp
View file

@ -205,7 +205,7 @@ namespace polysat {
}
bool viable::intersect(pvar v, entry* ne) {
SASSERT(!s.is_assigned(v));
// SASSERT(!s.is_assigned(v)); // TODO: do we get unsoundness if this condition is violated? (see comment on cyclic dependencies in solver::pop_levels)
entry* e = m_units[v];
if (e && e->interval.is_full()) {
m_alloc.push_back(ne);