mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix build breaks

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-20 20:36:26 -08:00
parent a3f7541719
commit 3cdcd831b1
1 changed files with 7 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/ast/sls/sls_arith_base.cpp
View file

@ -110,8 +110,8 @@ namespace sls {
template<typename num_t> template<typename num_t>
arith_base<num_t>::arith_base(context& ctx) : arith_base<num_t>::arith_base(context& ctx) :
plugin(ctx), plugin(ctx),
a(m),
m_new_terms(m), m_new_terms(m),
a(m),
m_clausal_sls(*this) { m_clausal_sls(*this) {
m_fid = a.get_family_id(); m_fid = a.get_family_id();
} }
@ -1421,12 +1421,16 @@ namespace sls {
auto& ui = m_vars[u]; auto& ui = m_vars[u];
for (auto const& idx : ui.m_muls) { for (auto const& idx : ui.m_muls) {
auto& [x, monomial] = m_muls[idx]; auto& [x, monomial] = m_muls[idx];
if (all_of(todo, [x](var_t v) { return x != v; })) bool found = false;
for (auto u : todo) found |= u == x;
if (!found)
todo.push_back(x); todo.push_back(x);
} }
for (auto const& idx : ui.m_adds) { for (auto const& idx : ui.m_adds) {
auto x = m_adds[idx].m_var; auto x = m_adds[idx].m_var;
if (all_of(todo, [x](var_t v) { return x != v; })) bool found = false;
for (auto u : todo) found |= u == x;
if (!found)
todo.push_back(x); todo.push_back(x);
} }
for (auto const& [coeff, bv] : ui.m_linear_occurs) for (auto const& [coeff, bv] : ui.m_linear_occurs)