From 3302ab9dc5a12f4d1e6ec68d842a4251aa5853a2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Apr 2023 16:12:11 -0700 Subject: [PATCH] fix bug introduced in is_valid() --- src/math/polysat/conflict.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 410ff5f5a..dea317bea 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -211,7 +211,7 @@ namespace polysat { bool conflict::is_valid() const { SASSERT(!empty()); // If m_dep is set, the corresponding constraint was asserted at m_level and is not valid earlier. - if (!m_dep.is_null() && m_level >= s.m_level) + if (!m_dep.is_null() && m_level > s.m_level) return false; // All conflict constraints must be bool-assigned. for (unsigned lit_idx : m_literals)