diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 2bdaf66c5..12d34c516 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1246,7 +1246,6 @@ namespace smt {
             if (!can_propagate()) {
                 return;
             }
-            unsigned qhead = m_asserted_qhead;
             while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent()) {
                 bool_var bv  = m_asserted_atoms[m_asserted_qhead].m_bv;
                 bool is_true = m_asserted_atoms[m_asserted_qhead].m_is_true;
@@ -1835,7 +1834,6 @@ namespace smt {
         // bounds propagation.
         // 
         void propagate_bound_compound(bool_var bv, bool is_true, lp::bound& b) {
-            lp::bound_kind k = b.get_bound_kind();
             theory_var v = b.get_var();
             TRACE("arith", tout << mk_pp(get_owner(v), m) << "\n";);
             if (static_cast<unsigned>(v) >= m_use_list.size()) {
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 4ce1da7c3..57b5f49cf 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -1691,7 +1691,10 @@ public:
 
     bool explanation_is_correct(const vector<std::pair<mpq, unsigned>>& explanation) const {
 #ifdef LEAN_DEBUG
+#if 0
+        // disabled as 'kind' is not assigned
         lconstraint_kind kind;
+        the_relations_are_of_same_type(explanation, kind);
         lean_assert(the_left_sides_sum_to_zero(explanation));
         mpq rs = sum_of_right_sides_of_explanation(explanation);
         switch (kind) {
@@ -1709,6 +1712,7 @@ public:
             lean_assert(false);
             return false;
         }
+#endif
 #endif
         return true;
     }
diff --git a/src/util/lp/random_updater.hpp b/src/util/lp/random_updater.hpp
index 56593b493..68e2f5bc9 100644
--- a/src/util/lp/random_updater.hpp
+++ b/src/util/lp/random_updater.hpp
@@ -184,7 +184,7 @@ void random_updater::remove_value(numeric_pair<mpq>& v) {
     lean_assert(it != m_values.end());
     it->second--;
     if (it->second == 0)
-        m_values.erase(it);
+        m_values.erase((std::unordered_map<numeric_pair<mpq>, unsigned>::const_iterator)it);
 }
 
 void random_updater::add_column_to_sets(unsigned j) {