From 7f1e74c0da681c467997fbaf1900f0fdde977ac9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 Jun 2026 10:49:05 -0700 Subject: [PATCH] remove atom Signed-off-by: Nikolaj Bjorner --- src/smt/smt_solver.cpp | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index aa575a336..69e63d1f2 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -233,18 +233,16 @@ namespace { unsigned get_assign_level(expr* e) const override { auto const& ctx = m_context.get_context(); - expr* atom = e; - get_manager().is_not(e, atom); - if (!ctx.b_internalized(atom)) + get_manager().is_not(e, e); + if (!ctx.b_internalized(e)) return UINT_MAX; - return ctx.get_assign_level(ctx.get_bool_var(atom)); + return ctx.get_assign_level(ctx.get_bool_var(e)); } bool is_relevant(expr* e) const override { auto const& ctx = m_context.get_context(); - expr* atom = e; - get_manager().is_not(e, atom); - return ctx.b_internalized(atom) && ctx.is_relevant(atom); + get_manager().is_not(e, e); + return ctx.b_internalized(e) && ctx.is_relevant(e); } unsigned get_num_bool_vars() const override { @@ -253,9 +251,8 @@ namespace { sat::bool_var get_bool_var(expr* e) const override { auto const& ctx = m_context.get_context(); - expr* atom = e; - get_manager().is_not(e, atom); - return ctx.b_internalized(atom) ? ctx.get_bool_var(atom) : sat::null_bool_var; + get_manager().is_not(e, e); + return ctx.b_internalized(e) ? ctx.get_bool_var(e) : sat::null_bool_var; } void pop_to_base_level() override {