diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 8c6d8065d..e146c271d 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -126,6 +126,7 @@ namespace lp { } bool all_columns_are_integral() const { + return true; // otherwise it never returns true! for (lpvar j = 0; j < lra.number_of_vars(); j++) if (!lra.column_is_int(j)) return false; diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 90c932b09..9d2fe675e 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -34,6 +34,7 @@ void lp::lp_settings::updt_params(params_ref const& _p) { m_nlsat_delay = p.arith_nl_delay(); m_dio_eqs = p.arith_lp_dio_eqs(); m_dio_enable_gomory_cuts = p.arith_lp_dio_cuts_enable_gomory(); + m_dio_enable_hnf_cuts = p.arith_lp_dio_cuts_enable_hnf(); m_dio_branching_period = p.arith_lp_dio_branching_period(); m_dump_bound_lemmas = p.arith_dump_bound_lemmas(); }