From a930a8d5d458d5ef41553a6ae891a45cfa77b2cb Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 14 Mar 2026 14:50:22 -1000 Subject: [PATCH] fix restore_x by recalulating new column values Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.h | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 5c7e7bbb0..b1c293346 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -446,8 +446,12 @@ public: cs.restore_x(); if (backup_sz < current_sz) { // New columns were added after backup. - // move_non_basic_columns_to_bounds snaps non-basic - // columns to their bounds and finds a feasible solution. + // Recalculate basic variable values from non-basic ones + // to restore the Ax=0 tableau invariant, then snap + // non-basic columns to their bounds and find a feasible solution. + 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)); move_non_basic_columns_to_bounds(); } else {