From 7ec02fc11f1e8884967c821b165db4f530adb98e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 8 Feb 2020 16:00:13 -0800 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/math/lp/int_branch.cpp | 6 +++--- src/math/lp/int_cube.cpp | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/math/lp/int_branch.cpp b/src/math/lp/int_branch.cpp index 2b7691572..eb670dedd 100644 --- a/src/math/lp/int_branch.cpp +++ b/src/math/lp/int_branch.cpp @@ -49,8 +49,8 @@ namespace lp { } TRACE("int_solver", - lia.display_column(tout << "branching v" << j << " = " << get_value(j) << "\n", j); - tout << "k = " << m_k << std::endl;); + lia.display_column(tout << "branching v" << j << " = " << lia.get_value(j) << "\n", j); + tout << "k = " << lia.m_k << std::endl;); return lia_move::branch; } @@ -114,7 +114,7 @@ namespace lp { inf_int_count++; if (!lia.is_boxed(j)) continue; - lp_assert(!is_fixed(j)); + lp_assert(!lia.is_fixed(j)); new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x; if (new_range > small_range_thresold) continue; diff --git a/src/math/lp/int_cube.cpp b/src/math/lp/int_cube.cpp index 3b5a87f65..87d89605d 100644 --- a/src/math/lp/int_cube.cpp +++ b/src/math/lp/int_cube.cpp @@ -28,7 +28,7 @@ namespace lp { lia.settings().stats().m_cube_calls++; TRACE("cube", for (unsigned j = 0; j < lra.A_r().column_count(); j++) - display_column(tout, j); + lia.display_column(tout, j); tout << lra.constraints(); ); @@ -50,7 +50,7 @@ namespace lp { lra.pop(); lra.round_to_integer_solution(); lra.set_status(lp_status::FEASIBLE); - lp_assert(lia.settings().get_cancel_flag() || is_feasible()); + lp_assert(lia.settings().get_cancel_flag() || lia.is_feasible()); TRACE("cube", tout << "success";); lia.settings().stats().m_cube_success++; return lia_move::sat;