From a5fdf6ba8a344db456b8dd4d52f50ff5caefb2df Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 16 Nov 2021 09:54:06 -0800 Subject: [PATCH] Update viable2.cpp --- src/math/polysat/viable2.cpp | 5 +++++ 1 file changed, 5 insertions(+) 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);