diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index a89cc18d0..093f6b346 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -573,18 +573,7 @@ expr * arith_decl_plugin::get_some_value(sort * s) {
     return mk_numeral(rational(0), s == m_int_decl);
 }
 
-arith_util::arith_util(ast_manager & m):
-    m_manager(m),
-    m_afid(m.get_family_id("arith")),
-    m_plugin(0) {
-}
-
-void arith_util::init_plugin() {
-    SASSERT(m_plugin == 0);
-    m_plugin = static_cast<arith_decl_plugin*>(m_manager.get_plugin(m_afid));
-}
-
-bool arith_util::is_numeral(expr const * n, rational & val, bool & is_int) const {
+bool arith_recognizers::is_numeral(expr const * n, rational & val, bool & is_int) const {
     if (!is_app_of(n, m_afid, OP_NUM))
         return false;
     func_decl * decl = to_app(n)->get_decl();
@@ -593,6 +582,17 @@ bool arith_util::is_numeral(expr const * n, rational & val, bool & is_int) const
     return true;
 }
 
+arith_util::arith_util(ast_manager & m):
+    arith_recognizers(m.get_family_id("arith")),
+    m_manager(m),
+    m_plugin(0) {
+}
+
+void arith_util::init_plugin() {
+    SASSERT(m_plugin == 0);
+    m_plugin = static_cast<arith_decl_plugin*>(m_manager.get_plugin(m_afid));
+}
+
 bool arith_util::is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val) {
     if (!is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM))
         return false;
diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index c39768d4c..e63e866c3 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -187,36 +187,24 @@ public:
     virtual void set_cancel(bool f);
 };
 
-class arith_util {
-    ast_manager &       m_manager;
+/**
+   \brief Procedures for recognizing arithmetic expressions.
+   We don't need access to ast_manager, and operations can be simultaneously
+   executed in different threads.
+*/
+class arith_recognizers {
+protected:
     family_id           m_afid;
-    arith_decl_plugin * m_plugin;
-
-    void init_plugin();
-
-    arith_decl_plugin & plugin() const {
-        if (!m_plugin) const_cast<arith_util*>(this)->init_plugin();
-        SASSERT(m_plugin != 0);
-        return *m_plugin;
-    }
-    
 public:
-    arith_util(ast_manager & m);
+    arith_recognizers(family_id id):m_afid(id) {}
 
-    ast_manager & get_manager() const { return m_manager; }
     family_id get_family_id() const { return m_afid; }
 
-    algebraic_numbers::manager & am() { 
-        return plugin().am(); 
-    }
-
     bool is_arith_expr(expr const * n) const { return is_app(n) && to_app(n)->get_family_id() == m_afid; }
+    bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); }
     bool is_numeral(expr const * n, rational & val, bool & is_int) const;
     bool is_numeral(expr const * n, rational & val) const { bool is_int; return is_numeral(n, val, is_int); }
     bool is_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_NUM); }
-    bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); }
-    bool is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val);
-    algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n);
     bool is_zero(expr const * n) const { rational val; return is_numeral(n, val) && val.is_zero(); }
     bool is_minus_one(expr * n) const { rational tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); }
     // return true if \c n is a term of the form (* -1 r)
@@ -227,6 +215,7 @@ public:
         }
         return false;
     }
+
     bool is_le(expr const * n) const { return is_app_of(n, m_afid, OP_LE); }
     bool is_ge(expr const * n) const { return is_app_of(n, m_afid, OP_GE); }
     bool is_lt(expr const * n) const { return is_app_of(n, m_afid, OP_LT); }
@@ -245,14 +234,13 @@ public:
     bool is_power(expr const * n) const { return is_app_of(n, m_afid, OP_POWER); }
     
     bool is_int(sort const * s) const { return is_sort_of(s, m_afid, INT_SORT); }
-    bool is_int(expr const * n) const { return is_int(m_manager.get_sort(n)); }
+    bool is_int(expr const * n) const { return is_int(get_sort(n)); }
     bool is_real(sort const * s) const { return is_sort_of(s, m_afid, REAL_SORT); }
-    bool is_real(expr const * n) const { return is_real(m_manager.get_sort(n)); }
+    bool is_real(expr const * n) const { return is_real(get_sort(n)); }
     bool is_int_real(sort const * s) const { return s->get_family_id() == m_afid; }
-    bool is_int_real(expr const * n) const { return is_int_real(m_manager.get_sort(n)); }
+    bool is_int_real(expr const * n) const { return is_int_real(get_sort(n)); }
 
     MATCH_UNARY(is_uminus);
-
     MATCH_BINARY(is_sub);
     MATCH_BINARY(is_add);
     MATCH_BINARY(is_mul);
@@ -265,6 +253,34 @@ public:
     MATCH_BINARY(is_div);
     MATCH_BINARY(is_idiv);
 
+    bool is_pi(expr * arg) { return is_app_of(arg, m_afid, OP_PI); }
+    bool is_e(expr * arg) { return is_app_of(arg, m_afid, OP_E); }
+};
+
+class arith_util : public arith_recognizers {
+    ast_manager &       m_manager;
+    arith_decl_plugin * m_plugin;
+
+    void init_plugin();
+
+    arith_decl_plugin & plugin() const {
+        if (!m_plugin) const_cast<arith_util*>(this)->init_plugin();
+        SASSERT(m_plugin != 0);
+        return *m_plugin;
+    }
+    
+public:
+    arith_util(ast_manager & m);
+
+    ast_manager & get_manager() const { return m_manager; }
+
+    algebraic_numbers::manager & am() { 
+        return plugin().am(); 
+    }
+
+    bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); }
+    bool is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val);
+    algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n);
     
     sort * mk_int() { return m_manager.mk_sort(m_afid, INT_SORT); }
     sort * mk_real() { return m_manager.mk_sort(m_afid, REAL_SORT); }
@@ -320,9 +336,6 @@ public:
     app * mk_acosh(expr * arg) { return m_manager.mk_app(m_afid, OP_ACOSH, arg); }
     app * mk_atanh(expr * arg) { return m_manager.mk_app(m_afid, OP_ATANH, arg); }
 
-    bool is_pi(expr * arg) { return is_app_of(arg, m_afid, OP_PI); }
-    bool is_e(expr * arg) { return is_app_of(arg, m_afid, OP_E); }
-
     app * mk_pi() { return plugin().mk_pi(); }
     app * mk_e()  { return plugin().mk_e(); }
 
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 3fb422a2e..94637bbdd 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -374,6 +374,31 @@ quantifier::quantifier(bool forall, unsigned num_decls, sort * const * decl_sort
     memcpy(const_cast<expr **>(get_no_patterns()), no_patterns, sizeof(expr *) * num_no_patterns);
 }
 
