From c954e82503f3b534f2536d38bd1afd8e25a93da0 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 16 Jan 2023 16:51:16 +0100 Subject: [PATCH] assertion should hold now after recent fix --- src/math/polysat/viable.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 863d1e002..a2b576507 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -237,7 +237,7 @@ namespace polysat { } bool viable::intersect(pvar v, entry* ne) { - // SASSERT(!s.is_assigned(v)); // TODO: do we get unsoundness if this condition is violated? (see comment on cyclic dependencies in solver::pop_levels) + SASSERT(!s.is_assigned(v)); entry* e = m_units[v]; if (e && e->interval.is_full()) { m_alloc.push_back(ne);