mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

pre-flatten use list before iterating over m_unsat

Browse source 
select_max_same_sign accesses the use-list which may cause it to be flattened.
This commit is contained in:
Nikolaj Bjorner 2025-01-30 16:34:17 -08:00
parent e3566288a4
commit c9ac4d6f75
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/sls/sat_ddfw.cpp
View file

@ -558,6 +558,7 @@ namespace sat {
void ddfw::shift_weights() { void ddfw::shift_weights() {
++m_shifts; ++m_shifts;
bool shifted = false; bool shifted = false;
flatten_use_list();
for (unsigned to_idx : m_unsat) { for (unsigned to_idx : m_unsat) {
SASSERT(!m_clauses[to_idx].is_true()); SASSERT(!m_clauses[to_idx].is_true());
unsigned from_idx = select_max_same_sign(to_idx); unsigned from_idx = select_max_same_sign(to_idx);