+// -----------------------------------
+//
+// Auxiliary functions
+//
+// -----------------------------------
+
+sort * get_sort(expr const * n) {
+    while (true) {
+        switch(n->get_kind()) {
+        case AST_APP: 
+            return to_app(n)->get_decl()->get_range();
+        case AST_VAR:
+            return to_var(n)->get_sort();
+        case AST_QUANTIFIER:
+            // The sort of the quantifier is the sort of the nested expression.
+            // This code assumes the given expression is well-sorted.
+            n = to_quantifier(n)->get_expr();
+            break;
+        default:
+            UNREACHABLE();
+            return 0;
+        }
+    }
+}
+
 // -----------------------------------
 //
 // AST hash-consing
@@ -1495,20 +1520,6 @@ void ast_manager::register_plugin(family_id id, decl_plugin * plugin) {
     plugin->set_manager(this, id);
 }
 
-sort * ast_manager::get_sort(expr const * n) const {
-    switch(n->get_kind()) {
-    case AST_APP: 
-        return to_app(n)->get_decl()->get_range();
-    case AST_VAR:
-        return to_var(n)->get_sort();
-    case AST_QUANTIFIER:
-        return m_bool_sort;
-    default:
-        UNREACHABLE();
-        return 0;
-    }
-}
-
 bool ast_manager::is_bool(expr const * n) const {
     return get_sort(n) == m_bool_sort;
 }
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 6af95e3a7..f899ed241 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1287,6 +1287,8 @@ inline bool has_labels(expr const * n) {
     else return false;
 }
 
+sort * get_sort(expr const * n);
+
 // -----------------------------------
 //
 // Get Some Value functor
@@ -1548,7 +1550,7 @@ protected:
     }
     
 public:
-    sort * get_sort(expr const * n) const;
+    sort * get_sort(expr const * n) const { return ::get_sort(n); }
     void check_sort(func_decl const * decl, unsigned num_args, expr * const * args) const;
     void check_sorts_core(ast const * n) const;
     bool check_sorts(ast const * n) const;
diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index fd15ca681..434bdaa11 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -41,26 +41,6 @@ bv_decl_plugin::bv_decl_plugin():
     m_int_sort(0) {
 }
 
