From 605a4744c631ce92e801d232bb65dada818a59ad Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 Oct 2025 00:15:49 -0700 Subject: [PATCH] revert a regression from PR Signed-off-by: Nikolaj Bjorner --- src/smt/smt_internalizer.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 6aa17d0b9..45c174f65 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -988,8 +988,7 @@ namespace smt { void context::undo_mk_bool_var() { - SASSERT(!m_b_internalized_stack.empty(ue key per literal - m_lit_scores[lit.sign()][v] += 1.)); + SASSERT(!m_b_internalized_stack.empty()); m_stats.m_num_del_bool_var++; expr * n = m_b_internalized_stack.back(); unsigned n_id = n->get_id();