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<bv_decl_plugin*>(m.get_plugin(m.mk_family_id("bv")));
-}
+    }
 
 app * bv_util::mk_numeral(rational const & val, sort* s) const {
     if (!is_bv_sort(s)) {