diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 3c10e7626..4ce1da7c3 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -1692,7 +1692,6 @@ public:
     bool explanation_is_correct(const vector<std::pair<mpq, unsigned>>& explanation) const {
 #ifdef LEAN_DEBUG
         lconstraint_kind kind;
-        lean_assert(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) {
diff --git a/src/util/lp/random_updater.hpp b/src/util/lp/random_updater.hpp
index 67bfcc49b..56593b493 100644
--- a/src/util/lp/random_updater.hpp
+++ b/src/util/lp/random_updater.hpp
@@ -180,7 +180,7 @@ void random_updater::add_value(numeric_pair<mpq>& v) {
 }
 
 void random_updater::remove_value(numeric_pair<mpq>& v) {
-    auto it = m_values.find(v);
+    std::unordered_map<numeric_pair<mpq>, unsigned>::iterator it = m_values.find(v);
     lean_assert(it != m_values.end());
     it->second--;
     if (it->second == 0)