From d43c12413d0e7d8e505cfb499c308c08f89a70be Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 9 May 2017 15:27:42 -0700 Subject: [PATCH] add disambiguation, avoid uninitialzed variable passing in debug mode Signed-off-by: Nikolaj Bjorner --- src/util/lp/lar_solver.h | 1 - src/util/lp/random_updater.hpp | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) 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>& 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& v) { } void random_updater::remove_value(numeric_pair& v) { - auto it = m_values.find(v); + std::unordered_map, unsigned>::iterator it = m_values.find(v); lean_assert(it != m_values.end()); it->second--; if (it->second == 0)