-void bv_decl_plugin::mk_table_upto(unsigned n) {
-    if (m_powers.empty()) {
-        m_powers.push_back(rational(1));
-    }
-    unsigned sz = m_powers.size();
-    rational curr = m_powers[sz - 1];
-    rational two(2);
-    for (unsigned i = sz; i <= n; i++) {
-        curr *= two;
-        m_powers.push_back(curr);
-    }
-}
-
-rational bv_decl_plugin::power_of_two(unsigned n) const {
-    if (n >= m_powers.size()) {
-        const_cast<bv_decl_plugin*>(this)->mk_table_upto(n + 1);
-    }
-    return m_powers[n];
-}
-
 void bv_decl_plugin::set_manager(ast_manager * m, family_id id) {
     decl_plugin::set_manager(m, id);
 
@@ -169,7 +149,7 @@ void bv_decl_plugin::mk_bv_sort(unsigned bv_size) {
             sz = sort_size::mk_very_big();
         }
         else {
-            sz = sort_size(power_of_two(bv_size));
+            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_manager->inc_ref(m_bv_sorts[bv_size]);
@@ -436,7 +416,7 @@ func_decl * bv_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const
     // This cannot be enforced now, since some Z3 modules try to generate these invalid numerals.
     // After SMT-COMP, I should find all offending modules.
     // For now, I will just simplify the numeral here.
-    parameter p0(mod(parameters[0].get_rational(), power_of_two(bv_size)));
+    parameter p0(mod(parameters[0].get_rational(), rational::power_of_two(bv_size)));
     parameter ps[2] = { p0, parameters[1] };
     sort * bv = get_bv_sort(bv_size);
     return m_manager->mk_const_decl(m_bv_sym, bv, func_decl_info(m_family_id, OP_BV_NUM, num_parameters, ps));
@@ -621,7 +601,7 @@ void bv_decl_plugin::get_offset_term(app * a, expr * & t, rational & offset) con
         offset = decl->get_parameter(0).get_rational();
         sz     = decl->get_parameter(1).get_int();
         t      = a->get_arg(1);
-        offset = mod(offset, power_of_two(sz));
+        offset = mod(offset, rational::power_of_two(sz));
     }
     else {
         t      = a;
@@ -729,37 +709,104 @@ expr * bv_decl_plugin::get_some_value(sort * s) {
     return m_manager->mk_app(m_family_id, OP_BV_NUM, 2, p, 0, 0);
 }
 
-bv_util::bv_util(ast_manager & m):
-    m_manager(m) {
-    SASSERT(m.has_plugin(symbol("bv")));
-    m_plugin = static_cast<bv_decl_plugin*>(m.get_plugin(m.get_family_id("bv")));
-}
-
-rational bv_util::norm(rational const & val, unsigned bv_size, bool is_signed) const {
-    rational r = mod(val, power_of_two(bv_size));
+rational bv_recognizers::norm(rational const & val, unsigned bv_size, bool is_signed) const {
+    rational r = mod(val, rational::power_of_two(bv_size));
     SASSERT(!r.is_neg());
     if (is_signed) {
-        if (r >= power_of_two(bv_size - 1)) {
-            r -= power_of_two(bv_size);
+        if (r >= rational::power_of_two(bv_size - 1)) {
+            r -= rational::power_of_two(bv_size);
         }
-        if (r < -power_of_two(bv_size - 1)) { 
-            r += power_of_two(bv_size);
+        if (r < -rational::power_of_two(bv_size - 1)) { 
+            r += rational::power_of_two(bv_size);
         }
     }
     return r;
 }
 
-bool bv_util::has_sign_bit(rational const & n, unsigned bv_size) const {
+bool bv_recognizers::has_sign_bit(rational const & n, unsigned bv_size) const {
     SASSERT(bv_size > 0);
     rational m = norm(n, bv_size, false);
-    rational p = power_of_two(bv_size - 1);
+    rational p = rational::power_of_two(bv_size - 1);
     return m >= p;
 }
 
-bool bv_util::is_bv_sort(sort const * s) const {
+bool bv_recognizers::is_bv_sort(sort const * s) const {
     return (s->get_family_id() == get_fid() && s->get_decl_kind() == BV_SORT && s->get_num_parameters() == 1); 
 }
 
+bool bv_recognizers::is_numeral(expr const * n, rational & val, unsigned & bv_size) const {
+    if (!is_app_of(n, get_fid(), OP_BV_NUM)) {
+        return false;
+    }
+    func_decl * decl = to_app(n)->get_decl();
+    val     = decl->get_parameter(0).get_rational();
+    bv_size = decl->get_parameter(1).get_int();
+    return true;
+}
+
+bool bv_recognizers::is_allone(expr const * e) const {
+    rational r;
+    unsigned bv_size;
+    if (!is_numeral(e, r, bv_size)) {
+        return false;
+    }
+    bool result = (r == rational::power_of_two(bv_size) - rational(1));
+    TRACE("is_allone", tout << r << " " << result << "\n";);
+    return result;
+}
+
+bool bv_recognizers::is_zero(expr const * n) const {
+    if (!is_app_of(n, get_fid(), OP_BV_NUM)) {
+        return false;
+    }
+    func_decl * decl = to_app(n)->get_decl();
+    return decl->get_parameter(0).get_rational().is_zero();
+}
+
+bool bv_recognizers::is_extract(expr const* e, unsigned& low, unsigned& high, expr*& b) {
+    if (!is_extract(e)) return false;
+    low = get_extract_low(e);
+    high = get_extract_high(e);
+    b = to_app(e)->get_arg(0);
+    return true;
+}
+
+bool bv_recognizers::is_bv2int(expr const* e, expr*& r) {
+    if (!is_bv2int(e)) return false;
+    r = to_app(e)->get_arg(0);
+    return true;
+}
+
+bool bv_recognizers::mult_inverse(rational const & n, unsigned bv_size, rational & result) {
+    if (n.is_one()) {
+        result = n;
+        return true;
+    }
+    
+    if (!mod(n, rational(2)).is_one()) {
+        return false;
+    }
+    
+    rational g;
+    rational x;
+    rational y;
+    g = gcd(n, rational::power_of_two(bv_size), x, y);
+    if (x.is_neg()) {
+        x = mod(x, rational::power_of_two(bv_size));
+    }
+    SASSERT(x.is_pos());
+    SASSERT(mod(x * n, rational::power_of_two(bv_size)).is_one());
+    result = x;
+    return true;
+}
+
+bv_util::bv_util(ast_manager & m):
+    bv_recognizers(m.get_family_id(symbol("bv"))),
+    m_manager(m) {
+    SASSERT(m.has_plugin(symbol("bv")));
+    m_plugin = static_cast<bv_decl_plugin*>(m.get_plugin(m.get_family_id("bv")));
+}
+
 app * bv_util::mk_numeral(rational const & val, sort* s) {
     if (!is_bv_sort(s)) {
         return 0;
@@ -774,65 +821,11 @@ app * bv_util::mk_numeral(rational const & val, unsigned bv_size) {
     return m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, 0);
 }
 
-bool bv_util::is_numeral(expr const * n, rational & val, unsigned & bv_size) const {
-    if (!is_app_of(n, get_fid(), OP_BV_NUM)) {
-        return false;
-    }
-    func_decl * decl = to_app(n)->get_decl();
-    val     = decl->get_parameter(0).get_rational();
-    bv_size = decl->get_parameter(1).get_int();
-    return true;
-}
-
-
-bool bv_util::is_allone(expr const * e) const {
-    rational r;
-    unsigned bv_size;
-    if (!is_numeral(e, r, bv_size)) {
-        return false;
-    }
-    bool result = (r == power_of_two(bv_size) - rational(1));
-    TRACE("is_allone", tout << r << " " << result << "\n";);
-    return result;
-}
-
-bool bv_util::is_zero(expr const * n) const {
-    if (!is_app_of(n, get_fid(), OP_BV_NUM)) {
-        return false;
-    }
-    func_decl * decl = to_app(n)->get_decl();
-    return decl->get_parameter(0).get_rational().is_zero();
-}
-
 sort * bv_util::mk_sort(unsigned bv_size) {
     parameter p[1] = { parameter(bv_size) };
     return m_manager.mk_sort(get_fid(), BV_SORT, 1, p);
 }
 
-
-bool bv_util::mult_inverse(rational const & n, unsigned bv_size, rational & result) {
-    if (n.is_one()) {
-        result = n;
-        return true;
-    }
-    
-    if (!mod(n, rational(2)).is_one()) {
-        return false;
-    }
-    
-    rational g;
-    rational x;
-    rational y;
-    g = gcd(n, power_of_two(bv_size), x, y);
-    if (x.is_neg()) {
-        x = mod(x, power_of_two(bv_size));
-    }
-    SASSERT(x.is_pos());
-    SASSERT(mod(x * n, power_of_two(bv_size)).is_one());
-    result = x;
-    return true;
-}
-
 app * bv_util::mk_bv2int(expr* e) {
     sort* s = m_manager.mk_sort(m_manager.get_family_id("arith"), INT_SORT);
     parameter p(s);
diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index 34f2baf6b..8ea90f844 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -127,9 +127,6 @@ inline func_decl * get_div0_decl(ast_manager & m, func_decl * decl) {
 
 class bv_decl_plugin : public decl_plugin {
 protected:
-    vector<rational> m_powers;
-    void mk_table_upto(unsigned n);
-
     symbol m_bv_sym;
     symbol m_concat_sym;
     symbol m_sign_extend_sym;
@@ -245,8 +242,6 @@ protected:
 public:
     bv_decl_plugin();
 
-    rational power_of_two(unsigned n) const;
-
     virtual ~bv_decl_plugin() {}
     virtual void finalize();
 
@@ -273,7 +268,70 @@ public:
     virtual expr * get_some_value(sort * s);
 };
 
-class bv_util {
+class bv_recognizers {
+    family_id m_afid;
+public:
+    bv_recognizers(family_id fid):m_afid(fid) {}
+
+    family_id get_fid() const { return m_afid; }
+    family_id get_family_id() const { return get_fid(); }
+
+    bool is_numeral(expr const * n, rational & val, unsigned & bv_size) const;
+    bool is_numeral(expr const * n) const { return is_app_of(n, get_fid(), OP_BV_NUM); }
+    bool is_allone(expr const * e) const;
+    bool is_zero(expr const * e) const;
+    bool is_bv_sort(sort const * s) const;
+    bool is_bv(expr const* e) const {  return is_bv_sort(get_sort(e)); }
+    
+    bool is_concat(expr const * e) const { return is_app_of(e, get_fid(), OP_CONCAT); }
+    bool is_extract(func_decl const * f) const { return is_decl_of(f, get_fid(), OP_EXTRACT); }
+    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);
+    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); }
+    bool is_bv_neg(expr const * e) const { return is_app_of(e, get_fid(), OP_BNEG); }
+    bool is_bv_sdiv(expr const * e) const { return is_app_of(e, get_fid(), OP_BSDIV); }
+    bool is_bv_udiv(expr const * e) const { return is_app_of(e, get_fid(), OP_BUDIV); }
+    bool is_bv_srem(expr const * e) const { return is_app_of(e, get_fid(), OP_BSREM); }
+    bool is_bv_urem(expr const * e) const { return is_app_of(e, get_fid(), OP_BUREM); }
+    bool is_bv_smod(expr const * e) const { return is_app_of(e, get_fid(), OP_BSMOD); }
+    bool is_bv_and(expr const * e) const { return is_app_of(e, get_fid(), OP_BAND); }
+    bool is_bv_or(expr const * e) const { return is_app_of(e, get_fid(), OP_BOR); }
+    bool is_bv_xor(expr const * e) const { return is_app_of(e, get_fid(), OP_BXOR); }
+    bool is_bv_nand(expr const * e) const { return is_app_of(e, get_fid(), OP_BNAND); }
+    bool is_bv_nor(expr const * e) const { return is_app_of(e, get_fid(), OP_BNOR); }
+    bool is_bv_not(expr const * e) const { return is_app_of(e, get_fid(), OP_BNOT); }
+    bool is_bv_ule(expr const * e) const { return is_app_of(e, get_fid(), OP_ULEQ); }
+    bool is_bv_sle(expr const * e) const { return is_app_of(e, get_fid(), OP_SLEQ); }
+    bool is_bit2bool(expr const * e) const { return is_app_of(e, get_fid(), OP_BIT2BOOL); }
+    bool is_bv2int(expr const* e) const { return is_app_of(e, get_fid(), OP_BV2INT); }
+    bool is_int2bv(expr const* e) const { return is_app_of(e, get_fid(), OP_INT2BV); }
+    bool is_mkbv(expr const * e) const { return is_app_of(e, get_fid(), OP_MKBV); }
+    bool is_bv_ashr(expr const * e) const { return is_app_of(e, get_fid(), OP_BASHR); }
+    bool is_bv_lshr(expr const * e) const { return is_app_of(e, get_fid(), OP_BLSHR); }
+    bool is_bv_shl(expr const * e) const { return is_app_of(e, get_fid(), OP_BSHL); }
+    bool is_sign_ext(expr const * e) const { return is_app_of(e, get_fid(), OP_SIGN_EXT); }
+
+    MATCH_BINARY(is_bv_add);
+    MATCH_BINARY(is_bv_mul);
+    MATCH_BINARY(is_bv_sle);
+    MATCH_BINARY(is_bv_ule);
+    MATCH_BINARY(is_bv_shl);
+
+    rational norm(rational const & val, unsigned bv_size, bool is_signed) const ;
+    rational norm(rational const & val, unsigned bv_size) const { return norm(val, bv_size, false); }
+    bool has_sign_bit(rational const & n, unsigned bv_size) const;
+    bool mult_inverse(rational const & n, unsigned bv_size, rational & result);
+    
+};
+
+class bv_util : public bv_recognizers {
     ast_manager &    m_manager;
     bv_decl_plugin * m_plugin;
 
@@ -282,29 +340,10 @@ public:
 
     ast_manager & get_manager() const { return m_manager; }
 
-    family_id get_fid() const { return m_plugin->get_family_id(); }
-
-    family_id get_family_id() const { return get_fid(); }
-
-    rational power_of_two(unsigned n) const { return m_plugin->power_of_two(n); }
-
-    rational norm(rational const & val, unsigned bv_size, bool is_signed) const ;
-    rational norm(rational const & val, unsigned bv_size) const { return norm(val, bv_size, false); }
-    bool has_sign_bit(rational const & n, unsigned bv_size) const;
     app * mk_numeral(rational const & val, sort* s);
     app * mk_numeral(rational const & val, unsigned bv_size);
     app * mk_numeral(uint64 u, unsigned bv_size) { return mk_numeral(rational(u, rational::ui64()), bv_size); }
     sort * mk_sort(unsigned bv_size);
-    bool is_numeral(expr const * n, rational & val, unsigned & bv_size) const;
-    bool is_numeral(expr const * n) const {
-        return is_app_of(n, get_fid(), OP_BV_NUM);
-    }
-    bool is_allone(expr const * e) const;
-    bool is_zero(expr const * e) const;
-    bool is_bv_sort(sort const * s) const;
-    bool is_bv(expr const* e) const {
-        return is_bv_sort(m_manager.get_sort(e));
-    }
     
     unsigned get_bv_size(sort const * s) const { 
         SASSERT(is_bv_sort(s));
@@ -348,59 +387,6 @@ public:
     app * mk_bvumul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_NO_OVFL, n, m); }
 
     app * mk_bv(unsigned n, expr* const* es) { return m_manager.mk_app(get_fid(), OP_MKBV, n, es); }
-
-    bool is_concat(expr const * e) const { return is_app_of(e, get_fid(), OP_CONCAT); }
-    bool is_extract(func_decl const * f) const { return is_decl_of(f, get_fid(), OP_EXTRACT); }
-    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) {
-        if (!is_extract(e)) return false;
-        low = get_extract_low(e);
-        high = get_extract_high(e);
-        b = to_app(e)->get_arg(0);
-        return true;
-    }
-    bool is_bv2int(expr const* e, expr*& r) {
-        if (!is_bv2int(e)) return false;
-        r = to_app(e)->get_arg(0);
-        return true;
-    }
-    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); }
-    bool is_bv_neg(expr const * e) const { return is_app_of(e, get_fid(), OP_BNEG); }
-    bool is_bv_sdiv(expr const * e) const { return is_app_of(e, get_fid(), OP_BSDIV); }
-    bool is_bv_udiv(expr const * e) const { return is_app_of(e, get_fid(), OP_BUDIV); }
-    bool is_bv_srem(expr const * e) const { return is_app_of(e, get_fid(), OP_BSREM); }
-    bool is_bv_urem(expr const * e) const { return is_app_of(e, get_fid(), OP_BUREM); }
-    bool is_bv_smod(expr const * e) const { return is_app_of(e, get_fid(), OP_BSMOD); }
-    bool is_bv_and(expr const * e) const { return is_app_of(e, get_fid(), OP_BAND); }
-    bool is_bv_or(expr const * e) const { return is_app_of(e, get_fid(), OP_BOR); }
-    bool is_bv_xor(expr const * e) const { return is_app_of(e, get_fid(), OP_BXOR); }
-    bool is_bv_nand(expr const * e) const { return is_app_of(e, get_fid(), OP_BNAND); }
-    bool is_bv_nor(expr const * e) const { return is_app_of(e, get_fid(), OP_BNOR); }
-    bool is_bv_not(expr const * e) const { return is_app_of(e, get_fid(), OP_BNOT); }
-    bool is_bv_ule(expr const * e) const { return is_app_of(e, get_fid(), OP_ULEQ); }
-    bool is_bv_sle(expr const * e) const { return is_app_of(e, get_fid(), OP_SLEQ); }
-    bool is_bit2bool(expr const * e) const { return is_app_of(e, get_fid(), OP_BIT2BOOL); }
-    bool is_bv2int(expr const* e) const { return is_app_of(e, get_fid(), OP_BV2INT); }
-    bool is_int2bv(expr const* e) const { return is_app_of(e, get_fid(), OP_INT2BV); }
-    bool is_mkbv(expr const * e) const { return is_app_of(e, get_fid(), OP_MKBV); }
-    bool is_bv_ashr(expr const * e) const { return is_app_of(e, get_fid(), OP_BASHR); }
-    bool is_bv_lshr(expr const * e) const { return is_app_of(e, get_fid(), OP_BLSHR); }
-    bool is_bv_shl(expr const * e) const { return is_app_of(e, get_fid(), OP_BSHL); }
-    bool is_sign_ext(expr const * e) const { return is_app_of(e, get_fid(), OP_SIGN_EXT); }
-
-    MATCH_BINARY(is_bv_add);
-    MATCH_BINARY(is_bv_mul);
-    MATCH_BINARY(is_bv_sle);
-    MATCH_BINARY(is_bv_ule);
-    MATCH_BINARY(is_bv_shl);
-
-    bool mult_inverse(rational const & n, unsigned bv_size, rational & result);
 };
     
 #endif /* _BV_DECL_PLUGIN_H_ */
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster.h b/src/ast/rewriter/bit_blaster/bit_blaster.h
index 42444aebc..7b317c6cb 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster.h
@@ -36,7 +36,7 @@ public:
     bit_blaster_cfg(bv_util & u, bit_blaster_params const & p, basic_simplifier_plugin & _s);
 
     ast_manager & m() const { return m_util.get_manager(); }
-    numeral power(unsigned n) const { return m_util.power_of_two(n); }
+    numeral power(unsigned n) const { return rational::power_of_two(n); }
     void mk_xor(expr * a, expr * b, expr_ref & r) { s.mk_xor(a, b, r); }
     void mk_xor3(expr * a, expr * b, expr * c, expr_ref & r);
     void mk_carry(expr * a, expr * b, expr * c, expr_ref & r);
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
index 1fd83e91f..80d319377 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
@@ -32,7 +32,7 @@ struct blaster_cfg {
     blaster_cfg(bool_rewriter & r, bv_util & u):m_rewriter(r), m_util(u) {}
     
     ast_manager & m() const { return m_util.get_manager(); }
-    numeral power(unsigned n) const { return m_util.power_of_two(n); }
+    numeral power(unsigned n) const { return rational::power_of_two(n); }
     void mk_xor(expr * a, expr * b, expr_ref & r) { m_rewriter.mk_xor(a, b, r); }
     void mk_xor3(expr * a, expr * b, expr * c, expr_ref & r) {
         expr_ref tmp(m());
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 5fd562676..f8ff27337 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -283,12 +283,12 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
 
     if (is_num1 || is_num2) {
         if (is_signed) {
-            lower = - m_util.power_of_two(sz - 1);
-            upper =   m_util.power_of_two(sz - 1) - numeral(1);
+            lower = - rational::power_of_two(sz - 1);
+            upper =   rational::power_of_two(sz - 1) - numeral(1);
         }
         else {
             lower = numeral(0);
-            upper = m_util.power_of_two(sz) - numeral(1);
+            upper = rational::power_of_two(sz) - numeral(1);
         }
     }
 
@@ -387,14 +387,14 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_
     if (is_numeral(arg, v, sz)) {
         sz = high - low + 1;
         if (v.is_neg())
-            mod(v, m_util.power_of_two(sz), v);
+            mod(v, rational::power_of_two(sz), v);
         if (v.is_uint64()) {
             uint64 u  = v.get_uint64();
             uint64 e  = shift_right(u, low) & (shift_left(1ull, sz) - 1ull);
             result    = mk_numeral(numeral(e, numeral::ui64()), sz);
             return BR_DONE;
         }
-        div(v, m_util.power_of_two(low), v);
+        div(v, rational::power_of_two(low), v);
         result = mk_numeral(v, sz);
         return BR_DONE;
     }
@@ -519,7 +519,7 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) {
             
             SASSERT(r2 < numeral(bv_size));
             SASSERT(r2.is_unsigned());
-            r1 = m_util.norm(r1 * m_util.power_of_two(r2.get_unsigned()), bv_size);
+            r1 = m_util.norm(r1 * rational::power_of_two(r2.get_unsigned()), bv_size);
             result = mk_numeral(r1, bv_size);
             return BR_DONE;
         }
@@ -567,7 +567,7 @@ br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) {
 
             SASSERT(r2.is_unsigned());
             unsigned sh = r2.get_unsigned();
-            div(r1, m_util.power_of_two(sh), r1);
+            div(r1, rational::power_of_two(sh), r1);
             result = mk_numeral(r1, bv_size);
             return BR_DONE;
         }
@@ -626,7 +626,7 @@ br_status bv_rewriter::mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result) {
 
     if (is_num1 && is_num2 && numeral(bv_size) <= r2) {
         if (m_util.has_sign_bit(r1, bv_size))
-            result = mk_numeral(m_util.power_of_two(bv_size) - numeral(1), bv_size);
+            result = mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size);
         else
             result = mk_numeral(0, bv_size);
         return BR_DONE;
@@ -635,7 +635,7 @@ br_status bv_rewriter::mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result) {
     if (is_num1 && is_num2) {
         SASSERT(r2 < numeral(bv_size));
         bool   sign = m_util.has_sign_bit(r1, bv_size);
-        div(r1, m_util.power_of_two(r2.get_unsigned()), r1);
+        div(r1, rational::power_of_two(r2.get_unsigned()), r1);
         if (sign) {
             // pad ones.
             numeral p(1);
@@ -697,7 +697,7 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e
                 // The "hardware interpretation" for (bvsdiv x 0) is (ite (bvslt x #x0000) #x0001 #xffff)
                 result = m().mk_ite(m().mk_app(get_fid(), OP_SLT, arg1, mk_numeral(0, bv_size)),
                                     mk_numeral(1, bv_size),
-                                    mk_numeral(m_util.power_of_two(bv_size) - numeral(1), bv_size));
+                                    mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size));
                 return BR_REWRITE2;
             }
         }
@@ -746,7 +746,7 @@ br_status bv_rewriter::mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, e
             }
             else {
                 // The "hardware interpretation" for (bvudiv x 0) is #xffff
-                result = mk_numeral(m_util.power_of_two(bv_size) - numeral(1), bv_size);
+                result = mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size);
                 return BR_DONE;
                 
             }
