mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-24 13:18:55 +00:00
Code Activity

fix #1984 - already fixed in private branch, but wasn't propagated to master

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-11-28 13:49:53 -08:00
parent eea9b79035
commit 5dc1337476
2 changed files with 10 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/arith_eq_solver.cpp
View file

@ -608,8 +608,8 @@ bool arith_eq_solver::solve_integer_equations_gcd(
return false;
}
live.erase(live.begin()+live_pos);
for (j = 0; j < live.size(); ++j) {
row& r = rows[live[j]];
for (unsigned l : live) {
row& r = rows[l];
if (!r[i].is_zero()) {
substitute(r, r0, i);
gcd_normalize(r);
@ -625,10 +625,7 @@ bool arith_eq_solver::solve_integer_equations_gcd(
TRACE("arith_eq_solver",
tout << ((live.size()<=1)?"solved ":"incomplete check ") << live.size() << "\n";
for (unsigned i = 0; i < live.size(); ++i) {
print_row(tout, rows[live[i]]);
}
);
for (unsigned l : live) print_row(tout, rows[l]); );
return true;
}