diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index b7e91c566..dfcb70537 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -853,10 +853,10 @@ 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(m_plugin->m_bv_sym)), + bv_recognizers(m.mk_family_id(symbol("bv"))), m_manager(m) { - SASSERT(m.has_plugin(m_plugin->m_bv_sym)); m_plugin = static_cast(m.get_plugin(m.mk_family_id("bv"))); + SASSERT(m.has_plugin(symbol("bv"))); } app * bv_util::mk_numeral(rational const & val, sort* s) const {