diff --git a/src/math/lp/general_matrix.h b/src/math/lp/general_matrix.h
index 6a996ddfa..749fa30dc 100644
--- a/src/math/lp/general_matrix.h
+++ b/src/math/lp/general_matrix.h
@@ -108,7 +108,7 @@ public:
     void init_row_from_container(int i, const T & c, std::function<unsigned (unsigned)> column_fix, const mpq& sign) {
         auto & row = m_data[adjust_row(i)];
         lp_assert(row_is_initialized_correctly(row));
-        for (const auto & p : c) {
+        for (lp::lar_term::ival p : c) {
             unsigned j = adjust_column(column_fix(p.column().index()));
             row[j] = sign * p.coeff();
         }
diff --git a/src/math/lp/int_cube.cpp b/src/math/lp/int_cube.cpp
index 269a85386..cdf190865 100644
--- a/src/math/lp/int_cube.cpp
+++ b/src/math/lp/int_cube.cpp
@@ -85,7 +85,7 @@ namespace lp {
         if (t.size() == 2) {
             bool seen_minus = false;
             bool seen_plus = false;
-            for(const auto & p : t) {
+            for(lar_term::ival p : t) {
                 if (!lia.column_is_int(p.column()))
                     goto usual_delta;
                 const mpq & c = p.coeff();
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index e01ba746a..88db78d85 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -271,7 +271,7 @@ std::ostream& core::print_explanation(const lp::explanation& exp, std::ostream&
 
 bool core::explain_upper_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_upper_bound(p, pb, e)) {
             b += pb;