diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index 0ef3b60d6..8b77244f9 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -766,7 +766,7 @@ bool bv_recognizers::is_zero(expr const * n) const {
     return decl->get_parameter(0).get_rational().is_zero();
 }
 
-bool bv_recognizers::is_extract(expr const* e, unsigned& low, unsigned& high, expr*& b) {
+bool bv_recognizers::is_extract(expr const* e, unsigned& low, unsigned& high, expr*& b) const {
     if (!is_extract(e)) return false;
     low = get_extract_low(e);
     high = get_extract_high(e);
@@ -774,7 +774,7 @@ bool bv_recognizers::is_extract(expr const* e, unsigned& low, unsigned& high, ex
     return true;
 }
 
-bool bv_recognizers::is_bv2int(expr const* e, expr*& r) {
+bool bv_recognizers::is_bv2int(expr const* e, expr*& r) const {
     if (!is_bv2int(e)) return false;
     r = to_app(e)->get_arg(0);
     return true;
diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index 8ea90f844..c5ebfb2d9 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -288,10 +288,10 @@ public:
     bool is_extract(expr const * e) const { return is_app_of(e, get_fid(), OP_EXTRACT); }
     unsigned get_extract_high(func_decl const * f) const { return f->get_parameter(0).get_int(); }
     unsigned get_extract_low(func_decl const * f) const { return f->get_parameter(1).get_int(); }
-    unsigned get_extract_high(expr const * n) { SASSERT(is_extract(n)); return get_extract_high(to_app(n)->get_decl()); }
-    unsigned get_extract_low(expr const * n) { SASSERT(is_extract(n)); return get_extract_low(to_app(n)->get_decl()); }
-    bool is_extract(expr const * e, unsigned & low, unsigned & high, expr * & b);
-    bool is_bv2int(expr const * e, expr * & r);
+    unsigned get_extract_high(expr const * n) const { SASSERT(is_extract(n)); return get_extract_high(to_app(n)->get_decl()); }
+    unsigned get_extract_low(expr const * n) const { SASSERT(is_extract(n)); return get_extract_low(to_app(n)->get_decl()); }
+    bool is_extract(expr const * e, unsigned & low, unsigned & high, expr * & b) const;
+    bool is_bv2int(expr const * e, expr * & r) const;
     bool is_bv_add(expr const * e) const { return is_app_of(e, get_fid(), OP_BADD); }
     bool is_bv_sub(expr const * e) const { return is_app_of(e, get_fid(), OP_BSUB); }
     bool is_bv_mul(expr const * e) const { return is_app_of(e, get_fid(), OP_BMUL); }