@@ -845,7 +845,7 @@ bool bv_rewriter::is_minus_one_core(expr * arg) const {
     numeral r;
     unsigned bv_size;
     if (is_numeral(arg, r, bv_size)) {
-        return r == (m_util.power_of_two(bv_size) - numeral(1));
+        return r == (rational::power_of_two(bv_size) - numeral(1));
     }
     return false;
 }
@@ -924,7 +924,7 @@ br_status bv_rewriter::mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, e
         if (is_x_minus_one(arg1, x) && x == arg2) {
             bv_size = get_bv_size(arg1);
             expr * x_minus_1 = arg1;
-            expr * minus_one = mk_numeral(m_util.power_of_two(bv_size) - numeral(1), bv_size);
+            expr * minus_one = mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size);
             result = m().mk_ite(m().mk_eq(x, mk_numeral(0, bv_size)),
                                 m().mk_app(get_fid(), OP_BUREM0, minus_one),
                                 x_minus_1);
@@ -1068,7 +1068,7 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
         if (i > 0) 
             prev = new_args.back();
         if (is_numeral(arg, v1, sz1) && prev != 0 && is_numeral(prev, v2, sz2)) {
-            v2  *= m_util.power_of_two(sz1);
+            v2  *= rational::power_of_two(sz1);
             v2  += v1;
             new_args.pop_back();
             new_args.push_back(mk_numeral(v2, sz1+sz2));
@@ -1137,7 +1137,7 @@ br_status bv_rewriter::mk_sign_extend(unsigned n, expr * arg, expr_ref & result)
     if (is_numeral(arg, r, bv_size)) {
         unsigned result_bv_size = bv_size + n;
         r = m_util.norm(r, bv_size, true);
-        mod(r, m_util.power_of_two(result_bv_size), r);
+        mod(r, rational::power_of_two(result_bv_size), r);
         result = mk_numeral(r, result_bv_size);
         return BR_DONE;
     }
@@ -1213,7 +1213,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
         if (m_util.is_bv_not(arg)) {
             expr * atom = to_app(arg)->get_arg(0);
             if (pos_args.is_marked(atom)) {
-                result = mk_numeral(m_util.power_of_two(sz) - numeral(1), sz);
+                result = mk_numeral(rational::power_of_two(sz) - numeral(1), sz);
                 return BR_DONE;
             }
             else if (neg_args.is_marked(atom)) {
@@ -1229,7 +1229,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
                 continue;
             }
             else if (neg_args.is_marked(arg)) {
-                result = mk_numeral(m_util.power_of_two(sz) - numeral(1), sz);
+                result = mk_numeral(rational::power_of_two(sz) - numeral(1), sz);
                 return BR_DONE;
             }
             pos_args.mark(arg, true);
@@ -1237,7 +1237,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
         }
     }
 
