make reset updates recursive

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Aug 24, 2024 · d6b89ba · d6b89ba
1 parent 47b793a
commit d6b89ba
Showing 1 changed file with 11 additions and 7 deletions.
diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
@@ -1500,13 +1500,7 @@ namespace sls {
                 add_update(w, delta);
         }
         for (auto const& [coeff, w] : coeffs)
-            if (is_mul(w)) {
-                auto const& [w1, c, monomial] = get_mul(w);
-                for (auto [w1, p] : monomial)
-                    add_reset_update(w1);
-            }
-            else
-                add_reset_update(w);    
+            add_reset_update(w);    
 
         if (apply_update())
             return eval_is_correct(v);
@@ -1769,6 +1763,16 @@ namespace sls {
         m_last_delta = 0;
         if (is_fixed(x))
             return;
+        if (is_mul(x)) {
+            auto const& [w1, c, monomial] = get_mul(x);
+            for (auto [w1, p] : monomial)
+                add_reset_update(w1);
+        }
+        if (is_add(x)) {
+            auto const& ad = get_add(x);
+            for (auto [c, w] : ad.m_args)
+                add_reset_update(w);
+        }
         auto const& vi = m_vars[x];
         auto const& lo = vi.m_lo;
         auto const& hi = vi.m_hi;