diff --git a/src/math/lp/hnf_cutter.cpp b/src/math/lp/hnf_cutter.cpp
index 7f1de7f5d..70a9222e4 100644
--- a/src/math/lp/hnf_cutter.cpp
+++ b/src/math/lp/hnf_cutter.cpp
@@ -49,7 +49,7 @@ namespace lp  {
         
         m_constraints_for_explanation.push_back(ci);
        
-        for (const auto &p : *t) {
+        for (lar_term::ival p : *t) {
             m_var_register.add_var(p.column().index(), true); // hnf only deals with integral variables for now
             mpq t = abs(ceil(p.coeff()));
             if (t > m_abs_max)
diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index 940cf6750..b2ee676de 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -189,7 +189,7 @@ std::ostream& int_solver::display_inf_rows(std::ostream& out) const {
 }
 
 bool int_solver::cut_indices_are_columns() const {
-    for (const auto & p: m_t) {
+    for (lar_term::ival p : m_t) {
         if (p.column().index() >= lra.A_r().column_count())
             return false;
     }
@@ -347,7 +347,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
     lp_assert(settings().use_tableau());
     const auto & A = lra.A_r();
     unsigned rounds = 0;
-    for (const auto &c : A.column(j)) {
+    for (auto c : A.column(j)) {
         row_index = c.var();
         const mpq & a = c.coeff();        
         unsigned i = lrac.m_r_basis[row_index];
@@ -357,7 +357,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
     }
     TRACE("random_update", tout <<  "m = " << m << "\n";);
     
-    for (const auto &c : A.column(j)) {
+    for (auto c : A.column(j)) {
         if (!inf_l && !inf_u && l >= u) break;       
         row_index = c.var();
         const mpq & a = c.coeff();        
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 354a30099..e01ba746a 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -55,7 +55,7 @@ bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const
 
 rational core::value(const lp::lar_term& r) const {
     rational ret(0);
-    for (const auto & t : r) {
+    for (lp::lar_term::ival t : r) {
         ret += t.coeff() * val(t.column());
     }
     return ret;
@@ -63,7 +63,7 @@ rational core::value(const lp::lar_term& r) const {
 
 lp::lar_term core::subs_terms_to_columns(const lp::lar_term& t) const {
     lp::lar_term r;
-    for (const auto& p : t) {
+    for (lp::lar_term::ival p : t) {
         lpvar j = p.column();
         if (lp::tv::is_term(j))
             j = m_lar_solver.map_term_index_to_column_index(j);
@@ -288,7 +288,7 @@ bool core::explain_upper_bound(const lp::lar_term& t, const rational& rs, lp::ex
 }
 bool core::explain_lower_bound(const lp::lar_term& t, const rational& rs, lp::explanation& e) const {
     rational b(0); // the bound
-    for (const auto& p : t) {
+    for (lp::lar_term::ival p : t) {
         rational pb;
         if (explain_coeff_lower_bound(p, pb, e)) {
             b += pb;
@@ -587,7 +587,7 @@ std::ostream & core::print_ineqs(const lemma& l, std::ostream & out) const {
             auto & in = l.ineqs()[i]; 
             print_ineq(in, out);
             if (i + 1 < l.ineqs().size()) out << " or ";
-            for (const auto & p: in.term())
+            for (lp::lar_term::ival p: in.term())
                 vars.insert(p.column());
         }
         out << std::endl;
@@ -708,7 +708,7 @@ bool core::is_octagon_term(const lp::lar_term& t, bool & sign, lpvar& i, lpvar &
     bool seen_minus = false;
     bool seen_plus = false;
     i = null_lpvar;
-    for(const auto & p : t) {
+    for(lp::lar_term::ival p : t) {
         const auto & c = p.coeff();
         if (c == 1) {
             seen_plus = true;
@@ -851,11 +851,11 @@ std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
     };
     
     for (const auto& i : l.ineqs()) {
-        for (const auto& p : i.term()) {                
+        for (lp::lar_term::ival p : i.term()) {                
             insert_j(p.column());
         }
     }
-    for (const auto& p : l.expl()) {
+    for (auto p : l.expl()) {
         const auto& c = m_lar_solver.constraints()[p.ci()];
         for (const auto& r : c.coeffs()) {
             insert_j(r.second);
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index 2fd880679..79a7fc060 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -204,7 +204,7 @@ struct solver::imp {
         // variable representing the term.
         svector<polynomial::var> vars;
         rational den(1);
-        for (const auto& kv : t) {
+        for (lp::lar_term::ival kv : t) {
             vars.push_back(lp2nl(kv.column().index()));
             den = lcm(den, denominator(kv.coeff()));
         }
diff --git a/src/math/lp/square_sparse_matrix_def.h b/src/math/lp/square_sparse_matrix_def.h
index df7f606fe..0a2cffd61 100644
--- a/src/math/lp/square_sparse_matrix_def.h
+++ b/src/math/lp/square_sparse_matrix_def.h
@@ -27,7 +27,7 @@ template <typename T, typename X>
 template <typename M>
 void square_sparse_matrix<T, X>::copy_column_from_input(unsigned input_column, const M& A, unsigned j) {
     vector<indexed_value<T>> & new_column_vector = m_columns[j].m_values;
-    for (const auto & c : A.column(input_column)) {
+    for (auto c : A.column(input_column)) {
         unsigned col_offset = static_cast<unsigned>(new_column_vector.size());
         vector<indexed_value<T>> & row_vector = m_rows[c.var()];
         unsigned row_offset = static_cast<unsigned>(row_vector.size());
@@ -41,7 +41,7 @@ template <typename T, typename X>
 template <typename M>
 void square_sparse_matrix<T, X>::copy_column_from_input_with_possible_zeros(const M& A, unsigned j) {
     vector<indexed_value<T>> & new_column_vector = m_columns[j].m_values;
-    for (const auto & c : A.column(j)) {
+    for (auto c : A.column(j)) {
         if (is_zero(c.coeff()))
             continue;
         unsigned col_offset = static_cast<unsigned>(new_column_vector.size());
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 2115eb9d3..820dd7e4e 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -316,7 +316,7 @@ namespace arith {
         if (e1->get_sort() != e2->get_sort())
             return;
         reset_evidence();
-        for (auto const& ev : e)
+        for (auto ev : e)
             set_evidence(ev.ci(), m_core, m_eqs);
         auto* jst = euf::th_explain::propagate(*this, m_core, m_eqs, n1, n2);
         ctx.propagate(n1, n2, jst->to_index());
@@ -1035,7 +1035,7 @@ namespace arith {
                 rational c1(0);
                 m_nla->am().set(r1, c1.to_mpq());
                 m_nla->am().add(r, r1, r);
-                for (auto const& arg : term) {
+                for (lp::lar_term::ival arg : term) {
                     auto wi = lp().column2tv(arg.column());
                     c1 = arg.coeff() * wcoeff;
                     if (wi.is_term()) {
@@ -1108,7 +1108,7 @@ namespace arith {
             ++m_stats.m_gomory_cuts;
             // m_explanation implies term <= k
             reset_evidence();
-            for (auto const& ev : m_explanation)
+            for (auto ev : m_explanation)
                 set_evidence(ev.ci(), m_core, m_eqs);
             // The call mk_bound() can set the m_infeasible_column in lar_solver
             // so the explanation is safer to take before this call.
@@ -1168,7 +1168,7 @@ namespace arith {
 
         ++m_num_conflicts;
         ++m_stats.m_conflicts;
-        for (auto const& ev : m_explanation)
+        for (auto ev : m_explanation)
             set_evidence(ev.ci(), m_core, m_eqs);
         TRACE("arith",
             tout << "Lemma - " << (is_conflict ? "conflict" : "propagation") << "\n";
@@ -1305,7 +1305,7 @@ namespace arith {
 
     void solver::term2coeffs(lp::lar_term const& term, u_map<rational>& coeffs, rational const& coeff) {
         TRACE("arith", lp().print_term(term, tout) << "\n";);
-        for (const auto& ti : term) {
+        for (lp::lar_term::ival ti : term) {
             theory_var w;
             auto tv = lp().column2tv(ti.column());
             if (tv.is_term()) {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index e5d75b260..c045c98f4 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1861,7 +1861,7 @@ public:
     void dump_cut_lemma(std::ostream& out, lp::lar_term const& term, lp::mpq const& k, lp::explanation const& ex, bool upper) {
         lp().print_term(term, out << "bound: "); 
         out << (upper?" <= ":" >= ") << k << "\n";
-        for (auto const& p : term) {
+        for (lp::lar_term::ival p : term) {
             auto ti = lp().column2tv(p.column());
             out << p.coeff() << " * ";
             if (ti.is_term()) {
@@ -1871,11 +1871,11 @@ public:
                 out << "v" << lp().local_to_external(ti.id()) << "\n";
             }
         }
-        for (auto const& ev : ex) {
+        for (auto ev : ex) {
             lp().constraints().display(out << ev.coeff() << ": ", ev.ci());
         }
         expr_ref_vector fmls(m);
-        for (auto const& ev : ex) {
+        for (auto ev : ex) {
             fmls.push_back(constraint2fml(ev.ci()));
         }        
         expr_ref t(term2expr(term), m);
@@ -1936,7 +1936,7 @@ public:
             ++m_stats.m_gomory_cuts;
             // m_explanation implies term <= k
             reset_evidence();
-            for (auto const& ev : m_explanation) {
+            for (auto ev : m_explanation) {
                 set_evidence(ev.ci(), m_core, m_eqs);
             }
             // The call mk_bound() can set the m_infeasible_column in lar_solver
@@ -2304,7 +2304,7 @@ public:
         if (m.is_ite(e1) || m.is_ite(e2))
             return;
         reset_evidence();
-        for (auto const& ev : e) 
+        for (auto ev : e) 
             set_evidence(ev.ci(), m_core, m_eqs);
         justification* js = ctx().mk_justification(
             ext_theory_eq_propagation_justification(
@@ -2709,7 +2709,7 @@ public:
             SASSERT(ti.is_term());
             m_todo_vars.pop_back();
             lp::lar_term const& term = lp().get_term(ti);
-            for (auto const& p : term) {
+            for (auto p : term) {
                 lp::tv wi = lp().column2tv(p.column());
                 if (wi.is_term()) {
                     m_todo_vars.push_back(wi);
@@ -2735,7 +2735,7 @@ public:
             SASSERT(ti.is_term());
             m_todo_vars.pop_back();
             lp::lar_term const& term = lp().get_term(ti);
-            for (auto const& coeff : term) {
+            for (auto coeff : term) {
                 auto wi = lp().column2tv(coeff.column());
                 if (wi.is_term()) {
                     m_todo_vars.push_back(wi);
@@ -3174,7 +3174,7 @@ public:
         ++m_stats.m_conflicts;
         TRACE("arith", tout << "scope: " << ctx().get_scope_level() << "\n"; display_evidence(tout, m_explanation); );
         TRACE("arith", display(tout << "is-conflict: " << is_conflict << "\n"););
-        for (auto const& ev : m_explanation) {
+        for (auto ev : m_explanation) {
             set_evidence(ev.ci(), m_core, m_eqs);
         }
         // SASSERT(validate_conflict(m_core, m_eqs));
diff --git a/src/util/container_util.h b/src/util/container_util.h
index 4c76850b8..fe70e9fd3 100644
--- a/src/util/container_util.h
+++ b/src/util/container_util.h
@@ -30,7 +30,7 @@ Revision History:
 template<class Set1, class Set2>
 void set_intersection(Set1 & tgt, const Set2 & src) {
     svector<typename Set1::data> to_remove;
-    for (typename Set1::data const& itm : tgt) 
+    for (auto itm : tgt) 
         if (!src.contains(itm)) 
             to_remove.push_back(itm);
     while (!to_remove.empty()) {
@@ -41,7 +41,7 @@ void set_intersection(Set1 & tgt, const Set2 & src) {
 
 template<class Set>
 void set_difference(Set & tgt, const Set & to_remove) {
-    for (auto const& itm : to_remove) 
+    for (auto itm : to_remove) 
         tgt.remove(itm);
 }