diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h index 973cadb4b..c52477a4c 100644 --- a/src/math/interval/dep_intervals.h +++ b/src/math/interval/dep_intervals.h @@ -209,8 +209,7 @@ public: } template - interval power(const interval& a, unsigned n) { - interval b; + void power(const interval& a, unsigned n, interval& b) { if (with_deps == wd) { interval_deps_combine_rule combine_rule; m_imanager.power(a, n, b, combine_rule); @@ -221,7 +220,6 @@ public: } TRACE("dep_intervals", tout << "power of "; display(tout, a) << " = "; display(tout, b) << "\n"; ); - return b; } template diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index f4abb3ea8..4d131b798 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -446,7 +446,8 @@ bool intervals::interval_of_mul(const nex_mul& e, scoped_dep_interval& a, const template void intervals::to_power(scoped_dep_interval& a, unsigned p) { if (p == 1) return; - interval b = m_dep_intervals.power(a, p); + scoped_dep_interval b(m_dep_intervals); + m_dep_intervals.power(a, p, b); m_dep_intervals.set(a, b); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index ce6c512ae..944e5a9aa 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1970,8 +1970,9 @@ bool theory_seq::check_length_coherence() { } bool theory_seq::fixed_length(bool is_zero) { - bool found = false; - for (auto e : m_length) { + bool found = false; + for (unsigned i = 0; i < m_length.size(); ++i) { + expr* e = m_length.get(i); if (fixed_length(e, is_zero)) { found = true; }