From d65dc82ef05562735cbdb4133027dbe299502e82 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 25 Jul 2022 13:49:21 +0200 Subject: [PATCH] bailout state: add premises of assignment --- src/math/polysat/conflict.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 5b6719450..9adf8a944 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -499,9 +499,6 @@ namespace polysat { s.inc_activity(v); m_vars.remove(v); - - if (is_bailout()) - goto bailout; if (j.is_propagation()) { for (auto const& c : s.m_viable.get_constraints(v)) @@ -512,6 +509,9 @@ namespace polysat { } } + if (is_bailout()) + goto bailout; + LOG("try-explain v" << v); if (try_explain(v)) return true;