mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-29 07:27:57 +00:00
Code Activity

Merge branch 'dio' of https://github.com/Z3Prover/Z3 into dio

Browse source
This commit is contained in:
Lev Nachmanson 2025-02-25 10:58:24 -10:00
commit f9b4f68982
2 changed files with 4 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/math/lp/dioph_eq.cpp
View file

@ -1377,15 +1377,11 @@ namespace lp {
std_vector<unsigned> cleanup; std_vector<unsigned> cleanup;
m_tightened_columns.reset(); m_tightened_columns.reset();
for (unsigned j : m_changed_terms) { for (unsigned j : m_changed_terms) {
if ( if (j >= lra.column_count() ||
j >= lra.column_count() ||
!lra.column_has_term(j) || !lra.column_has_term(j) ||
lra.column_is_free(j) || lra.column_is_free(j) ||
is_fixed(j) || !lia.column_is_int(j) ||
!lia.column_is_int(j) !term_has_int_inv_vars(j)) {
||
!term_has_int_inv_vars(j)
) {
cleanup.push_back(j); cleanup.push_back(j);
continue; continue;
} }

2
src/math/lp/int_solver.cpp
View file

@ -188,7 +188,7 @@ namespace lp {
} }
bool should_gomory_cut() { bool should_gomory_cut() {
return (!settings().dio_eqs() || settings().dio_enable_gomory_cuts()) return (!all_columns_are_integral() ||(!settings().dio_eqs() || settings().dio_enable_gomory_cuts()))
&& m_number_of_calls % settings().m_int_gomory_cut_period == 0; && m_number_of_calls % settings().m_int_gomory_cut_period == 0;
} }