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

na

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-31 11:27:06 -07:00
parent 22b5b63743
commit 475ac77897
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/fixplex_def.h
View file

@ -844,6 +844,7 @@ namespace polysat {
unsigned rz = r_z.id(); unsigned rz = r_z.id();
if (rz == rx) if (rz == rx)
continue; continue;
TRACE("fixplex", display_row(tout << "eliminate ", r_z, false) << "\n";);
VERIFY(eliminate_var(r_x, col, tz_b, old_value_y)); VERIFY(eliminate_var(r_x, col, tz_b, old_value_y));
TRACE("fixplex", display_row(tout << "eliminated ", r_z, false) << "\n";); TRACE("fixplex", display_row(tout << "eliminated ", r_z, false) << "\n";);
add_patch(row2base(r_z)); add_patch(row2base(r_z));