From 95f86ae2c0533231880c49ba00b56bc1800cda0a Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 3 Aug 2017 11:03:52 -0700 Subject: [PATCH] more efficient lar_solver::get_model Signed-off-by: Lev Nachmanson --- src/util/lp/lar_solver.h | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index bded5dc26..c8048a550 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -1259,7 +1259,7 @@ public: void get_model(std::unordered_map & variable_values) const { - mpq delta = mpq(1, 2); // start from 0.5 to have less clashes + mpq delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(mpq(1, 2)); // start from 0.5 to have less clashes lean_assert(m_status == OPTIMAL); unsigned i; do { @@ -1267,7 +1267,6 @@ public: // different pairs have to produce different singleton values std::unordered_set set_of_different_pairs; std::unordered_set set_of_different_singles; - delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta); for (i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) { const numeric_pair & rp = m_mpq_lar_core_solver.m_r_x[i]; set_of_different_pairs.insert(rp);