mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

fix #2788

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-07 09:46:33 +03:00
parent 8eb2356b68
commit 3fa3c8bf76
1 changed files with 16 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/smt/theory_arith_core.h
View file

@ -214,22 +214,28 @@ namespace smt {
row & r = m_rows[r_id];
column & c = m_columns[v];
if (row_vars().contains(v)) {
typename vector<row_entry>::iterator it = r.begin_entries();
typename vector<row_entry>::iterator end = r.end_entries();
bool found = false;
for (; !found && it != end; ++it) {
SASSERT(!it->is_dead());
if (it->m_var == v) {
for (unsigned r_idx = 0; r_idx < r.size(); ++r_idx) {
row_entry& re = r[r_idx];
SASSERT(!re.is_dead());
if (re.m_var == v) {
if (invert) {
it->m_coeff -= coeff;
re.m_coeff -= coeff;
}
else {
it->m_coeff += coeff;
re.m_coeff += coeff;
}
found = true;
if (re.m_coeff.is_zero()) {
unsigned c_idx = re.m_col_idx;
r.del_row_entry(r_idx);
c.del_col_entry(c_idx);
row_vars().remove(v);
r.compress(m_columns);
c.compress(m_rows);
}
return;
}
}
SASSERT(found);
SASSERT(false);
return;
}
row_vars().insert(v);