From 8895ed7122e881faa4709d92d906384078770ad1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 1 Jul 2018 18:34:02 -0700
Subject: [PATCH] remove unintialized variable

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_lra.cpp     | 1 +
 src/util/lp/lar_solver.cpp | 1 -
 2 files changed, 1 insertion(+), 1 deletion(-)

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) {