diff --git a/src/math/polysat/viable2.cpp b/src/math/polysat/viable2.cpp index 67d7b853b..f6d625671 100644 --- a/src/math/polysat/viable2.cpp +++ b/src/math/polysat/viable2.cpp @@ -72,6 +72,11 @@ namespace polysat { if (e && e->interval.is_full()) return; + if (ne->interval.is_currently_empty()) { + m_alloc.push_back(ne); + return; + } + auto create_entry = [&]() { m_trail.push_back({ v, ne }); s.m_trail.push_back(trail_instr_t::viable_add_i);