From 3cdcd831b1d4abad6cfba3a920590e29792569c9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 20 Jan 2025 20:36:26 -0800 Subject: [PATCH] fix build breaks --- src/ast/sls/sls_arith_base.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp index 8ad22e40e..44c935330 100644 --- a/src/ast/sls/sls_arith_base.cpp +++ b/src/ast/sls/sls_arith_base.cpp @@ -110,8 +110,8 @@ namespace sls { template arith_base::arith_base(context& ctx) : plugin(ctx), - a(m), m_new_terms(m), + a(m), m_clausal_sls(*this) { m_fid = a.get_family_id(); } @@ -1421,12 +1421,16 @@ namespace sls { auto& ui = m_vars[u]; for (auto const& idx : ui.m_muls) { 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); } for (auto const& idx : ui.m_adds) { 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); } for (auto const& [coeff, bv] : ui.m_linear_occurs)