From 2999d33ede0611aba0e60d03c89d96231cf4a799 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Jan 2020 16:03:45 -0800 Subject: [PATCH] reuse m_bv_sym based on stack in #2842 Signed-off-by: Nikolaj Bjorner --- src/ast/bv_decl_plugin.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 0154b3b58..b7e91c566 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -151,7 +151,7 @@ void bv_decl_plugin::mk_bv_sort(unsigned bv_size) { else { sz = sort_size(rational::power_of_two(bv_size)); } - m_bv_sorts[bv_size] = m_manager->mk_sort(symbol("bv"), sort_info(m_family_id, BV_SORT, sz, 1, &p)); + m_bv_sorts[bv_size] = m_manager->mk_sort(m_bv_sym, sort_info(m_family_id, BV_SORT, sz, 1, &p)); m_manager->inc_ref(m_bv_sorts[bv_size]); } } @@ -163,7 +163,7 @@ inline sort * bv_decl_plugin::get_bv_sort(unsigned bv_size) { } parameter p(bv_size); sort_size sz(sort_size::mk_very_big()); - return m_manager->mk_sort(symbol("bv"), sort_info(m_family_id, BV_SORT, sz, 1, &p)); + return m_manager->mk_sort(m_bv_sym, sort_info(m_family_id, BV_SORT, sz, 1, &p)); } sort * bv_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { @@ -853,11 +853,11 @@ bool bv_recognizers::mult_inverse(rational const & n, unsigned bv_size, rational } bv_util::bv_util(ast_manager & m): - bv_recognizers(m.mk_family_id(symbol("bv"))), + bv_recognizers(m.mk_family_id(m_plugin->m_bv_sym)), m_manager(m) { - SASSERT(m.has_plugin(symbol("bv"))); + SASSERT(m.has_plugin(m_plugin->m_bv_sym)); m_plugin = static_cast(m.get_plugin(m.mk_family_id("bv"))); -} + } app * bv_util::mk_numeral(rational const & val, sort* s) const { if (!is_bv_sort(s)) {