From c9ac4d6f75119ecae98fe74b5c6099c1fd4adf0e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 30 Jan 2025 16:34:17 -0800
Subject: [PATCH] pre-flatten use list before iterating over m_unsat

select_max_same_sign accesses the use-list which may cause it to be flattened.
---
 src/ast/sls/sat_ddfw.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/ast/sls/sat_ddfw.cpp b/src/ast/sls/sat_ddfw.cpp
index da6d567f8..1e9c484af 100644
--- a/src/ast/sls/sat_ddfw.cpp
+++ b/src/ast/sls/sat_ddfw.cpp
@@ -558,6 +558,7 @@ namespace sat {
     void ddfw::shift_weights() {
         ++m_shifts;
         bool shifted = false;
+        flatten_use_list();
         for (unsigned to_idx : m_unsat) {
             SASSERT(!m_clauses[to_idx].is_true());
             unsigned from_idx = select_max_same_sign(to_idx);