diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 7edc4a7a0..e396bb6b5 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -2422,29 +2422,6 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
     split_triple(args[0], sgn, s, e);
     result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s);
 }
-void fpa2bv_converter::mk_internal_bvwrap(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
-    TRACE("fpa2bv_internal", tout << "wrap ";
-                             for (unsigned i = 0; i < num; i++)
-                                 tout << " " << mk_ismt2_pp(args[i], m);
-                             tout << std::endl;);
-    SASSERT(num == 1);    
-    result = m.mk_app(f, num, args);
-}
-
-void fpa2bv_converter::mk_internal_bvunwrap(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
-    TRACE("fpa2bv_internal", tout << "unwrap ";
-    for (unsigned i = 0; i < num; i++)
-        tout << " " << mk_ismt2_pp(args[i], m);
-    tout << std::endl;);
-    SASSERT(num == 1);
-    app * a0 = to_app(args[0]);
-    SASSERT(a0->get_kind() == AST_APP);
-    SASSERT(is_float_family(a0->get_decl()));
-    decl_kind k = a0->get_decl_kind();
-    SASSERT(k == OP_FLOAT_INTERNAL_BVWRAP);
-    SASSERT(a0->get_num_args() == 1);
-    result = a0->get_arg(0);
-}
 
 void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 3);
@@ -2631,7 +2608,7 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
     expr_ref sgn(m), sig(m), exp(m), lz(m);
     unpack(x, sgn, sig, exp, lz, true);
     // sig is of the form [1].[sigbits]
-
+    
     SASSERT(m_bv_util.get_bv_size(sgn) == 1);
     SASSERT(m_bv_util.get_bv_size(sig) == sbits);
     SASSERT(m_bv_util.get_bv_size(exp) == ebits);
@@ -2646,8 +2623,8 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
     for (unsigned i = sbits-2; i != (unsigned)-1; i--)
     {
         bit = m_bv_util.mk_extract(i, i, sig);
-        rsig = m_arith_util.mk_mul(rsig, two);
-        rsig = m_arith_util.mk_add(rsig, m.mk_ite(m.mk_eq(bit, bv1), one, zero));
+        rsig = m_arith_util.mk_add(m_arith_util.mk_mul(rsig, two),
+                                   m.mk_ite(m.mk_eq(bit, bv1), one, zero));
     }
 
     const mpz & p2 = fu().fm().m_powers2(sbits-1);
@@ -2661,19 +2638,18 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
     exp_is_neg = m.mk_eq(m_bv_util.mk_extract(ebits - 1, ebits - 1, exp), bv1);
     dbg_decouple("fpa2bv_to_real_exp_is_neg", exp_is_neg);
     exp_p = m_bv_util.mk_sign_extend(1, exp);
-    exp_n = m_bv_util.mk_bv_not(m_bv_util.mk_sign_extend(1, exp));
+    exp_n = m_bv_util.mk_bv_neg(exp_p);
     exp_abs = m.mk_ite(exp_is_neg, exp_n, exp_p);
     dbg_decouple("fpa2bv_to_real_exp_abs", exp);
     SASSERT(m_bv_util.get_bv_size(exp_abs) == ebits + 1);
 
     expr_ref exp2(m), prev_bit(m);
     exp2 = zero;
-    prev_bit = bv0;
     for (unsigned i = ebits; i != (unsigned)-1; i--)
     {
         bit = m_bv_util.mk_extract(i, i, exp_abs);
-        exp2 = m_arith_util.mk_mul(exp2, two);
-        exp2 = m_arith_util.mk_add(exp2, m.mk_ite(m.mk_eq(bit, prev_bit), zero, one));
+        exp2 = m_arith_util.mk_add(m_arith_util.mk_mul(exp2, two),
+                                   m.mk_ite(m.mk_eq(bit, bv1), one, zero));
         prev_bit = bit;
     }
     
diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index 6a854adb3..440fc9d14 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -147,13 +147,6 @@ public:
     void dbg_decouple(const char * prefix, expr_ref & e);
     expr_ref_vector m_extra_assertions;
 
-    void mk_internal_bvwrap(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
-    void mk_internal_bvunwrap(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
-    
-    void mk_internal_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
-    void mk_internal_to_sbv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
-    void mk_internal_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
-
 protected:
     void mk_is_nan(expr * e, expr_ref & result);
     void mk_is_inf(expr * e, expr_ref & result);
diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h
index 42fd7a7fe..c9296dd5b 100644
--- a/src/ast/fpa/fpa2bv_rewriter.h
+++ b/src/ast/fpa/fpa2bv_rewriter.h
@@ -151,8 +151,11 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
             case OP_FLOAT_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
             case OP_FLOAT_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
             case OP_FLOAT_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_INTERNAL_BVWRAP: m_conv.mk_internal_bvwrap(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_INTERNAL_BVUNWRAP: m_conv.mk_internal_bvunwrap(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_INTERNAL_BVWRAP: 
+            case OP_FLOAT_INTERNAL_BVUNWRAP:
+            case OP_FLOAT_INTERNAL_TO_REAL_UNSPECIFIED:
+            case OP_FLOAT_INTERNAL_TO_UBV_UNSPECIFIED: 
+            case OP_FLOAT_INTERNAL_TO_SBV_UNSPECIFIED: return BR_FAILED;
             default:
                 TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
                       for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);