diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index d7cb5f10d..24d7f80dd 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -1257,7 +1257,8 @@ extern "C" {
             case OP_EXT_ROTATE_LEFT:  return Z3_OP_EXT_ROTATE_LEFT;
             case OP_EXT_ROTATE_RIGHT: return Z3_OP_EXT_ROTATE_RIGHT;
             case OP_INT2BV:    return Z3_OP_INT2BV;
-            case OP_BV2INT:    return Z3_OP_BV2INT;
+            case OP_UBV2INT:    return Z3_OP_BV2INT;
+            case OP_SBV2INT:    return Z3_OP_SBV2INT;
             case OP_CARRY:     return Z3_OP_CARRY;
             case OP_XOR3:      return Z3_OP_XOR3;
             case OP_BIT2BOOL: return Z3_OP_BIT2BOOL;
diff --git a/src/api/api_bv.cpp b/src/api/api_bv.cpp
index 3ea5ba918..5b627944c 100644
--- a/src/api/api_bv.cpp
+++ b/src/api/api_bv.cpp
@@ -140,7 +140,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) {                \
         else {
             expr * _n = to_expr(n);
             parameter p(to_sort(int_s));
-            ast* a = mk_c(c)->m().mk_app(mk_c(c)->get_bv_fid(), OP_BV2INT, 1, &p, 1, &_n);
+            ast* a = mk_c(c)->m().mk_app(mk_c(c)->get_bv_fid(), OP_UBV2INT, 1, &p, 1, &_n);
             mk_c(c)->save_ast_trail(a);
             check_sorts(c, a);
             RETURN_Z3(of_ast(a));
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 8c83cc1a4..ca2f4f283 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -367,13 +367,11 @@ typedef enum
 
    - Z3_OP_EXT_ROTATE_RIGHT (extended) Right rotation. Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one.
 
-   - Z3_OP_INT2BV Coerce integer to bit-vector. NB. This function
-       is not supported by the decision procedures. Only the most
-       rudimentary simplification rules are applied to this function.
+   - Z3_OP_INT2BV Coerce integer to bit-vector. 
 
-   - Z3_OP_BV2INT Coerce bit-vector to integer. NB. This function
-       is not supported by the decision procedures. Only the most
-       rudimentary simplification rules are applied to this function.
+   - Z3_OP_BV2INT Coerce bit-vector to integer. 
+
+   - Z3_OP_SBV2INT Coerce signed bit-vector to integer. 
 
    - Z3_OP_CARRY Compute the carry bit in a full-adder.
        The meaning is given by the equivalence
@@ -1106,6 +1104,7 @@ typedef enum {
     Z3_OP_BIT2BOOL,
     Z3_OP_INT2BV,
     Z3_OP_BV2INT,
+    Z3_OP_SBV2INT,
     Z3_OP_CARRY,
     Z3_OP_XOR3,
 
diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index 7c317970c..ef15935e9 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -143,7 +143,8 @@ void bv_decl_plugin::finalize() {
     DEC_REF(m_ext_rotate_right);
 
     DEC_REF(m_int2bv);
-    DEC_REF(m_bv2int);
+    DEC_REF(m_ubv2int);
+    DEC_REF(m_sbv2int);
     for (auto& ds : m_bit2bool)
         DEC_REF(ds);
     DEC_REF(m_mkbv);
@@ -228,13 +229,13 @@ func_decl * bv_decl_plugin::mk_int2bv(unsigned bv_size, unsigned num_parameters,
     force_ptr_array_size(m_int2bv, bv_size + 1);
 
     if (arity != 1) {
-        m_manager->raise_exception("expecting one argument to int2bv");
+        m_manager->raise_exception("expecting one argument to int_to_bv");
         return nullptr;
     }
 
     if (m_int2bv[bv_size] == 0) {
         sort * s = get_bv_sort(bv_size);
-        m_int2bv[bv_size] = m_manager->mk_func_decl(symbol("int2bv"), domain[0], s,
+        m_int2bv[bv_size] = m_manager->mk_func_decl(symbol("int_to_bv"), domain[0], s,
                                                     func_decl_info(m_family_id, OP_INT2BV, num_parameters, parameters));
         m_manager->inc_ref(m_int2bv[bv_size]);
     }
@@ -242,22 +243,40 @@ func_decl * bv_decl_plugin::mk_int2bv(unsigned bv_size, unsigned num_parameters,
     return m_int2bv[bv_size];
 }
 
-func_decl * bv_decl_plugin::mk_bv2int(unsigned bv_size, unsigned num_parameters, parameter const * parameters,
+func_decl * bv_decl_plugin::mk_ubv2int(unsigned bv_size, unsigned num_parameters, parameter const * parameters,
                                     unsigned arity, sort * const * domain) {
-    force_ptr_array_size(m_bv2int, bv_size + 1);
+    force_ptr_array_size(m_ubv2int, bv_size + 1);
 
     if (arity != 1) {
-        m_manager->raise_exception("expecting one argument to bv2int");
+        m_manager->raise_exception("expecting one argument to ubv_to_int");
         return nullptr;
     }
 
-    if (m_bv2int[bv_size] == 0) {
-        m_bv2int[bv_size] = m_manager->mk_func_decl(symbol("bv2int"), domain[0], m_int_sort,
-                                                    func_decl_info(m_family_id, OP_BV2INT));
-        m_manager->inc_ref(m_bv2int[bv_size]);
+    if (m_ubv2int[bv_size] == 0) {
+        m_ubv2int[bv_size] = m_manager->mk_func_decl(symbol("ubv_to_int"), domain[0], m_int_sort,
+                                                     func_decl_info(m_family_id, OP_UBV2INT));
+        m_manager->inc_ref(m_ubv2int[bv_size]);
     }
 
-    return m_bv2int[bv_size];
+    return m_ubv2int[bv_size];
+}
+
+func_decl * bv_decl_plugin::mk_sbv2int(unsigned bv_size, unsigned num_parameters, parameter const * parameters,
+                                    unsigned arity, sort * const * domain) {
+    force_ptr_array_size(m_sbv2int, bv_size + 1);
+
+    if (arity != 1) {
+        m_manager->raise_exception("expecting one argument to sbv_to_int");
+        return nullptr;
+    }
+
+    if (m_sbv2int[bv_size] == 0) {
+        m_sbv2int[bv_size] = m_manager->mk_func_decl(symbol("sbv_to_int"), domain[0], m_int_sort,
+                                                    func_decl_info(m_family_id, OP_SBV2INT));
+        m_manager->inc_ref(m_sbv2int[bv_size]);
+    }
+
+    return m_sbv2int[bv_size];
 }
 
 func_decl * bv_decl_plugin::mk_unary_pred(ptr_vector<func_decl> & decls, decl_kind k, char const * name, unsigned bv_size) {
@@ -552,8 +571,10 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
         return mk_bit2bool(bv_size, num_parameters, parameters, arity, domain);
     case OP_INT2BV:
         return mk_int2bv(bv_size, num_parameters, parameters, arity, domain);
-    case OP_BV2INT:
-        return mk_bv2int(bv_size, num_parameters, parameters, arity, domain);
+    case OP_UBV2INT:
+        return mk_ubv2int(bv_size, num_parameters, parameters, arity, domain);
+    case OP_SBV2INT:
+        return mk_sbv2int(bv_size, num_parameters, parameters, arity, domain);
     case OP_CONCAT:
         if (!get_concat_size(arity, domain, r_size))
             m_manager->raise_exception("invalid concat application");
@@ -780,8 +801,11 @@ void bv_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
         op_names.push_back(builtin_name("ext_rotate_left",OP_EXT_ROTATE_LEFT));
         op_names.push_back(builtin_name("ext_rotate_right",OP_EXT_ROTATE_RIGHT));
         op_names.push_back(builtin_name("int2bv",OP_INT2BV));
-        op_names.push_back(builtin_name("bv2int",OP_BV2INT));
-        op_names.push_back(builtin_name("bv2nat",OP_BV2INT));
+        op_names.push_back(builtin_name("int_to_bv",OP_INT2BV));
+        op_names.push_back(builtin_name("bv2int",OP_UBV2INT));
+        op_names.push_back(builtin_name("bv2nat",OP_UBV2INT));
+        op_names.push_back(builtin_name("ubv_to_int",OP_UBV2INT));
+        op_names.push_back(builtin_name("sbv_to_int",OP_SBV2INT));
         op_names.push_back(builtin_name("mkbv",OP_MKBV));
     }
 }
@@ -878,10 +902,8 @@ bool bv_recognizers::is_repeat(expr const * e, expr*& arg, unsigned& n) const {
 }
 
 
-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;
+bool bv_recognizers::is_ubv2int(expr const* e, expr*& r) const {
+    return is_ubv2int(e) && (r = to_app(e)->get_arg(0), true);
 }
 
 bool bv_recognizers::is_bit2bool(expr* e, expr*& bv, unsigned& idx) const {
@@ -934,10 +956,28 @@ unsigned bv_util::get_int2bv_size(parameter const& p) {
     return static_cast<unsigned>(sz);
 }
 
-app * bv_util::mk_bv2int(expr* e) const {
+app * bv_util::mk_ubv2int(expr* e) const {
     sort* s = m_manager.mk_sort(m_manager.mk_family_id("arith"), INT_SORT);
     parameter p(s);
-    return m_manager.mk_app(get_fid(), OP_BV2INT, 1, &p, 1, &e);
+    return m_manager.mk_app(get_fid(), OP_UBV2INT, 1, &p, 1, &e);
+}
+
+app * bv_util::mk_sbv2int(expr* e) const {
+    sort* s = m_manager.mk_sort(m_manager.mk_family_id("arith"), INT_SORT);
+    parameter p(s);
+    return m_manager.mk_app(get_fid(), OP_SBV2INT, 1, &p, 1, &e);
+}
+
+app* bv_util::mk_sbv2int_as_ubv2int(expr* e) {
+    // if e <_s 0 then ubv2int(e) - 2^n else ubv2int(e)
+    app* r = mk_ubv2int(e);
+    arith_util autil(m_manager);
+    unsigned sz = get_bv_size(e);
+    expr_ref zero(mk_numeral(rational::zero(), sz), m_manager);
+    r = m_manager.mk_ite(mk_slt(e, zero),
+        autil.mk_sub(r, autil.mk_numeral(rational::power_of_two(sz), true)),
+        r);
+    return r;
 }
 
 app* bv_util::mk_int2bv(unsigned sz, expr* e) const {
diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index b8dde9361..916910087 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -109,7 +109,8 @@ enum bv_op_kind {
     OP_BIT2BOOL, // predicate
     OP_MKBV,     // bools to bv
     OP_INT2BV,
-    OP_BV2INT,
+    OP_UBV2INT,
+    OP_SBV2INT,
 
     OP_CARRY,
     OP_XOR3,
@@ -225,7 +226,8 @@ protected:
     ptr_vector<func_decl>  m_ext_rotate_left;
     ptr_vector<func_decl>  m_ext_rotate_right;
 
-    ptr_vector<func_decl>  m_bv2int;
+    ptr_vector<func_decl>  m_ubv2int;
+    ptr_vector<func_decl>  m_sbv2int;
     ptr_vector<func_decl>  m_int2bv;
     vector<ptr_vector<func_decl> > m_bit2bool;
     ptr_vector<func_decl>  m_mkbv;
@@ -250,7 +252,9 @@ protected:
     bool get_extract_size(unsigned num_parameters, parameter const * parameters,
                           unsigned arity, sort * const * domain, int & result);
 
-    func_decl * mk_bv2int(unsigned bv_size, unsigned num_parameters, parameter const * parameters,
+    func_decl * mk_ubv2int(unsigned bv_size, unsigned num_parameters, parameter const * parameters,
+                          unsigned arity, sort * const * domain);
+    func_decl * mk_sbv2int(unsigned bv_size, unsigned num_parameters, parameter const * parameters,
                           unsigned arity, sort * const * domain);
 
     func_decl * mk_int2bv(unsigned bv_size, unsigned num_parameters, parameter const * parameters,
@@ -337,7 +341,8 @@ public:
     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_repeat(expr const * e, expr*& arg, unsigned& n) const;
-    bool is_bv2int(expr const * e, expr * & r) const;
+    bool is_ubv2int(expr const * e, expr * & r) const;
+    bool is_sbv2int(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); }
@@ -378,7 +383,8 @@ public:
     bool is_uge(expr const * e) const { return is_app_of(e, get_fid(), OP_UGEQ); }
     bool is_sge(expr const * e) const { return is_app_of(e, get_fid(), OP_SGEQ); }
     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_ubv2int(expr const* e) const { return is_app_of(e, get_fid(), OP_UBV2INT); }
+    bool is_sbv2int(expr const* e) const { return is_app_of(e, get_fid(), OP_SBV2INT); }
     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); }
@@ -549,7 +555,9 @@ public:
     app * mk_bv_ashr(expr* arg1, expr* arg2) { return m_manager.mk_app(get_fid(), OP_BASHR, arg1, arg2); }
     app * mk_bv_lshr(expr* arg1, expr* arg2) { return m_manager.mk_app(get_fid(), OP_BLSHR, arg1, arg2); }
 
-    app * mk_bv2int(expr* e) const;
+    app * mk_ubv2int(expr* e) const;
+    app * mk_sbv2int(expr* e) const;
+    app * mk_sbv2int_as_ubv2int(expr* e);
     app * mk_int2bv(unsigned sz, expr* e) const;
 
     app* mk_bv_rotate_left(expr* arg1, expr* arg2) { return m_manager.mk_app(get_fid(), OP_EXT_ROTATE_LEFT, arg1, arg2); }
diff --git a/src/ast/rewriter/bit2int.cpp b/src/ast/rewriter/bit2int.cpp
index cb845d2ba..d2c37dbbf 100644
--- a/src/ast/rewriter/bit2int.cpp
+++ b/src/ast/rewriter/bit2int.cpp
@@ -46,7 +46,7 @@ void bit2int::operator()(expr * n, expr_ref & result, proof_ref& p) {
 
 unsigned bit2int::get_b2i_size(expr* n) {
     expr* arg = nullptr;
-    VERIFY(m_bv_util.is_bv2int(n, arg));
+    VERIFY(m_bv_util.is_ubv2int(n, arg));
     return m_bv_util.get_bv_size(arg);
 }
 
@@ -83,7 +83,7 @@ bool bit2int::extract_bv(expr* n, unsigned& sz, bool& sign, expr_ref& bv) {
     numeral k;
     bool is_int;
     expr* r = nullptr;
-    if (m_bv_util.is_bv2int(n, r)) {
+    if (m_bv_util.is_ubv2int(n, r)) {
         bv = r;
         sz = m_bv_util.get_bv_size(bv);
         sign = false;
@@ -123,7 +123,7 @@ bool bit2int::mk_add(expr* e1, expr* e2, expr_ref& result) {
         tmp2 = m_rewriter.mk_zero_extend(1, tmp2);
         SASSERT(m_bv_util.get_bv_size(tmp1) == m_bv_util.get_bv_size(tmp2));
         tmp3 = m_rewriter.mk_bv_add(tmp1, tmp2);
-        result = m_rewriter.mk_bv2int(tmp3);
+        result = m_rewriter.mk_ubv2int(tmp3);
         return true;
     }
     return false;
@@ -168,7 +168,7 @@ bool bit2int::mk_mul(expr* e1, expr* e2, expr_ref& result) {
 
         SASSERT(m_bv_util.get_bv_size(tmp1) == m_bv_util.get_bv_size(tmp2));
         tmp3 = m_rewriter.mk_bv_mul(tmp1, tmp2);
-        result = m_rewriter.mk_bv2int(tmp3);
+        result = m_rewriter.mk_ubv2int(tmp3);
         if (sign1 != sign2) {
             result = m_arith_util.mk_uminus(result);
         }
@@ -183,13 +183,13 @@ bool bit2int::is_bv_poly(expr* n, expr_ref& pos, expr_ref& neg) {
     numeral k;
     bool is_int;
     todo.push_back(n);
-    neg = pos = m_rewriter.mk_bv2int(m_bit0);
+    neg = pos = m_rewriter.mk_ubv2int(m_bit0);
         
     while (!todo.empty()) {
         n = todo.back();
         todo.pop_back();
         expr* arg1 = nullptr, *arg2 = nullptr;
-        if (m_bv_util.is_bv2int(n)) {
+        if (m_bv_util.is_ubv2int(n)) {
             VERIFY(mk_add(n, pos, pos));
         }
         else if (m_arith_util.is_numeral(n, k, is_int) && is_int) {
@@ -208,16 +208,16 @@ bool bit2int::is_bv_poly(expr* n, expr_ref& pos, expr_ref& neg) {
         }
         else if (m_arith_util.is_mul(n, arg1, arg2) &&
                  m_arith_util.is_numeral(arg1, k, is_int) && is_int && k.is_minus_one() &&
-                 m_bv_util.is_bv2int(arg2)) {
+                 m_bv_util.is_ubv2int(arg2)) {
             VERIFY(mk_add(arg2, neg, neg));
         }
         else if (m_arith_util.is_mul(n, arg1, arg2) &&
                  m_arith_util.is_numeral(arg2, k, is_int) && is_int && k.is_minus_one() &&
-                 m_bv_util.is_bv2int(arg1)) {
+                 m_bv_util.is_ubv2int(arg1)) {
             VERIFY(mk_add(arg1, neg, neg));
         }
         else if (m_arith_util.is_uminus(n, arg1) &&
-                 m_bv_util.is_bv2int(arg1)) {
+                 m_bv_util.is_ubv2int(arg1)) {
             VERIFY(mk_add(arg1, neg, neg));
         }
         else {
@@ -251,7 +251,7 @@ void bit2int::visit(app* n) {
         m_arith_util.is_lt(n) || m.is_eq(n);
     expr_ref result(m);
     for (unsigned i = 0; !has_b2i && i < num_args; ++i) {
-        has_b2i = m_bv_util.is_bv2int(args[i]);
+        has_b2i = m_bv_util.is_ubv2int(args[i]);
     }
     if (!has_b2i) {
         result = m.mk_app(f, num_args, args);
@@ -367,7 +367,7 @@ void bit2int::visit(app* n) {
             tmp2 = e2bv;
             align_sizes(tmp1, tmp2);
             tmp3 = m_rewriter.mk_bv_urem(tmp1, tmp2);
-            result = m_rewriter.mk_bv2int(tmp3);
+            result = m_rewriter.mk_ubv2int(tmp3);
             cache_result(n, result);
             return;
         }
@@ -393,7 +393,7 @@ void bit2int::visit(app* n) {
         tmp2 = e2bv;
         align_sizes(tmp1, tmp2);
         tmp3 = m_rewriter.mk_bv_urem(tmp1, tmp2);
-        result = m_rewriter.mk_bv2int(tmp3);
+        result = m_rewriter.mk_ubv2int(tmp3);
 
         cache_result(n, result);
     }
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
index bb8b067e8..a3e797a80 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
@@ -548,7 +548,8 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
             case OP_BIT2BOOL:
             case OP_MKBV:
             case OP_INT2BV:
-            case OP_BV2INT:
+            case OP_UBV2INT:
+            case OP_SBV2INT:
                 return BR_FAILED;
             default:                
                 TRACE("bit_blaster", tout << "non-supported operator: " << f->get_name() << "\n";
diff --git a/src/ast/rewriter/bv2int_translator.cpp b/src/ast/rewriter/bv2int_translator.cpp
index 4e49e85e4..4387413bd 100644
--- a/src/ast/rewriter/bv2int_translator.cpp
+++ b/src/ast/rewriter/bv2int_translator.cpp
@@ -164,7 +164,7 @@ void bv2int_translator::translate_app(app* e) {
         expr* r = m.mk_app(f, m_args);
         if (has_bv_sort) {
             ctx.push(push_back_vector(m_vars));
-            r = bv.mk_bv2int(r);
+            r = bv.mk_ubv2int(r);
         }
         set_translated(e, r);
         return;
@@ -424,7 +424,7 @@ void bv2int_translator::translate_bv(app* e) {
         ctx.push(push_back_vector(m_int2bv));
         r = arg(0);
         break;
-    case OP_BV2INT:
+    case OP_UBV2INT:
         m_bv2int.push_back(e);
         ctx.push(push_back_vector(m_bv2int));
         r = umod(e->get_arg(0), 0);
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 0f73c7c89..5dd7c211f 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -197,9 +197,12 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
     case OP_EXT_ROTATE_RIGHT:
         SASSERT(num_args == 2);
         return mk_bv_ext_rotate_right(args[0], args[1], result);
-    case OP_BV2INT:
+    case OP_UBV2INT:
         SASSERT(num_args == 1);
-        return mk_bv2int(args[0], result);
+        return mk_ubv2int(args[0], result);
+    case OP_SBV2INT:
+        SASSERT(num_args == 1);
+        return mk_sbv2int(args[0], result);
     case OP_INT2BV:
         SASSERT(num_args == 1);
         return mk_int2bv(m_util.get_bv_size(f->get_range()), args[0], result);
@@ -1480,20 +1483,20 @@ br_status bv_rewriter::mk_int2bv(unsigned bv_size, expr * arg, expr_ref & result
         return BR_DONE;
     }
 
-    // int2bv (bv2int x) --> x
-    if (m_util.is_bv2int(arg, x) && bv_size == get_bv_size(x)) {
+    // int2bv (ubv2int x) --> x
+    if (m_util.is_ubv2int(arg, x) && bv_size == get_bv_size(x)) {
         result = x;
         return BR_DONE;
     }
 
-    // int2bv (bv2int x) --> 0000x
-    if (m_util.is_bv2int(arg, x) && bv_size > get_bv_size(x)) {
+    // int2bv (ubv2int x) --> 0000x
+    if (m_util.is_ubv2int(arg, x) && bv_size > get_bv_size(x)) {
         mk_zero_extend(bv_size - get_bv_size(x), x, result);
         return BR_REWRITE1;
     }
 
-    // int2bv (bv2int x) --> x[sz-1:0]
-    if (m_util.is_bv2int(arg, x) && bv_size < get_bv_size(x)) {
+    // int2bv (ubv2int x) --> x[sz-1:0]
+    if (m_util.is_ubv2int(arg, x) && bv_size < get_bv_size(x)) {
         result = m_mk_extract(bv_size - 1, 0, x);
         return BR_REWRITE1;
     }
@@ -1520,7 +1523,13 @@ br_status bv_rewriter::mk_int2bv(unsigned bv_size, expr * arg, expr_ref & result
     return BR_FAILED;
 }
 
-br_status bv_rewriter::mk_bv2int(expr * arg, expr_ref & result) {
+br_status bv_rewriter::mk_sbv2int(expr* arg, expr_ref& result) {
+    result = m_util.mk_sbv2int_as_ubv2int(arg);
+
+    return BR_REWRITE2;
+}
+
+br_status bv_rewriter::mk_ubv2int(expr * arg, expr_ref & result) {
     numeral v;
     unsigned sz;
     if (is_numeral(arg, v, sz)) {
@@ -1536,7 +1545,7 @@ br_status bv_rewriter::mk_bv2int(expr * arg, expr_ref & result) {
         
         unsigned num_args = to_app(arg)->get_num_args();
         for (expr* x : *to_app(arg)) {
-            args.push_back(m_util.mk_bv2int(x));
+            args.push_back(m_util.mk_ubv2int(x));
         }
         unsigned sz = get_bv_size(to_app(arg)->get_arg(num_args-1));
         for (unsigned i = num_args - 1; i > 0; ) {
@@ -1552,13 +1561,13 @@ br_status bv_rewriter::mk_bv2int(expr * arg, expr_ref & result) {
     }
     if (is_mul_no_overflow(arg)) {
         expr_ref_vector args(m);
-        for (expr* x : *to_app(arg)) args.push_back(m_util.mk_bv2int(x));
+        for (expr* x : *to_app(arg)) args.push_back(m_util.mk_ubv2int(x));
         result = m_autil.mk_mul(args.size(), args.data());
         return BR_REWRITE2;
     }
     if (is_add_no_overflow(arg)) {
         expr_ref_vector args(m);
-        for (expr* x : *to_app(arg)) args.push_back(m_util.mk_bv2int(x));
+        for (expr* x : *to_app(arg)) args.push_back(m_util.mk_ubv2int(x));
         result = m_autil.mk_add(args.size(), args.data());
         return BR_REWRITE2;
     }
@@ -2805,7 +2814,7 @@ br_status bv_rewriter::mk_eq_bv2int(expr* lhs, expr* rhs, expr_ref& result) {
     if (m_autil.is_numeral(lhs))
         std::swap(lhs, rhs);
    
-    if (m_autil.is_numeral(rhs, r) && m_util.is_bv2int(lhs, x)) {
+    if (m_autil.is_numeral(rhs, r) && m_util.is_ubv2int(lhs, x)) {
         unsigned bv_size = m_util.get_bv_size(x);
         if (0 <= r && r < rational::power_of_two(bv_size)) 
             result = m.mk_eq(m_util.mk_numeral(r, bv_size), x);
@@ -2813,8 +2822,8 @@ br_status bv_rewriter::mk_eq_bv2int(expr* lhs, expr* rhs, expr_ref& result) {
             result = m.mk_false();        
         return BR_REWRITE1;
     }
-    if (m_util.is_bv2int(lhs, x) &&
-        m_util.is_bv2int(rhs, y)) {
+    if (m_util.is_ubv2int(lhs, x) &&
+        m_util.is_ubv2int(rhs, y)) {
         auto szx = m_util.get_bv_size(x);
         auto szy = m_util.get_bv_size(y);
         if (szx < szy)
diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h
index bcf797353..713a0790b 100644
--- a/src/ast/rewriter/bv_rewriter.h
+++ b/src/ast/rewriter/bv_rewriter.h
@@ -128,7 +128,8 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     br_status mk_bv_urem_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_urem_core(arg1, arg2, true, result); }
     br_status mk_bv_smod_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_smod_core(arg1, arg2, true, result); }
     br_status mk_int2bv(unsigned bv_size, expr * arg, expr_ref & result);
-    br_status mk_bv2int(expr * arg, expr_ref & result);
+    br_status mk_ubv2int(expr * arg, expr_ref & result);
+    br_status mk_sbv2int(expr* arg, expr_ref& result);
     br_status mk_bv_redor(expr * arg, expr_ref & result);
     br_status mk_bv_redand(expr * arg, expr_ref & result);
     br_status mk_bv_comp(expr * arg1, expr * arg2, expr_ref & result);
@@ -244,10 +245,10 @@ public:
     MK_BV_BINARY(mk_bv_sub);
 
 
-    expr_ref mk_bv2int(expr* a) {
+    expr_ref mk_ubv2int(expr* a) {
         expr_ref result(m);
-        if (BR_FAILED == mk_bv2int(a, result)) 
-            result = m_util.mk_bv2int(a);
+        if (BR_FAILED == mk_ubv2int(a, result)) 
+            result = m_util.mk_ubv2int(a);
         return result;        
     }
 
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index e284c012c..a81567411 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -2639,7 +2639,7 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
     }
     if (str().is_ubv2s(a, b)) {
         bv_util bv(m());
-        result = bv.mk_bv2int(b);
+        result = bv.mk_ubv2int(b);
         return BR_DONE;
     }
     
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 10bc8ce8f..bb4b9fef1 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -693,7 +693,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     }
 
     br_status extended_bv_eq(expr* a, expr* b, expr_ref& result) {
-        if (m_bv_util.is_bv2int(a) || m_bv_util.is_bv2int(b))
+        if (m_bv_util.is_ubv2int(a) || m_bv_util.is_ubv2int(b))
             return m_bv_rw.mk_eq_bv2int(a, b, result);
         return BR_FAILED;        
     }
diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp
index 532cebe42..98e1e6e6b 100644
--- a/src/ast/sls/sls_bv_eval.cpp
+++ b/src/ast/sls/sls_bv_eval.cpp
@@ -693,7 +693,8 @@ namespace sls {
             NOT_IMPLEMENTED_YET();
             break;
         case OP_BIT2BOOL:
-        case OP_BV2INT:
+        case OP_UBV2INT:
+        case OP_SBV2INT:
         case OP_BNEG_OVFL:
         case OP_BSADD_OVFL:
         case OP_BUADD_OVFL:
@@ -824,7 +825,8 @@ namespace sls {
             return false;
         case OP_BIT1:
             return false;
-        case OP_BV2INT:
+        case OP_UBV2INT:
+        case OP_SBV2INT:
             return false;
         case OP_INT2BV:
             return try_repair_int2bv(assign_value(e), e->get_arg(0));          
diff --git a/src/ast/sls/sls_bv_fixed.cpp b/src/ast/sls/sls_bv_fixed.cpp
index 993b79c41..34e45ee4f 100644
--- a/src/ast/sls/sls_bv_fixed.cpp
+++ b/src/ast/sls/sls_bv_fixed.cpp
@@ -514,7 +514,8 @@ namespace sls {
         case OP_BV_NUM:
         case OP_BIT0:
         case OP_BIT1:
-        case OP_BV2INT:
+        case OP_UBV2INT:
+        case OP_SBV2INT:
         case OP_BNEG_OVFL:
         case OP_BSADD_OVFL:
         case OP_BUADD_OVFL:
diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp
index 78aecfbed..fca773680 100644
--- a/src/muz/fp/dl_cmds.cpp
+++ b/src/muz/fp/dl_cmds.cpp
@@ -159,17 +159,14 @@ struct dl_context {
 */
 class dl_rule_cmd : public cmd {
     ref<dl_context> m_dl_ctx;
-    mutable unsigned     m_arg_idx;
-    expr*        m_t;
+    mutable unsigned     m_arg_idx = 0;
+    expr* m_t = nullptr;
     symbol       m_name;
-    unsigned     m_bound;
+    unsigned     m_bound = UINT_MAX;
 public:
     dl_rule_cmd(dl_context * dl_ctx):
         cmd("rule"),
-        m_dl_ctx(dl_ctx),
-        m_arg_idx(0),
-        m_t(nullptr),
-        m_bound(UINT_MAX) {}
+        m_dl_ctx(dl_ctx) {}
     char const * get_usage() const override { return "(forall (q) (=> (and body) head)) :optional-name :optional-recursion-bound"; }
     char const * get_descr(cmd_context & ctx) const override { return "add a Horn rule."; }
     unsigned get_arity() const override { return VAR_ARITY; }
@@ -193,10 +190,9 @@ public:
         m_bound = bound;
         m_arg_idx++;
     }
-    void reset(cmd_context & ctx) override { m_dl_ctx->reset(); prepare(ctx); m_t = nullptr; }
-    void prepare(cmd_context& ctx) override { m_arg_idx = 0; m_name = symbol::null; m_bound = UINT_MAX; }
-    void finalize(cmd_context & ctx) override {
-    }
+    void reset(cmd_context& ctx) override { m_dl_ctx->reset(); prepare(ctx); m_t = nullptr; }
+    void prepare(cmd_context& ctx) override {  m_arg_idx = 0; m_t = nullptr;  m_name = symbol::null; m_bound = UINT_MAX; }
+    void finalize(cmd_context & ctx) override {}
     void execute(cmd_context & ctx) override {
         if (!m_t) throw cmd_exception("invalid rule, expected formula");
         m_dl_ctx->add_rule(m_t, m_name, m_bound);
diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp
index 0baf35ece..62d15d4bc 100644
--- a/src/qe/qe_arith_plugin.cpp
+++ b/src/qe/qe_arith_plugin.cpp
@@ -729,7 +729,7 @@ namespace qe {
             sort* s = m_bv.mk_sort(sz);
             z_bv = m.mk_fresh_const("z", s);
             expr_ref tmp(m);
-            z = m_bv.mk_bv2int(z_bv);
+            z = m_bv.mk_ubv2int(z_bv);
         }
 
         bool solve(conj_enum& conjs, expr* fml) {
diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp
index f1e9e8374..c791f1cae 100644
--- a/src/sat/smt/bv_internalize.cpp
+++ b/src/sat/smt/bv_internalize.cpp
@@ -139,7 +139,7 @@ namespace bv {
         SASSERT(!n || !n->is_attached_to(get_id()));
         bool suppress_args = !reflect() 
             && !m.is_considered_uninterpreted(a->get_decl())
-            && !bv.is_int2bv(e) && !bv.is_bv2int(e);
+            && !bv.is_int2bv(e) && !bv.is_ubv2int(e);
         if (!n)
             n = mk_enode(e, suppress_args);
 
@@ -219,7 +219,8 @@ namespace bv {
         case OP_REPEAT:           internalize_repeat(a); break;
         case OP_MKBV:             internalize_mkbv(a); break;
         case OP_INT2BV:           internalize_int2bv(a); break;
-        case OP_BV2INT:           internalize_bv2int(a); break;
+        case OP_UBV2INT:          internalize_bv2int(a); break;
+        case OP_SBV2INT:          throw default_exception("sbv_to_int is not handled. Pre-processing should have removed it");
         case OP_BUDIV:            internalize_int(bv.mk_bv_udiv_i, bv.mk_bv_udiv0); break;
         case OP_BSDIV:            internalize_int(bv.mk_bv_sdiv_i, bv.mk_bv_sdiv0); break;
         case OP_BSREM:            internalize_int(bv.mk_bv_srem_i, bv.mk_bv_srem0); break;
@@ -415,7 +416,7 @@ namespace bv {
 
     void solver::assert_bv2int_axiom(app* n) {
         expr* k = nullptr;        
-        VERIFY(bv.is_bv2int(n, k));
+        VERIFY(bv.is_ubv2int(n, k));
         SASSERT(bv.is_bv_sort(k->get_sort()));
         expr_ref_vector k_bits(m);
         euf::enode* k_enode = expr2enode(k);
@@ -461,7 +462,7 @@ namespace bv {
         VERIFY(bv.is_int2bv(n, e));      
         euf::enode* n_enode = expr2enode(n);
         expr_ref lhs(m), rhs(m);
-        lhs = bv.mk_bv2int(n);
+        lhs = bv.mk_ubv2int(n);
         unsigned sz = bv.get_bv_size(n);
         numeral mod = power(numeral(2), sz);
         rhs = m_autil.mk_mod(e, m_autil.mk_int(mod));
diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index e879ba30c..f898d5cd8 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -231,7 +231,7 @@ namespace bv {
         }
         else {
             for (euf::enode* bv2int : euf::enode_class(n1)) {                
-                if (bv.is_bv2int(bv2int->get_expr()))
+                if (bv.is_ubv2int(bv2int->get_expr()))
                     propagate_bv2int(bv2int);
             }
         }
diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp
index caca1e48c..1a3a646d7 100644
--- a/src/sat/smt/intblast_solver.cpp
+++ b/src/sat/smt/intblast_solver.cpp
@@ -382,7 +382,7 @@ namespace intblast {
             for (auto sib : euf::enode_class(n)) {
                 if (sib == n)
                     continue;
-                if (!bv.is_bv2int(sib->get_expr()))
+                if (!bv.is_ubv2int(sib->get_expr()))
                     continue;
                 if (sib->get_arg(0)->get_root() == r1)
                     continue;
@@ -401,7 +401,7 @@ namespace intblast {
         for (auto e : m_translator.int2bv()) {
             auto n = expr2enode(e);
             auto x = n->get_arg(0)->get_expr();
-            auto bv2int = bv.mk_bv2int(e);
+            auto bv2int = bv.mk_ubv2int(e);
             ctx.internalize(bv2int);
             auto N = rational::power_of_two(bv.get_bv_size(e));
             auto xModN = a.mk_mod(x, a.mk_int(N));
@@ -490,7 +490,7 @@ namespace intblast {
             rw.mk_app(n->get_decl(), args.size(), args.data(), value);
         }
         else {
-            expr_ref bv2int(bv.mk_bv2int(n->get_expr()), m);
+            expr_ref bv2int(bv.mk_ubv2int(n->get_expr()), m);
             euf::enode* b2i = ctx.get_enode(bv2int);
             SASSERT(b2i);
             VERIFY(b2i);
@@ -513,7 +513,7 @@ namespace intblast {
                 continue;
             auto t = m_translator.translated(e);
             
-            expr_ref ei(bv.mk_bv2int(e), m);
+            expr_ref ei(bv.mk_ubv2int(e), m);
             expr_ref ti(a.mk_mod(t, a.mk_int(rational::power_of_two(bv.get_bv_size(e)))), m);
             auto ev = mdl(ei);
             auto tv = mdl(ti);
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 26091dbc5..b6ebcbbc5 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -612,7 +612,7 @@ namespace smt {
         // n = bv2int(k) = ite(bit2bool(k[sz-1],2^{sz-1},0) + ... + ite(bit2bool(k[0],1,0))
         // 
         SASSERT(ctx.e_internalized(n));
-        SASSERT(m_util.is_bv2int(n));
+        SASSERT(m_util.is_ubv2int(n));
         TRACE("bv2int_bug", tout << "bv2int:\n" << mk_pp(n, m) << "\n";);
         sort * int_sort = n->get_sort();
         app * k = to_app(n->get_arg(0));
@@ -693,7 +693,7 @@ namespace smt {
         expr* n_expr = n;
         expr* e = n->get_arg(0);
         expr_ref lhs(m), rhs(m);
-        lhs = m.mk_app(get_id(), OP_BV2INT, 1, &param, 1, &n_expr);
+        lhs = m.mk_app(get_id(), OP_UBV2INT, 1, &param, 1, &n_expr);
         unsigned sz = m_util.get_bv_size(n);
         numeral mod = power(numeral(2), sz);
         rhs = m_autil.mk_mod(e, m_autil.mk_numeral(mod, true));
@@ -940,11 +940,13 @@ namespace smt {
                 internalize_int2bv(term); 
             }
             return params().m_bv_enable_int2bv2int;
-        case OP_BV2INT:         
+        case OP_UBV2INT:         
             if (params().m_bv_enable_int2bv2int) {
                 internalize_bv2int(term); 
             }
             return params().m_bv_enable_int2bv2int;
+        case OP_SBV2INT:
+            throw default_exception("sbv_to_int should have been removed by pre-processing");
         case OP_BSREM:        return false;
         case OP_BUREM:        return false;
         case OP_BSMOD:        return false;
@@ -1393,7 +1395,7 @@ namespace smt {
                 }
             }
         }
-        else if (params().m_bv_enable_int2bv2int && m_util.is_bv2int(n)) {
+        else if (params().m_bv_enable_int2bv2int && m_util.is_ubv2int(n)) {
             ctx.mark_as_relevant(n->get_arg(0));
             assert_bv2int_axiom(n);
         }
@@ -1537,7 +1539,7 @@ namespace smt {
             }
             else {
                 for (enode* bv2int : *n1) {
-                    if (m_util.is_bv2int(bv2int->get_expr())) 
+                    if (m_util.is_ubv2int(bv2int->get_expr())) 
                         propagate_bv2int(bv2int);
                 }
             }
diff --git a/src/smt/theory_intblast.cpp b/src/smt/theory_intblast.cpp
index 0e8b937d7..c6c94958e 100644
--- a/src/smt/theory_intblast.cpp
+++ b/src/smt/theory_intblast.cpp
@@ -45,7 +45,7 @@ namespace smt {
             for (auto sib : *n) {
                 if (sib == n)
                     continue;
-                if (!bv.is_bv2int(sib->get_expr()))
+                if (!bv.is_ubv2int(sib->get_expr()))
                     continue;
                 if (sib->get_arg(0)->get_root() == r1)
                     continue;
@@ -64,7 +64,7 @@ namespace smt {
         for (auto e : m_translator.int2bv()) {
             auto n = ctx.get_enode(e);
             auto x = n->get_arg(0)->get_expr();
-            auto bv2int = bv.mk_bv2int(e);
+            auto bv2int = bv.mk_ubv2int(e);
             ctx.internalize(bv2int, false);
             auto N = rational::power_of_two(bv.get_bv_size(e));
             auto xModN = a.mk_mod(x, a.mk_int(N));
diff --git a/src/tactic/arith/bv2int_rewriter.cpp b/src/tactic/arith/bv2int_rewriter.cpp
index d9f85d822..21d750d54 100644
--- a/src/tactic/arith/bv2int_rewriter.cpp
+++ b/src/tactic/arith/bv2int_rewriter.cpp
@@ -147,12 +147,12 @@ br_status bv2int_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr *
 
 br_status bv2int_rewriter::mk_le(expr * s, expr * t, expr_ref & result) {
     expr_ref s1(m()), t1(m()), s2(m()), t2(m());
-    if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
+    if (is_ubv2int(s, s1) && is_ubv2int(t, t1)) {
         align_sizes(s1, t1, false);
         result = m_bv.mk_ule(s1, t1);
         return BR_DONE;
     }
-    if (is_bv2int_diff(s, s1, s2) && is_bv2int_diff(t, t1, t2)) {
+    if (is_ubv2int_diff(s, s1, s2) && is_ubv2int_diff(t, t1, t2)) {
         //     s1 - s2 <= t1 - t2
         // <=>
         //     s1 + t2 <= t1 + s2
@@ -187,9 +187,9 @@ br_status bv2int_rewriter::mk_gt(expr * arg1, expr * arg2, expr_ref & result) {
 
 br_status bv2int_rewriter::mk_ite(expr* c, expr* s, expr* t, expr_ref& result) {
     expr_ref s1(m()), t1(m());
-    if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
+    if (is_ubv2int(s, s1) && is_ubv2int(t, t1)) {
         align_sizes(s1, t1, false);
-        result = m_bv.mk_bv2int(m().mk_ite(c, s1, t1));
+        result = m_bv.mk_ubv2int(m().mk_ite(c, s1, t1));
         return BR_DONE;
     }
 
@@ -203,12 +203,12 @@ br_status bv2int_rewriter::mk_ite(expr* c, expr* s, expr* t, expr_ref& result) {
 
 br_status bv2int_rewriter::mk_eq(expr * s, expr * t, expr_ref & result) {
     expr_ref s1(m()), t1(m()), s2(m()), t2(m());
-    if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
+    if (is_ubv2int(s, s1) && is_ubv2int(t, t1)) {
         align_sizes(s1, t1, false);
         result = m().mk_eq(s1, t1);
         return BR_DONE;
     }
-    if (is_bv2int_diff(s, s1, s2) && is_bv2int_diff(t, t1, t2)) {
+    if (is_ubv2int_diff(s, s1, s2) && is_ubv2int_diff(t, t1, t2)) {
         s1 = mk_bv_add(s1, t2, false);
         t1 = mk_bv_add(s2, t1, false);        
         align_sizes(s1, t1, false);
@@ -234,9 +234,9 @@ br_status bv2int_rewriter::mk_mod(expr * s, expr * t, expr_ref & result) {
     rational r;
     if (!m_arith.is_numeral(t, r) || !r.is_pos())
         return BR_FAILED;
-    if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
+    if (is_ubv2int(s, s1) && is_ubv2int(t, t1)) {
         align_sizes(s1, t1, false);
-        result = m_bv.mk_bv2int(m_bv.mk_bv_urem(s1, t1));
+        result = m_bv.mk_ubv2int(m_bv.mk_bv_urem(s1, t1));
         TRACE("bv2int_rewriter", tout << result << "\n";);
         return BR_DONE;
     }
@@ -244,14 +244,14 @@ br_status bv2int_rewriter::mk_mod(expr * s, expr * t, expr_ref & result) {
     //
     // (s1 - s2) mod t1 = (s1 + (t1 - (s2 mod t1))) mod t1
     //
-    if (is_bv2int_diff(s, s1, s2) && is_bv2int(t, t1)) {
+    if (is_ubv2int_diff(s, s1, s2) && is_ubv2int(t, t1)) {
         expr_ref u1(m());
         align_sizes(s2, t1, false);
         u1 = m_bv.mk_bv_urem(s2, t1);
         u1 = m_bv.mk_bv_sub(t1, u1);
         u1 = mk_bv_add(s1, u1, false);
         align_sizes(u1, t1, false);
-        result = m_bv.mk_bv2int(m_bv.mk_bv_urem(u1, t1));
+        result = m_bv.mk_ubv2int(m_bv.mk_bv_urem(u1, t1));
         TRACE("bv2int_rewriter", tout << result << "\n";);
         return BR_DONE;
     }
@@ -275,8 +275,8 @@ br_status bv2int_rewriter::mk_rem(expr * arg1, expr * arg2, expr_ref & result) {
 
 br_status bv2int_rewriter::mk_uminus(expr * s, expr_ref & result) {
     expr_ref s1(m()), s2(m());
-    if (is_bv2int_diff(s, s1, s2)) {
-        result = m_arith.mk_sub(m_bv.mk_bv2int(s2), m_bv.mk_bv2int(s1));
+    if (is_ubv2int_diff(s, s1, s2)) {
+        result = m_arith.mk_sub(m_bv.mk_ubv2int(s2), m_bv.mk_ubv2int(s1));
         return BR_DONE;
     }
     if (is_sbv2int(s, s1)) {
@@ -341,17 +341,17 @@ expr* bv2int_rewriter::mk_bv_add(expr* s, expr* t, bool is_signed) {
 
 br_status bv2int_rewriter::mk_add(expr* s, expr* t, expr_ref& result) {
     expr_ref s1(m()), t1(m()), s2(m()), t2(m());
-    if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
-        result = m_bv.mk_bv2int(mk_bv_add(s1, t1, false));
+    if (is_ubv2int(s, s1) && is_ubv2int(t, t1)) {
+        result = m_bv.mk_ubv2int(mk_bv_add(s1, t1, false));
         return BR_DONE;
     }
-    if (is_bv2int_diff(s, s1, s2) && is_bv2int_diff(t, t1, t2)) {
+    if (is_ubv2int_diff(s, s1, s2) && is_ubv2int_diff(t, t1, t2)) {
         //     s1 - s2 + t1 - t2
         // =
         //     s1 + t1 - (s2 + t2)
         //
-        t1 = m_bv.mk_bv2int(mk_bv_add(s1, t1, false));
-        t2 = m_bv.mk_bv2int(mk_bv_add(s2, t2, false));
+        t1 = m_bv.mk_ubv2int(mk_bv_add(s1, t1, false));
+        t2 = m_bv.mk_ubv2int(mk_bv_add(s2, t2, false));
         result = m_arith.mk_sub(t1, t2); 
         return BR_DONE;
     }
@@ -420,23 +420,23 @@ expr* bv2int_rewriter::mk_bv_mul(expr* s, expr* t, bool is_signed) {
 
 br_status bv2int_rewriter::mk_mul(expr* s, expr* t, expr_ref& result) {
     expr_ref s1(m()), s2(m()), t1(m()), t2(m());
-    if ((is_shl1(s, s1) && is_bv2int(t, t1)) ||
-        (is_shl1(t, s1) && is_bv2int(s, t1))) {
+    if ((is_shl1(s, s1) && is_ubv2int(t, t1)) ||
+        (is_shl1(t, s1) && is_ubv2int(s, t1))) {
         unsigned n = m_bv.get_bv_size(s1);
         unsigned m = m_bv.get_bv_size(t1);
         s1 = mk_extend(m, s1, false);
         t1 = mk_extend(n, t1, false);
-        result = m_bv.mk_bv2int(m_bv.mk_bv_shl(t1, s1));
+        result = m_bv.mk_ubv2int(m_bv.mk_bv_shl(t1, s1));
         return BR_DONE;
     }
-    if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
-        result = m_bv.mk_bv2int(mk_bv_mul(s1, t1, false));
+    if (is_ubv2int(s, s1) && is_ubv2int(t, t1)) {
+        result = m_bv.mk_ubv2int(mk_bv_mul(s1, t1, false));
         return BR_DONE;
     }
-    if ((is_bv2int(s, s1) && is_bv2int_diff(t, t1, t2)) ||
-        (is_bv2int(t, s1) && is_bv2int_diff(s, t1, t2))) {
-        t1 = m_bv.mk_bv2int(mk_bv_mul(s1, t1, false));
-        t2 = m_bv.mk_bv2int(mk_bv_mul(s1, t2, false));
+    if ((is_ubv2int(s, s1) && is_ubv2int_diff(t, t1, t2)) ||
+        (is_ubv2int(t, s1) && is_ubv2int_diff(s, t1, t2))) {
+        t1 = m_bv.mk_ubv2int(mk_bv_mul(s1, t1, false));
+        t2 = m_bv.mk_ubv2int(mk_bv_mul(s1, t2, false));
         result = m_arith.mk_sub(t1, t2);
         return BR_DONE;
     }
@@ -459,13 +459,13 @@ br_status bv2int_rewriter::mk_sub(unsigned num_args, expr * const* args, expr_re
 
 br_status bv2int_rewriter::mk_sub(expr* s, expr* t, expr_ref& result) {
     expr_ref s1(m()), t1(m()), s2(m()), t2(m());
-    if (is_bv2int_diff(s, s1, s2) && is_bv2int_diff(t, t1, t2)) {
+    if (is_ubv2int_diff(s, s1, s2) && is_ubv2int_diff(t, t1, t2)) {
         //     s1 - s2 - (t1 - t2)
         // =
         //     s1 + t2 - (t1 + s2)
         //
-        s1 = m_bv.mk_bv2int(mk_bv_add(s1, t2, false));
-        s2 = m_bv.mk_bv2int(mk_bv_add(s2, t1, false));
+        s1 = m_bv.mk_ubv2int(mk_bv_add(s1, t2, false));
+        s2 = m_bv.mk_ubv2int(mk_bv_add(s2, t1, false));
         result = m_arith.mk_sub(s1, s2); 
         return BR_DONE;
     }
@@ -479,10 +479,10 @@ br_status bv2int_rewriter::mk_sub(expr* s, expr* t, expr_ref& result) {
     return BR_FAILED;
 }
 
-bool bv2int_rewriter::is_bv2int(expr* n, expr_ref& s) {
+bool bv2int_rewriter::is_ubv2int(expr* n, expr_ref& s) {
     rational k;
     bool is_int;
-    if (m_bv.is_bv2int(n)) {
+    if (m_bv.is_ubv2int(n)) {
         s = to_app(n)->get_arg(0);
         return true;
     }
@@ -498,7 +498,7 @@ bool bv2int_rewriter::is_shl1(expr* n, expr_ref& s) {
     expr* s1, *s2;
     rational r;
     unsigned bv_size;
-    if(m_bv.is_bv2int(n, s2) && 
+    if(m_bv.is_ubv2int(n, s2) && 
         m_bv.is_bv_shl(s2, s1, s2) && 
         m_bv.is_numeral(s1, r, bv_size) && 
         r.is_one()) {
@@ -508,8 +508,8 @@ bool bv2int_rewriter::is_shl1(expr* n, expr_ref& s) {
     return false;
 }
 
-bool bv2int_rewriter::is_bv2int_diff(expr* n, expr_ref& s, expr_ref& t) {
-    if (is_bv2int(n, s)) {
+bool bv2int_rewriter::is_ubv2int_diff(expr* n, expr_ref& s, expr_ref& t) {
+    if (is_ubv2int(n, s)) {
         t = m_bv.mk_numeral(0, 1);
         return true;
     }
@@ -528,13 +528,13 @@ bool bv2int_rewriter::is_bv2int_diff(expr* n, expr_ref& s, expr_ref& t) {
     // 
     expr *e1, *e2;
     if (m_arith.is_sub(n, e1, e2) &&
-        is_bv2int(e1, s) &&
-        is_bv2int(e2, t)) {
+        is_ubv2int(e1, s) &&
+        is_ubv2int(e2, t)) {
         return true;
     }   
     if (m_arith.is_add(n, e1, e2) &&
         m_arith.is_numeral(e1, k, is_int) && is_int && k.is_neg() &&
-        is_bv2int(e2, s)) {
+        is_ubv2int(e2, s)) {
         k.neg();
         unsigned sz = k.get_num_bits();
         t = m_bv.mk_numeral(k, m_bv.mk_sort(sz));
@@ -542,7 +542,7 @@ bool bv2int_rewriter::is_bv2int_diff(expr* n, expr_ref& s, expr_ref& t) {
     }
     if (m_arith.is_add(n, e1, e2) &&
         m_arith.is_numeral(e2, k, is_int) && is_int && k.is_neg() &&
-        is_bv2int(e1, s)) {
+        is_ubv2int(e1, s)) {
         k.neg();
         unsigned sz = k.get_num_bits();
         t = m_bv.mk_numeral(k, m_bv.mk_sort(sz));
@@ -552,12 +552,12 @@ bool bv2int_rewriter::is_bv2int_diff(expr* n, expr_ref& s, expr_ref& t) {
 }
 
 bool bv2int_rewriter::is_sbv2int(expr* n, expr_ref& s) {
-    if (is_bv2int(n, s)) {
+    if (is_ubv2int(n, s)) {
         s = m_bv.mk_zero_extend(1, s);
         return true;
     }
     expr_ref u1(m()), u2(m());
-    if (is_bv2int_diff(n, u1, u2)) {
+    if (is_ubv2int_diff(n, u1, u2)) {
         align_sizes(u1, u2, false);
         u1 = mk_extend(1, u1, false);
         u2 = mk_extend(1, u2, false);
@@ -577,7 +577,7 @@ bool bv2int_rewriter::is_sbv2int(expr* n, expr_ref& s) {
         lo == hi && lo == m_bv.get_bv_size(c3) - 1 && 
         m_arith.is_sub(t, t1, t2) &&
         e1 == t1 &&
-        m_bv.is_bv2int(e1, e2) &&
+        m_bv.is_ubv2int(e1, e2) &&
         m_bv.is_extract(e2, lo1, hi1, e3) &&
         lo1 == 0 && hi1 == hi-1 &&
         m_arith.is_numeral(t2, k, is_int) && is_int &&
@@ -590,7 +590,7 @@ bool bv2int_rewriter::is_sbv2int(expr* n, expr_ref& s) {
 #if 0
     // bv2int(b[0:n-2]) - ite(bv1 == b[n-1:n-1], 2^{n-1}, 0)
     if (m().is_sub(n, e1, e2) &&
-        m_bv.is_bv2int(e1, e3) &&
+        m_bv.is_ubv2int(e1, e3) &&
         m_bv.is_extract(e3, lo, hi, e4) &&
         lo == 0 && hi == m_bv.get_bv_size(e4) - 2 &&
         m().is_ite(e2, t1, t2, t3) &&
@@ -612,7 +612,7 @@ expr* bv2int_rewriter::mk_sbv2int(expr* b) {
     expr* bv1 = m_bv.mk_numeral(1, 1);
     unsigned n = m_bv.get_bv_size(b);
     expr* c = m().mk_eq(bv1, m_bv.mk_extract(n-1, n-1, b));
-    expr* e = m_bv.mk_bv2int(m_bv.mk_extract(n-2, 0, b));
+    expr* e = m_bv.mk_ubv2int(m_bv.mk_extract(n-2, 0, b));
     expr* t = m_arith.mk_sub(e, m_arith.mk_numeral(power(rational(2), n-1), true));
     return m().mk_ite(c, t, e);
 } 
diff --git a/src/tactic/arith/bv2int_rewriter.h b/src/tactic/arith/bv2int_rewriter.h
index eb3c05790..a30ada255 100644
--- a/src/tactic/arith/bv2int_rewriter.h
+++ b/src/tactic/arith/bv2int_rewriter.h
@@ -84,9 +84,9 @@ private:
     br_status mk_sub(expr* s, expr* t, expr_ref& result);
     br_status mk_uminus(expr* e, expr_ref & result); 
 
-    bool      is_bv2int(expr* e, expr_ref& s);
+    bool      is_ubv2int(expr* e, expr_ref& s);
     bool      is_sbv2int(expr* e, expr_ref& s);
-    bool      is_bv2int_diff(expr* e, expr_ref& s, expr_ref& t);
+    bool      is_ubv2int_diff(expr* e, expr_ref& s, expr_ref& t);
     bool      is_zero(expr* e);
     bool      is_shl1(expr* e, expr_ref& s);
 
diff --git a/src/tactic/arith/bv2real_rewriter.cpp b/src/tactic/arith/bv2real_rewriter.cpp
index f94965fe9..66616fb12 100644
--- a/src/tactic/arith/bv2real_rewriter.cpp
+++ b/src/tactic/arith/bv2real_rewriter.cpp
@@ -146,7 +146,7 @@ void bv2real_util::mk_sbv2real(expr* e, expr_ref& result) {
     rational r;
     unsigned bv_size = m_bv.get_bv_size(e);
     rational bsize = power(rational(2), bv_size);
-    expr_ref bvr(a().mk_to_real(m_bv.mk_bv2int(e)), m());
+    expr_ref bvr(a().mk_to_real(m_bv.mk_ubv2int(e)), m());
     expr_ref c(m_bv.mk_sle(m_bv.mk_numeral(rational(0), bv_size), e), m());
     result = m().mk_ite(c, bvr, a().mk_sub(bvr, a().mk_numeral(bsize, false)));
 }
diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp
index 31ca836ac..f47953655 100644
--- a/src/tactic/arith/nla2bv_tactic.cpp
+++ b/src/tactic/arith/nla2bv_tactic.cpp
@@ -131,7 +131,7 @@ class nla2bv_tactic : public tactic {
             for (auto const& kv : p2) {
                 expr* v = kv.m_value;
                 unsigned num_bits = m_bv.get_bv_size(v);
-                expr* w = m_bv.mk_bv2int(m_bv.mk_bv_shl(m_bv.mk_numeral(1, num_bits), v));
+                expr* w = m_bv.mk_ubv2int(m_bv.mk_bv_shl(m_bv.mk_numeral(1, num_bits), v));
                 m_trail.push_back(w);
                 m_subst.insert(kv.m_key, w);
                 TRACE("nla2bv", tout << mk_ismt2_pp(kv.m_key, m_manager) << " " << mk_ismt2_pp(w, m_manager) << "\n";);
@@ -235,7 +235,7 @@ class nla2bv_tactic : public tactic {
             bv_sort = m_bv.mk_sort(num_bits);
             s_bv = m_manager.mk_fresh_const(n->get_decl()->get_name(), bv_sort);
             m_fmc->hide(s_bv);
-            s_bv = m_bv.mk_bv2int(s_bv);
+            s_bv = m_bv.mk_ubv2int(s_bv);
             if (low) {
                 if (!(*low).is_zero()) {
                     //    low <= s_bv 
diff --git a/src/tactic/fd_solver/bounded_int2bv_solver.cpp b/src/tactic/fd_solver/bounded_int2bv_solver.cpp
index 6f305372d..67e726ddf 100644
--- a/src/tactic/fd_solver/bounded_int2bv_solver.cpp
+++ b/src/tactic/fd_solver/bounded_int2bv_solver.cpp
@@ -190,7 +190,7 @@ public:
         for (auto const& kv : m_int2bv) {
             rational offset;
             VERIFY (m_bv2offset.find(kv.m_value, offset));
-            expr_ref value(m_bv.mk_bv2int(m.mk_const(kv.m_value)), m);
+            expr_ref value(m_bv.mk_ubv2int(m.mk_const(kv.m_value)), m);
             if (!offset.is_zero()) {
                 value = m_arith.mk_add(value, m_arith.mk_numeral(offset, true));
             }
@@ -293,7 +293,7 @@ private:
                     VERIFY(m_bv2offset.find(fbv, offset));
                 }
                 expr_ref t(m.mk_const(fbv), m);
-                t = m_bv.mk_bv2int(t);
+                t = m_bv.mk_ubv2int(t);
                 if (!offset.is_zero()) {
                     t = m_arith.mk_add(t, m_arith.mk_numeral(offset, true));
                 }