From 79d77bc6902b0e76d49a9d44db89211d5a4b6800 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 29 Nov 2023 13:35:49 +0100 Subject: [PATCH] exit conditions --- src/math/polysat/viable.cpp | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 4999eabc7..9fe444301 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -1744,9 +1744,18 @@ namespace polysat { return l_true; // done SASSERT(result == l_undef); - // TODO: continue with intervals at current level + + if (progress >= mod_value) { + // covered the whole domain => conflict + return l_false; + } + + if (progress >= to_cover_len) { + // we covered the hole left at larger bit-width + return l_undef; + } } - NOT_IMPLEMENTED_YET(); + UNREACHABLE(); return l_undef; }