From 21c604e7b4ebebdd4a4500280926ea8c82551f48 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Nov 2021 18:56:32 +0100 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/math/polysat/conflict.cpp | 4 ++-- src/math/polysat/solver.cpp | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 081c5767d..4d31cb8b3 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -294,8 +294,8 @@ namespace polysat { return false; } - if (conflict_var() == v && s.m_viable.resolve(v, *this)) - return true; + // forbidden interval projection is performed at top level + SASSERT(v != conflict_var()); m_vars.remove(v); diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 1d09a600c..0405bc801 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -473,7 +473,7 @@ namespace polysat { if (m_conflict.conflict_var() != null_var) { // This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack. - resolve_value(m_conflict.conflict_var()); + VERIFY(m_viable.resolve(m_conflict.conflict_var(), m_conflict)); } search_iterator search_it(m_search);