From 61d887b36ff31c758e46c5d8cc691388bbd4993e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Jul 2018 04:35:22 -0700 Subject: [PATCH] use for pattern Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index d49d0de6a..9f73023e4 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1176,7 +1176,7 @@ public: if (m_solver->is_term(wi)) { const lp::lar_term& term = m_solver->get_term(wi); result += term.m_v * coeff; - for (const auto & i: term.m_coeffs) { + for (const auto & i : term.m_coeffs) { m_todo_terms.push_back(std::make_pair(i.first, coeff * i.second)); } } @@ -2088,8 +2088,8 @@ public: vi = m_todo_vars.back(); m_todo_vars.pop_back(); lp::lar_term const& term = m_solver->get_term(vi); - for (auto i = term.m_coeffs.begin(); i != term.m_coeffs.end(); ++i) { - lp::var_index wi = i->first; + for (auto const& coeff : term.m_coeffs) { + lp::var_index wi = coeff.first; if (m_solver->is_term(wi)) { m_todo_vars.push_back(wi); } @@ -2113,8 +2113,8 @@ public: vi = m_todo_vars.back(); m_todo_vars.pop_back(); lp::lar_term const& term = m_solver->get_term(vi); - for (auto i = term.m_coeffs.begin(); i != term.m_coeffs.end(); ++i) { - lp::var_index wi = i->first; + for (auto const& coeff : term.m_coeffs) { + lp::var_index wi = coeff.first; if (m_solver->is_term(wi)) { m_todo_vars.push_back(wi); } @@ -2204,7 +2204,7 @@ public: lp::var_index vi = m_theory_var2var_index[v]; SASSERT(m_solver->is_term(vi)); lp::lar_term const& term = m_solver->get_term(vi); - for (auto const coeff : term.m_coeffs) { + for (auto const & coeff : term.m_coeffs) { lp::var_index wi = coeff.first; lp::constraint_index ci; rational value;