mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

allow bounds tightening on fixed columns

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-03-12 17:31:34 -07:00 • committed by Lev Nachmanson
parent f501aea3eb
commit ecfbdbbd23
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1028,8 +1028,8 @@ namespace lp {
eliminate_substituted_in_changed_rows();
m_changed_columns.reset();
SASSERT(m_changed_columns.size() == 0);
m_changed_rows.reset();
// do not clean up m_changed_terms as they are used in tighten_terms_with_S()
SASSERT(entries_are_ok());
}
@ -1372,7 +1372,7 @@ namespace lp {
if (j >= lra.column_count() ||
!lra.column_has_term(j) ||
lra.column_is_free(j) ||
is_fixed(j) || !lia.column_is_int(j)) {
!lia.column_is_int(j)) {
cleanup.push_back(j);
continue;
}