mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 18:36:41 +00:00
Code Activity

relax level constraint

Browse source
This commit is contained in:
Jakob Rath 2024-03-20 13:39:16 +01:00
parent 91a9feb5a8
commit ef6b5f82d1
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/polysat/project_interval.cpp
View file

@ -257,7 +257,7 @@ namespace polysat {
for (unsigned i = 0; i < m_fixed.size(); ++i) { for (unsigned i = 0; i < m_fixed.size(); ++i) {
auto const& f = m_fixed[i]; auto const& f = m_fixed[i];
unsigned const f_level = m_fixed_levels[i]; unsigned const f_level = m_fixed_levels[i];
if (f_level >= w_level) if (f_level > w_level)
continue; continue;
// ??????xxxxxxxyyyyyyzzzz // ??????xxxxxxxyyyyyyzzzz
// 1111 not useful at this point // 1111 not useful at this point
@ -330,7 +330,7 @@ namespace polysat {
for (unsigned i = 0; i < m_fixed.size(); ++i) { for (unsigned i = 0; i < m_fixed.size(); ++i) {
auto const& f = m_fixed[i]; auto const& f = m_fixed[i];
unsigned const f_level = m_fixed_levels[i]; unsigned const f_level = m_fixed_levels[i];
if (f_level >= w_level) if (f_level > w_level)
continue; continue;
// ?????????????yyyyyyzzzzz??? // ?????????????yyyyyyzzzzz???
// 1111 not useful at this point // 1111 not useful at this point