From 78c06bcc50cfa1263307c0e57d20e47a3a4ad61a Mon Sep 17 00:00:00 2001
From: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Date: Wed, 24 Jun 2026 22:59:34 -0700
Subject: [PATCH] sat solver uses actual phase birthdate instead of preferred
 phase birthdate for bb ranking

---
 src/sat/sat_solver.cpp | 9 +--------
 src/sat/sat_solver.h   | 1 -
 2 files changed, 1 insertion(+), 9 deletions(-)

diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 9cda41b50b..0a109bd0c5 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1744,13 +1744,6 @@ namespace sat {
         }
     }
 
-    uint64_t solver::get_preferred_phase_birthdate(bool_var v) const {
-        bool use_best =
-            m_config.m_phase == PS_FROZEN ||
-            ((m_config.m_phase == PS_SAT_CACHING || m_config.m_phase == PS_LOCAL_SEARCH) && m_search_state == s_sat);
-        return use_best ? m_best_phase_birthdate[v] : m_phase_birthdate[v];
-    }
-
     void solver::get_backbone_candidates(literal_vector& lits, unsigned max_num) {
         struct candidate {
             literal lit;
@@ -1762,7 +1755,7 @@ namespace sat {
             if (value(v) != l_undef || was_eliminated(v))
                 continue;
             bool is_pos = guess(v);
-            cands.push_back({ literal(v, !is_pos), now - get_preferred_phase_birthdate(v) });
+            cands.push_back({ literal(v, !is_pos), now - get_phase_birthdate(v) });
         }
         std::stable_sort(cands.begin(), cands.end(),
             [](candidate const& a, candidate const& b) { return a.age > b.age; });
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index c7ddd22f0e..66352387a2 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -382,7 +382,6 @@ namespace sat {
         bool get_best_phase(bool_var b) { return m_best_phase.get(b, false); }
         uint64_t get_phase_birthdate(bool_var b) const { return m_phase_birthdate.get(b, 0); }
         uint64_t get_best_phase_birthdate(bool_var b) const { return m_best_phase_birthdate.get(b, 0); }
-        uint64_t get_preferred_phase_birthdate(bool_var b) const;
         void set_has_new_best_phase(bool b) { m_new_best_phase = b; }
         bool has_new_best_phase() const { return m_new_best_phase; }
         void move_to_front(bool_var b);