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

allow fixed variables is term tightening

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-02-24 13:07:40 -08:00
parent 3271f2fad9
commit 447af0f548
1 changed files with 3 additions and 7 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;
} }