diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index dc393676e..03c46d004 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2610,6 +2610,7 @@ public:
         lp::var_index vi = m_theory_var2var_index[v];
         rational val;
         if (m_solver->has_value(vi, val)) {
+            if (is_int(n) && !val.is_int()) return false;
             r = a.mk_numeral(val, is_int(n));
             return true;
         }
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 122d01c8d..35a5095d2 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -1024,7 +1024,6 @@ bool lar_solver::the_right_sides_do_not_sum_to_zero(const vector<std::pair<mpq,
 bool lar_solver::explanation_is_correct(const vector<std::pair<mpq, unsigned>>& explanation) const {
 #ifdef Z3DEBUG
     lconstraint_kind kind;
-    lp_assert(the_relations_are_of_same_type(explanation, kind));
     lp_assert(the_left_sides_sum_to_zero(explanation));
     mpq rs = sum_of_right_sides_of_explanation(explanation);
     switch (kind) {