-    if (v1 == m_util.power_of_two(sz) - numeral(1)) {
+    if (v1 == rational::power_of_two(sz) - numeral(1)) {
         result = mk_numeral(v1, sz);
         return BR_DONE;
     }
@@ -1294,7 +1294,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
             }
             if (i != low) {
                 unsigned num_sz = i - low;
-                exs.push_back(m_util.mk_numeral(m_util.power_of_two(num_sz) - numeral(1), num_sz));
+                exs.push_back(m_util.mk_numeral(rational::power_of_two(num_sz) - numeral(1), num_sz));
                 low = i;
             }
             while (i < sz && mod(v1, two).is_zero()) {
@@ -1385,7 +1385,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
             else if (pos_args.is_marked(atom)) {
                 pos_args.mark(atom, false);
                 merged = true;
-                v1 = bitwise_xor(v1, m_util.power_of_two(sz) - numeral(1));
+                v1 = bitwise_xor(v1, rational::power_of_two(sz) - numeral(1));
             }
             else {
                 neg_args.mark(atom, true);
@@ -1399,7 +1399,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
             else if (neg_args.is_marked(arg)) {
                 neg_args.mark(arg, false);
                 merged = true;
-                v1 = bitwise_xor(v1, m_util.power_of_two(sz) - numeral(1));
+                v1 = bitwise_xor(v1, rational::power_of_two(sz) - numeral(1));
             }
             else {
                 pos_args.mark(arg, true);
@@ -1455,7 +1455,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
         return BR_REWRITE3;
     } 
 
-    if (!merged && !flattened && (num_coeffs == 0 || (num_coeffs == 1 && !v1.is_zero() && v1 != (m_util.power_of_two(sz) - numeral(1)))))
+    if (!merged && !flattened && (num_coeffs == 0 || (num_coeffs == 1 && !v1.is_zero() && v1 != (rational::power_of_two(sz) - numeral(1)))))
         return BR_FAILED;
 
     ptr_buffer<expr> new_args;
@@ -1611,7 +1611,7 @@ br_status bv_rewriter::mk_bv_redand(expr * arg, expr_ref & result) {
     numeral r;
     unsigned bv_size;
     if (is_numeral(arg, r, bv_size)) {
-        result = (r == m_util.power_of_two(bv_size) - numeral(1)) ? mk_numeral(1, 1) : mk_numeral(0, 1);
+        result = (r == rational::power_of_two(bv_size) - numeral(1)) ? mk_numeral(1, 1) : mk_numeral(0, 1);
         return BR_DONE;
     }
     return BR_FAILED;
@@ -1707,7 +1707,7 @@ bool bv_rewriter::is_zero_bit(expr * x, unsigned idx) {
     if (is_numeral(x, val, bv_size)) {
         if (val.is_zero())
             return true;
-        div(val, m_util.power_of_two(idx), val);
+        div(val, rational::power_of_two(idx), val);
         return (val % numeral(2)).is_zero();
     }
     if (m_util.is_concat(x)) {
diff --git a/src/ast/simplifier/bv_simplifier_plugin.cpp b/src/ast/simplifier/bv_simplifier_plugin.cpp
index 2da1f3bab..3ef55baba 100644
--- a/src/ast/simplifier/bv_simplifier_plugin.cpp
+++ b/src/ast/simplifier/bv_simplifier_plugin.cpp
@@ -76,9 +76,9 @@ app * bv_simplifier_plugin::mk_numeral(numeral const & n) {
 }
 
 app * bv_simplifier_plugin::mk_numeral(numeral const& n, unsigned bv_size) {
-    numeral r = mod(n, m_util.power_of_two(bv_size));
+    numeral r = mod(n, rational::power_of_two(bv_size));
     SASSERT(!r.is_neg());
-    SASSERT(r < m_util.power_of_two(bv_size));
+    SASSERT(r < rational::power_of_two(bv_size));
     return m_util.mk_numeral(r, bv_size);
 }
 
@@ -225,7 +225,7 @@ inline uint64 bv_simplifier_plugin::to_uint64(const numeral & n, unsigned bv_siz
     SASSERT(bv_size <= 64);
     numeral tmp = n;
     if (tmp.is_neg()) {
-        tmp = mod(tmp, m_util.power_of_two(bv_size));
+        tmp = mod(tmp, rational::power_of_two(bv_size));
     }
     SASSERT(tmp.is_nonneg());
     SASSERT(tmp.is_uint64());
@@ -235,7 +235,7 @@ inline uint64 bv_simplifier_plugin::to_uint64(const numeral & n, unsigned bv_siz
 #define MK_BV_OP(_oper_,_binop_) \
 rational bv_simplifier_plugin::mk_bv_ ## _oper_(numeral const& a0, numeral const& b0, unsigned sz) { \
     rational r(0), a(a0), b(b0); \
-    numeral p64 = m_util.power_of_two(64); \
+    numeral p64 = rational::power_of_two(64); \
     numeral mul(1); \
     while (sz > 0) { \
         numeral a1 = a % p64; \
@@ -260,7 +260,7 @@ MK_BV_OP(xor,^)
 
 rational bv_simplifier_plugin::mk_bv_not(numeral const& a0, unsigned sz) { 
     rational r(0), a(a0), mul(1);
-    numeral p64 = m_util.power_of_two(64); 
+    numeral p64 = rational::power_of_two(64); 
     while (sz > 0) { 
         numeral a1 = a % p64; 
         uint64 u = ~a1.get_uint64();
@@ -320,12 +320,12 @@ void bv_simplifier_plugin::mk_leq_core(bool is_signed, expr * arg1, expr * arg2,
 
     if (is_num1 || is_num2) {
         if (is_signed) {
-            lower = - m_util.power_of_two(bv_size - 1);
-            upper =   m_util.power_of_two(bv_size - 1) - numeral(1);
+            lower = - rational::power_of_two(bv_size - 1);
+            upper =   rational::power_of_two(bv_size - 1) - numeral(1);
         }
         else {
             lower = numeral(0);
-            upper = m_util.power_of_two(bv_size) - numeral(1);
+            upper = rational::power_of_two(bv_size) - numeral(1);
         }
     }
 
@@ -509,7 +509,7 @@ bool bv_simplifier_plugin::try_mk_extract(unsigned high, unsigned low, expr * ar
 
     if (m_util.is_numeral(a, r, num_bits)) {
         if (r.is_neg()) {
-            r = mod(r, m_util.power_of_two(sz));
+            r = mod(r, rational::power_of_two(sz));
         }
         SASSERT(r.is_nonneg());
         if (r.is_uint64()) {
@@ -520,7 +520,7 @@ bool bv_simplifier_plugin::try_mk_extract(unsigned high, unsigned low, expr * ar
             result = mk_numeral(numeral(e, numeral::ui64()), sz);
             return true;
         }
-        result = mk_numeral(div(r, m_util.power_of_two(low)), sz);
+        result = mk_numeral(div(r, rational::power_of_two(low)), sz);
         return true;
     }
     // (extract[high:low] (extract[high2:low2] x)) == (extract[high+low2 : low+low2] x)
@@ -902,7 +902,7 @@ void bv_simplifier_plugin::mk_concat(unsigned num_args, expr * const * args, exp
         --i;
         expr * arg   = args[i];
         if (is_numeral(arg, arg_val)) {
-            arg_val    *= m_util.power_of_two(shift);
+            arg_val    *= rational::power_of_two(shift);
             val        += arg_val;
             shift      += get_bv_size(arg);
             TRACE("bv_simplifier_plugin", 
@@ -1203,7 +1203,7 @@ bool bv_simplifier_plugin::is_minus_one_core(expr * arg) const {
     unsigned bv_size;
     if (m_util.is_numeral(arg, r, bv_size)) {
         numeral minus_one(-1);
-        minus_one = mod(minus_one, m_util.power_of_two(bv_size));
+        minus_one = mod(minus_one, rational::power_of_two(bv_size));
         return r == minus_one;
     }
     return false;
@@ -1295,7 +1295,7 @@ void bv_simplifier_plugin::mk_sign_extend(unsigned n, expr * arg, expr_ref & res
     if (m_util.is_numeral(arg, r, bv_size)) {
         unsigned result_bv_size = bv_size + n;
         r = norm(r, bv_size, true);
-        r = mod(r, m_util.power_of_two(result_bv_size));
+        r = mod(r, rational::power_of_two(result_bv_size));
         result = mk_numeral(r, result_bv_size);
         TRACE("mk_sign_extend", tout << "n: " << n << "\n"; 
               ast_ll_pp(tout, m_manager, arg); tout << "====>\n"; 
@@ -1373,7 +1373,7 @@ void bv_simplifier_plugin::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result
     else if (is_num1 && is_num2) {
         SASSERT(r2 < rational(bv_size));
         SASSERT(r2.is_unsigned());
-        result = mk_numeral(r1 * m_util.power_of_two(r2.get_unsigned()), bv_size);
+        result = mk_numeral(r1 * rational::power_of_two(r2.get_unsigned()), bv_size);
     }
 
     //
@@ -1423,7 +1423,7 @@ void bv_simplifier_plugin::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & resul
     else if (is_num1 && is_num2) {
         SASSERT(r2.is_unsigned());
         unsigned sh = r2.get_unsigned();
-        r1 = div(r1, m_util.power_of_two(sh));
+        r1 = div(r1, rational::power_of_two(sh));
         result = mk_numeral(r1, bv_size);
     }
     //
@@ -1804,8 +1804,8 @@ void bv_simplifier_plugin::mk_bv_rotate_left_core(unsigned shift, numeral r, uns
         result = mk_numeral(r, bv_size);        
     }
     else {
-        rational r1 = div(r, m_util.power_of_two(bv_size - shift)); // shift right
-        rational r2 = (r * m_util.power_of_two(shift)) % m_util.power_of_two(bv_size); // shift left
+        rational r1 = div(r, rational::power_of_two(bv_size - shift)); // shift right
+        rational r2 = (r * rational::power_of_two(shift)) % rational::power_of_two(bv_size); // shift left
         result = mk_numeral(r1 + r2, bv_size);
     }
 }
@@ -1831,8 +1831,8 @@ void bv_simplifier_plugin::mk_bv_rotate_right_core(unsigned shift, numeral r, un
         result = mk_numeral(r, bv_size);
     }
     else {
-        rational r1 = div(r, m_util.power_of_two(shift)); // shift right
-        rational r2 = (r * m_util.power_of_two(bv_size - shift)) % m_util.power_of_two(bv_size); // shift left
+        rational r1 = div(r, rational::power_of_two(shift)); // shift right
+        rational r2 = (r * rational::power_of_two(bv_size - shift)) % rational::power_of_two(bv_size); // shift left
         result = mk_numeral(r1 + r2, bv_size);            
     }
 }
@@ -1935,7 +1935,7 @@ void bv_simplifier_plugin::mk_bv_ashr(expr* arg1, expr* arg2, expr_ref& result)
     else if (is_num1 && is_num2) {
         SASSERT(r2 < rational(bv_size));
         bool   sign = has_sign_bit(r1, bv_size);
-        r1 = div(r1, m_util.power_of_two(r2.get_unsigned()));
+        r1 = div(r1, rational::power_of_two(r2.get_unsigned()));
         if (sign) {
             // pad ones.
             rational p(1);
diff --git a/src/ast/simplifier/bv_simplifier_plugin.h b/src/ast/simplifier/bv_simplifier_plugin.h
index 7f66566b6..36e773de0 100644
--- a/src/ast/simplifier/bv_simplifier_plugin.h
+++ b/src/ast/simplifier/bv_simplifier_plugin.h
@@ -172,7 +172,7 @@ public:
     app * mk_numeral(rational const & n, unsigned bv_size);
     app * mk_numeral(uint64 n, unsigned bv_size) { return mk_numeral(numeral(n, numeral::ui64()), bv_size); }
     app* mk_bv0(unsigned bv_size) { return m_util.mk_numeral(numeral(0), bv_size); }
-    rational mk_allone(unsigned bv_size) { return m_util.power_of_two(bv_size) - numeral(1); }
+    rational mk_allone(unsigned bv_size) { return rational::power_of_two(bv_size) - numeral(1); }
     bool is_minus_one_core(expr * arg) const;
     bool is_x_minus_one(expr * arg, expr * & x);
     void mk_int2bv(expr * arg, sort* range, expr_ref & result);
diff --git a/src/tactic/arith/bv2int_rewriter.cpp b/src/tactic/arith/bv2int_rewriter.cpp
index 0965f36f2..872981283 100644
--- a/src/tactic/arith/bv2int_rewriter.cpp
+++ b/src/tactic/arith/bv2int_rewriter.cpp
@@ -544,7 +544,7 @@ bool bv2int_rewriter::is_sbv2int(expr* n, expr_ref& s) {
         m_bv.is_extract(e2, lo1, hi1, e3) &&
         lo1 == 0 && hi1 == hi-1 &&
         m_arith.is_numeral(t2, k, is_int) && is_int &&
-        k == m_bv.power_of_two(hi) 
+        k == rational::power_of_two(hi) 
         ) {
         s = e3;
         return true;
diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp
index 188ea7d70..bd5af58f2 100644
--- a/src/tactic/arith/nla2bv_tactic.cpp
+++ b/src/tactic/arith/nla2bv_tactic.cpp
@@ -253,7 +253,7 @@ class nla2bv_tactic : public tactic {
                 s_bv = m_arith.mk_sub(m_arith.mk_numeral(*up, true), s_bv);
             }
             else {
-                s_bv = m_arith.mk_sub(s_bv, m_arith.mk_numeral(m_bv.power_of_two(num_bits-1), true));
+                s_bv = m_arith.mk_sub(s_bv, m_arith.mk_numeral(rational::power_of_two(num_bits-1), true));
             }
             
             m_trail.push_back(s_bv);
diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp
index 8790ca5a7..83a949579 100644
--- a/src/tactic/arith/pb2bv_tactic.cpp
+++ b/src/tactic/arith/pb2bv_tactic.cpp
@@ -583,7 +583,7 @@ private:
                 return false; // size must be even
             // I implemented only the easy (and very common) case, where a_i = 2^{n-i-1} and c = 2^n - 1
             unsigned n = sz/2;
-            if (c != m_bv_util.power_of_two(n) - numeral(1))
+            if (c != rational::power_of_two(n) - numeral(1))
                 return false;
             for (unsigned i = 0; i < n; i++) {
                 monomial const & m1 = p[i*2];
@@ -592,7 +592,7 @@ private:
                     return false;
                 if (m1.m_a != m2.m_a)
                     return false;
-                if (m1.m_a != m_bv_util.power_of_two(n - i - 1))
+                if (m1.m_a != rational::power_of_two(n - i - 1))
                     return false;
             }
             return true;
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index d1dca296a..00e14a41f 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -647,9 +647,9 @@ class elim_uncnstr_tactic : public tactic {
                     unsigned bv_sz = m_bv_util.get_bv_size(arg1);
                     rational MAX;
                     if (is_signed)
-                        MAX = m_bv_util.power_of_two(bv_sz - 1) - rational(1);
+                        MAX = rational::power_of_two(bv_sz - 1) - rational(1);
                     else
-                        MAX = m_bv_util.power_of_two(bv_sz) - rational(1);
+                        MAX = rational::power_of_two(bv_sz) - rational(1);
                     app * u;
                     bool is_new = mk_fresh_uncnstr_var_for(f, arg1, arg2, u);
                     app * r = m().mk_or(u, m().mk_eq(t, m_bv_util.mk_numeral(MAX, bv_sz)));
@@ -666,7 +666,7 @@ class elim_uncnstr_tactic : public tactic {
                     unsigned bv_sz = m_bv_util.get_bv_size(arg1);
                     rational MIN;
                     if (is_signed)
-                        MIN = -m_bv_util.power_of_two(bv_sz - 1);
+                        MIN = -rational::power_of_two(bv_sz - 1);
                     else
                         MIN = rational(0);
                     app * u;
diff --git a/src/util/rational.cpp b/src/util/rational.cpp
index 0a91bd8da..122db7217 100644
--- a/src/util/rational.cpp
+++ b/src/util/rational.cpp
@@ -27,6 +27,31 @@ synch_mpq_manager *  rational::g_mpq_manager = 0;
 rational             rational::m_zero(0);
 rational             rational::m_one(1);
 rational             rational::m_minus_one(-1);
+vector<rational>     rational::m_powers_of_two;
+
+void mk_power_up_to(vector<rational> & pws, unsigned n) {
+    if (pws.empty()) {
+        pws.push_back(rational(1));
+    }
+    unsigned sz = pws.size();
+    rational curr = pws[sz - 1];
+    rational two(2);
+    for (unsigned i = sz; i <= n; i++) {
+        curr *= two;
+        pws.push_back(curr);
+    }
+}
+
+rational rational::power_of_two(unsigned k) {
+    rational result;
+    #pragma omp critical (powers_of_two)
+    {
+        if (k >= m_powers_of_two.size())
+            mk_power_up_to(m_powers_of_two, k+1);
+        result = m_powers_of_two[k];
+    }
+    return result;
+}
 
 void rational::initialize() {
     if (!g_mpq_manager) {
@@ -35,6 +60,7 @@ void rational::initialize() {
 }
 
 void rational::finalize() {
+    m_powers_of_two.finalize();
     dealloc(g_mpq_manager);
     g_mpq_manager = 0;
 }
diff --git a/src/util/rational.h b/src/util/rational.h
index f0406f30a..fc03228bf 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -26,14 +26,13 @@ class rational {
     static rational                  m_zero;
     static rational                  m_one;
     static rational                  m_minus_one;
-
+    static vector<rational>          m_powers_of_two;
     static synch_mpq_manager *       g_mpq_manager;
-
+    
     static synch_mpq_manager & m() { return *g_mpq_manager; }
 
 public:
     static void initialize();
-
     static void finalize();
     /*
       ADD_INITIALIZER('rational::initialize();')
@@ -272,6 +271,8 @@ public:
         return result;
     }
 
+    static rational power_of_two(unsigned k);
+
     bool is_power_of_two(unsigned & shift) {
         return m().is_power_of_two(m_val, shift);
     }