From eff3f5f65eecd6772b7a6827d31676785ab4443f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 22 Sep 2023 09:45:58 -0700 Subject: [PATCH] port bug fixes from unit prop branch Signed-off-by: Nikolaj Bjorner --- src/math/lp/int_solver.cpp | 2 +- src/math/lp/lar_constraints.h | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 0ab7d1e40..1964262f3 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -31,7 +31,7 @@ namespace lp { lra.remove_fixed_vars_from_base(); lp_assert(lia.is_feasible()); for (unsigned j : lra.r_basis()) - if (!lra.get_value(j).is_int() && lra.column_is_int(j)) + if (!lra.get_value(j).is_int() && lra.column_is_int(j) && !lia.is_fixed(j)) patch_basic_column(j); if (!lia.has_inf_int()) { lia.settings().stats().m_patches_success++; diff --git a/src/math/lp/lar_constraints.h b/src/math/lp/lar_constraints.h index 0a16353c1..f0c937324 100644 --- a/src/math/lp/lar_constraints.h +++ b/src/math/lp/lar_constraints.h @@ -136,9 +136,10 @@ class constraint_set { } public: - constraint_set(u_dependency_manager& d, column_namer& cn): - m_dep_manager(d), - m_namer(cn) {} + constraint_set(u_dependency_manager& d, column_namer& cn): + m_namer(cn), + m_dep_manager(d) + {} ~constraint_set() { for (auto* c : m_constraints)