From de028f33a226153cc10367adc94c3d09418dfebc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jun 2026 15:40:11 -0700 Subject: [PATCH] Update inc_sat_solver.cpp --- src/sat/sat_solver/inc_sat_solver.cpp | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index e8cd6d3fd..f5a5eed75 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -406,16 +406,14 @@ public: } unsigned get_assign_level(expr* e) const override { - expr* atom = e; - m.is_not(e, atom); - sat::bool_var bv = m_map.to_bool_var(atom); + m.is_not(e, e); + sat::bool_var bv = m_map.to_bool_var(e); return bv == sat::null_bool_var ? UINT_MAX : m_solver.lvl(bv); } bool is_relevant(expr* e) const override { - expr* atom = e; - m.is_not(e, atom); - sat::bool_var bv = m_map.to_bool_var(atom); + m.is_not(e, e); + sat::bool_var bv = m_map.to_bool_var(e); if (bv == sat::null_bool_var) return true; auto* ext = dynamic_cast(m_solver.get_extension()); @@ -427,9 +425,8 @@ public: } unsigned get_bool_var(expr* e) const override { - expr* atom = e; - m.is_not(e, atom); - sat::bool_var bv = m_map.to_bool_var(atom); + m.is_not(e, e); + auto bv = m_map.to_bool_var(atom); return bv == sat::null_bool_var ? UINT_MAX : bv; }