diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index 2248afe02..40f5c6b49 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -219,7 +219,6 @@ namespace lp {
         void init() {
             m_e_matrix = static_matrix<mpq, mpq>(lra.row_count(), lra.column_count());
             m_report_branch = false;
-            unsigned n_of_rows = lra.A_r().row_count();
             m_k2s.clear();
             m_k2s.resize(lra.column_count(), -1);
             m_conflict_index = -1;
@@ -230,7 +229,7 @@ namespace lp {
             for (unsigned i = 0; i < lra.terms().size(); i++) {
                 const lar_term* t = lra.terms()[i];
                 TRACE("dioph_eq",  tout << "term "<< i <<":"; lra.print_term(*t, tout) << "\n";
-                    for(auto & p: *t) {
+                    for(const auto & p: *t) {
                         lra.print_column_info(p.var(), tout);
                     }
                 );
diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h
index 577503c13..436dda46e 100644
--- a/src/math/lp/static_matrix.h
+++ b/src/math/lp/static_matrix.h
@@ -47,7 +47,7 @@ template <typename T>
 using row_strip = vector<row_cell<T>>; 
 template <typename K> mpq get_denominators_lcm(const K & row) {
     mpq r = mpq(1);
-    for (auto & c : row) 
+    for (const auto & c : row) 
         r = lcm(r, denominator(c.coeff()));
     return r;
 }