mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-05 00:20:50 +00:00
Code Activity

fix restore_x by recalulating new column values

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-03-14 14:55:44 -10:00
parent a930a8d5d4
commit b2b811749a
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/lp/lar_solver.h
View file

@ -450,8 +450,7 @@ public:
// to restore the Ax=0 tableau invariant, then snap // to restore the Ax=0 tableau invariant, then snap
// non-basic columns to their bounds and find a feasible solution. // non-basic columns to their bounds and find a feasible solution.
for (unsigned i = 0; i < A_r().row_count(); i++) for (unsigned i = 0; i < A_r().row_count(); i++)
if (r_basis()[i] >= backup_sz) set_column_value(r_basis()[i], get_basic_var_value_from_row(i));
set_column_value(r_basis()[i], get_basic_var_value_from_row(i));
move_non_basic_columns_to_bounds(); move_non_basic_columns_to_bounds();
} }
else { else {