remove recalculated entries from S

Signed-off-by: Lev Nachmanson <[email protected]>
Z3Prover · Jan 24, 2025 · 5f292d6 · 5f292d6
1 parent a71263a
commit 5f292d6
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
@@ -698,7 +698,9 @@ namespace lp {
                 m_l_matrix.multiply_row(ei, denom);
                 m_e_matrix.multiply_row(ei, denom);
             }
-
+            if (belongs_to_s(ei)) {
+                remove_from_S(ei);
+            }
             SASSERT(entry_invariant(ei));
         }