From ef6b5f82d16642f6cf1378876614b43e685ffcd6 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 20 Mar 2024 13:39:16 +0100
Subject: [PATCH] relax level constraint

---
 src/sat/smt/polysat/project_interval.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/sat/smt/polysat/project_interval.cpp b/src/sat/smt/polysat/project_interval.cpp
index 3e72a2a1f..fe3f5a3fb 100644
--- a/src/sat/smt/polysat/project_interval.cpp
+++ b/src/sat/smt/polysat/project_interval.cpp
@@ -257,7 +257,7 @@ namespace polysat {
             for (unsigned i = 0; i < m_fixed.size(); ++i) {
                 auto const& f = m_fixed[i];
                 unsigned const f_level = m_fixed_levels[i];
-                if (f_level >= w_level)
+                if (f_level > w_level)
                     continue;
                 // ??????xxxxxxxyyyyyyzzzz
                 //  1111            not useful at this point
@@ -330,7 +330,7 @@ namespace polysat {
             for (unsigned i = 0; i < m_fixed.size(); ++i) {
                 auto const& f = m_fixed[i];
                 unsigned const f_level = m_fixed_levels[i];
-                if (f_level >= w_level)
+                if (f_level > w_level)
                     continue;
                 // ?????????????yyyyyyzzzzz???
                 //            1111              not useful at this point