mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-27 06:26:35 +00:00
Code Activity

assert entry_invariant only when all changes are done

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-12-25 11:33:32 -10:00
parent f26facaf8f
commit ce2405aab6
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -988,7 +988,6 @@ namespace lp {
if (belongs_to_s(ei)) {
remove_from_S(ei);
}
SASSERT(entry_invariant(ei));
}
void find_changed_terms_and_more_changed_rows() {
@ -1099,6 +1098,7 @@ namespace lp {
m_changed_f_columns.reset();
m_changed_rows.reset();
m_changed_terms.reset();
SASSERT(entries_are_ok());
}
int get_sign_in_e_row(unsigned ei, unsigned j) const {