FPA bug and leak fixes (thanks to Gabriele Paganelli)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

src/ast/float_decl_plugin.cpp

@@ -151,6 +151,10 @@ sort * float_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, paramete
         if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) {
             m_manager->raise_exception("expecting two integer parameters to floating point sort");
         }
+        if (parameters[0].get_int() <= 1 || parameters[1].get_int() <= 1)
+            m_manager->raise_exception("floating point sorts need parameters > 1");
+        if (parameters[0].get_int() > parameters[1].get_int())
+            m_manager->raise_exception("floating point sorts with ebits > sbits are currently not supported");
         return mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
     case ROUNDING_MODE_SORT:
         return mk_rm_sort();

src/tactic/fpa/fpa2bv_converter.cpp

@@ -21,8 +21,8 @@ Notes:
 
 #include"fpa2bv_converter.h"
 
-#define BVULT(X,Y,R) { expr_ref bvult_eq(m), bvult_not(m); m_simp.mk_eq(X, Y, bvult_eq); m_simp.mk_not(bvult_eq, bvult_not); m_simp.mk_and(m_bv_util.mk_ule(X,Y), bvult_not, R); }
+#define BVULT(X,Y,R) { expr_ref bvult_eq(m), bvult_not(m); m_simp.mk_eq(X, Y, bvult_eq); m_simp.mk_not(bvult_eq, bvult_not); expr_ref t(m); t = m_bv_util.mk_ule(X,Y); m_simp.mk_and(t, bvult_not, R); }
-#define BVSLT(X,Y,R) { expr_ref bvslt_eq(m), bvslt_not(m); m_simp.mk_eq(X, Y, bvslt_eq); m_simp.mk_not(bvslt_eq, bvslt_not); m_simp.mk_and(m_bv_util.mk_sle(X,Y), bvslt_not, R); }
+#define BVSLT(X,Y,R) { expr_ref bvslt_eq(m), bvslt_not(m); m_simp.mk_eq(X, Y, bvslt_eq); m_simp.mk_not(bvslt_eq, bvslt_not); expr_ref t(m); t = m_bv_util.mk_sle(X,Y); m_simp.mk_and(t, bvslt_not, R); }
 
 fpa2bv_converter::fpa2bv_converter(ast_manager & m) : 
     m(m),
@@ -123,17 +123,23 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
         unsigned ebits = m_util.get_ebits(srt);
         unsigned sbits = m_util.get_sbits(srt);
         
+        expr_ref sgn(m), s(m), e(m);
+        sort_ref s_sgn(m), s_sig(m), s_exp(m);
+        s_sgn =  m_bv_util.mk_sort(1);
+        s_sig = m_bv_util.mk_sort(sbits-1);
+        s_exp = m_bv_util.mk_sort(ebits);
+
 #ifdef _DEBUG
         std::string p("fpa2bv");
         std::string name = f->get_name().str();
         
-        expr * sgn = m.mk_fresh_const((p + "_sgn_" + name).c_str(), m_bv_util.mk_sort(1));
+        sgn = m.mk_fresh_const((p + "_sgn_" + name).c_str(), s_sgn);
-        expr * s = m.mk_fresh_const((p + "_sig_" + name).c_str(), m_bv_util.mk_sort(sbits-1));
+        s = m.mk_fresh_const((p + "_sig_" + name).c_str(), s_sig);
-        expr * e = m.mk_fresh_const((p + "_exp_" + name).c_str(), m_bv_util.mk_sort(ebits));
+        e = m.mk_fresh_const((p + "_exp_" + name).c_str(), s_exp);
 #else
-        expr * sgn = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
+        sgn = m.mk_fresh_const(0, s_sgn);
-        expr * s = m.mk_fresh_const(0, m_bv_util.mk_sort(sbits-1));
+        s = m.mk_fresh_const(0, s_sig);
-        expr * e = m.mk_fresh_const(0, m_bv_util.mk_sort(ebits));
+        e = m.mk_fresh_const(0, s_exp);
 #endif
         
         mk_triple(sgn, s, e, result);
@@ -245,9 +251,10 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm,
     dbg_decouple("fpa2bv_add_exp_delta", exp_delta);
 
     // cap the delta    
-    expr_ref cap(m);
+    expr_ref cap(m), cap_le_delta(m);
     cap = m_bv_util.mk_numeral(sbits+2, ebits);
-    m_simp.mk_ite(m_bv_util.mk_ule(cap, exp_delta), cap, exp_delta, exp_delta);
+    cap_le_delta = m_bv_util.mk_ule(cap, exp_delta);
+    m_simp.mk_ite(cap_le_delta, cap, exp_delta, exp_delta);
 
     dbg_decouple("fpa2bv_add_exp_delta_capped", exp_delta);
 
@@ -270,21 +277,23 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm,
     SASSERT(is_well_sorted(m, shifted_d_sig));
 
     sticky_raw = m_bv_util.mk_extract(sbits+2, 0, shifted_big);    
-    expr_ref sticky_eq(m); 
+    expr_ref sticky_eq(m), nil_sbit3(m), one_sbit3(m); 
-    m_simp.mk_eq(sticky_raw, m_bv_util.mk_numeral(0, sbits+3), sticky_eq);
+    nil_sbit3 = m_bv_util.mk_numeral(0, sbits+3);
-    m_simp.mk_ite(sticky_eq, 
+    one_sbit3 = m_bv_util.mk_numeral(1, sbits+3);
-                  m_bv_util.mk_numeral(0, sbits+3), 
+    m_simp.mk_eq(sticky_raw, nil_sbit3, sticky_eq);
-                  m_bv_util.mk_numeral(1, sbits+3),
+    m_simp.mk_ite(sticky_eq, nil_sbit3, one_sbit3, sticky);
-                  sticky);    
     SASSERT(is_well_sorted(m, sticky));
     
-    expr * or_args[2] = { shifted_d_sig.get(), sticky.get() };
+    expr * or_args[2] = { shifted_d_sig, sticky };
     shifted_d_sig = m_bv_util.mk_bv_or(2, or_args);
     SASSERT(is_well_sorted(m, shifted_d_sig));
 
-    expr_ref eq_sgn(m), neq_sgn(m);
+    expr_ref eq_sgn(m);
     m_simp.mk_eq(c_sgn, d_sgn, eq_sgn);
 
+    // dbg_decouple("fpa2bv_add_eq_sgn", eq_sgn);
+    TRACE("fpa2bv_add_core", tout << "EQ_SGN = " << mk_ismt2_pp(eq_sgn, m) << std::endl; );    
+    
     // two extra bits for catching the overflow.
     c_sig = m_bv_util.mk_zero_extend(2, c_sig);
     shifted_d_sig = m_bv_util.mk_zero_extend(2, shifted_d_sig);
@@ -318,11 +327,12 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm,
     res_sgn_c1 = m.mk_app(bvfid, OP_BAND, m_bv_util.mk_bv_not(c_sgn), d_sgn, sign_bv);
     res_sgn_c2 = m.mk_app(bvfid, OP_BAND, c_sgn, m_bv_util.mk_bv_not(d_sgn), m_bv_util.mk_bv_not(sign_bv));
     res_sgn_c3 = m.mk_app(bvfid, OP_BAND, c_sgn, d_sgn);
-    expr * res_sgn_or_args[3] = { res_sgn_c1.get(), res_sgn_c2.get(), res_sgn_c3.get() };   
+    expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 };   
     res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args);
 
-    expr_ref res_sig_eq(m), sig_abs(m);
+    expr_ref res_sig_eq(m), sig_abs(m), one_1(m);
-    m_simp.mk_eq(sign_bv, m_bv_util.mk_numeral(1, 1), res_sig_eq);
+    one_1 = m_bv_util.mk_numeral(1, 1);
+    m_simp.mk_eq(sign_bv, one_1, res_sig_eq);
     m_simp.mk_ite(res_sig_eq, n_sum, sum, sig_abs);
 
     dbg_decouple("fpa2bv_add_sig_abs", sig_abs);
@@ -432,8 +442,9 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args,
              c_sgn, c_sig, c_exp, d_sgn, d_sig, d_exp, 
              res_sgn, res_sig, res_exp);
 
-    expr_ref is_zero_sig(m);
+    expr_ref is_zero_sig(m), nil_sbit4(m);
-    m_simp.mk_eq(res_sig, m_bv_util.mk_numeral(0, sbits+4), is_zero_sig);
+    nil_sbit4 = m_bv_util.mk_numeral(0, sbits+4);
+    m_simp.mk_eq(res_sig, nil_sbit4, is_zero_sig);
 
     SASSERT(is_well_sorted(m, is_zero_sig));
 
@@ -463,7 +474,7 @@ void fpa2bv_converter::mk_sub(func_decl * f, unsigned num, expr * const * args,
     SASSERT(num == 3);
     expr_ref t(m);
     mk_uminus(f, 1, &args[2], t);
-    expr * nargs[3] = { args[0], args[1], t.get() };
+    expr * nargs[3] = { args[0], args[1], t };
     mk_add(f, 3, nargs, result);
 }
 
@@ -589,9 +600,20 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args,
 
     SASSERT(m_bv_util.get_bv_size(product) == 2*sbits);
 
+    expr_ref h_p(m), l_p(m), rbits(m);
+    h_p = m_bv_util.mk_extract(2*sbits-1, sbits, product);
+    l_p = m_bv_util.mk_extract(2*sbits-1, sbits, product);
+    
+    if (sbits >= 4) {
         expr_ref sticky(m);
-    sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(sbits-4, 0, product));    
+        sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(sbits-4, 0, l_p));    
-    res_sig = m_bv_util.mk_concat(m_bv_util.mk_extract(2*sbits-1, sbits-3, product), sticky);
+        rbits = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits-1, sbits-3, l_p), sticky);
+    }
+    else
+        rbits = m_bv_util.mk_concat(l_p, m_bv_util.mk_numeral(0, 4 - m_bv_util.get_bv_size(l_p)));
+    
+    SASSERT(m_bv_util.get_bv_size(rbits) == 4);
+    res_sig = m_bv_util.mk_concat(h_p, rbits);
 
     round(f->get_range(), rm, res_sgn, res_sig, res_exp, v7);
 
@@ -1108,8 +1130,9 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
     sig_size = m_bv_util.get_bv_size(res_sig);    
     SASSERT(sig_size == sbits+4);    
 
-    expr_ref is_zero_sig(m);
+    expr_ref is_zero_sig(m), nil_sbits4(m);
-    m_simp.mk_eq(res_sig, m_bv_util.mk_numeral(0, sbits+4), is_zero_sig);
+    nil_sbits4 = m_bv_util.mk_numeral(0, sbits+4);
+    m_simp.mk_eq(res_sig, nil_sbits4, is_zero_sig);
 
     SASSERT(is_well_sorted(m, is_zero_sig));
 
@@ -1175,10 +1198,10 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
     expr_ref a_sgn(m), a_sig(m), a_exp(m);
     unpack(x, a_sgn, a_sig, a_exp, true);
 
-    expr_ref exp_is_small(m);
+    expr_ref exp_is_small(m), exp_h(m), one_1(m);
-    m_simp.mk_eq(m_bv_util.mk_extract(ebits-1, ebits-1, a_exp),
+    exp_h = m_bv_util.mk_extract(ebits-1, ebits-1, a_exp);
-                 m_bv_util.mk_numeral(1, 1),
+    one_1 = m_bv_util.mk_numeral(1, 1);
-                 exp_is_small);
+    m_simp.mk_eq(exp_h, one_1, exp_is_small);
     dbg_decouple("fpa2bv_r2i_exp_is_small", exp_is_small);
     c3 = exp_is_small;
     mk_ite(x_is_pos, pzero, nzero, v3);
@@ -1273,12 +1296,13 @@ void fpa2bv_converter::mk_float_lt(func_decl * f, unsigned num, expr * const * a
     split(x, x_sgn, x_sig, x_exp);
     split(y, y_sgn, y_sig, y_exp);
 
-    expr_ref c3(m), t3(m), t4(m);
+    expr_ref c3(m), t3(m), t4(m), one_1(m), nil_1(m);
-
+    one_1 = m_bv_util.mk_numeral(1, 1);
-    m_simp.mk_eq(x_sgn, m_bv_util.mk_numeral(1, 1), c3);
+    nil_1 = m_bv_util.mk_numeral(0, 1);
+    m_simp.mk_eq(x_sgn, one_1, c3);
 
     expr_ref y_sgn_eq_0(m), y_lt_x_exp(m), y_lt_x_sig(m), y_eq_x_exp(m), y_le_x_sig_exp(m), t3_or(m);
-    m_simp.mk_eq(y_sgn, m_bv_util.mk_numeral(0, 1), y_sgn_eq_0);
+    m_simp.mk_eq(y_sgn, nil_1, y_sgn_eq_0);
     BVULT(y_exp, x_exp, y_lt_x_exp);
     BVULT(y_sig, x_sig, y_lt_x_sig);
     m_simp.mk_eq(y_exp, x_exp, y_eq_x_exp);
@@ -1287,7 +1311,7 @@ void fpa2bv_converter::mk_float_lt(func_decl * f, unsigned num, expr * const * a
     m_simp.mk_ite(y_sgn_eq_0, m.mk_true(), t3_or, t3);
 
     expr_ref y_sgn_eq_1(m), x_lt_y_exp(m), x_eq_y_exp(m), x_lt_y_sig(m), x_le_y_sig_exp(m), t4_or(m);
-    m_simp.mk_eq(y_sgn, m_bv_util.mk_numeral(1, 1), y_sgn_eq_1);
+    m_simp.mk_eq(y_sgn, one_1, y_sgn_eq_1);
     BVULT(x_exp, y_exp, x_lt_y_exp);
     m_simp.mk_eq(x_exp, y_exp, x_eq_y_exp);
     BVULT(x_sig, y_sig, x_lt_y_sig);
@@ -1418,10 +1442,11 @@ void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) {
     split(e, sgn, sig, exp);
     
     // exp == 1^n , sig != 0
-    expr_ref sig_is_zero(m), sig_is_not_zero(m), exp_is_top(m), top_exp(m);
+    expr_ref sig_is_zero(m), sig_is_not_zero(m), exp_is_top(m), top_exp(m), zero(m);
     mk_top_exp(m_bv_util.get_bv_size(exp), top_exp);
 
-    m_simp.mk_eq(sig, m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig)), sig_is_zero);
+    zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig));
+    m_simp.mk_eq(sig, zero, sig_is_zero);
     m_simp.mk_not(sig_is_zero, sig_is_not_zero);
     m_simp.mk_eq(exp, top_exp, exp_is_top);
     m_simp.mk_and(exp_is_top, sig_is_not_zero, result);
@@ -1430,9 +1455,10 @@ void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) {
 void fpa2bv_converter::mk_is_inf(expr * e, expr_ref & result) {
     expr * sgn, * sig, * exp;
     split(e, sgn, sig, exp);
-    expr_ref eq1(m), eq2(m), top_exp(m);
+    expr_ref eq1(m), eq2(m), top_exp(m), zero(m);
     mk_top_exp(m_bv_util.get_bv_size(exp), top_exp);
-    m_simp.mk_eq(sig, m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig)), eq1);
+    zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig));
+    m_simp.mk_eq(sig, zero, eq1);
     m_simp.mk_eq(exp, top_exp, eq2);
     m_simp.mk_and(eq1, eq2, result);
 }
@@ -1455,22 +1481,27 @@ void fpa2bv_converter::mk_is_pos(expr * e, expr_ref & result) {
     SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT));
     SASSERT(to_app(e)->get_num_args() == 3);
     expr * a0 = to_app(e)->get_arg(0);
-    m_simp.mk_eq(a0, m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(a0)), result);
+    expr_ref zero(m);
+    zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(a0));
+    m_simp.mk_eq(a0, zero, result);
 }
 
 void fpa2bv_converter::mk_is_neg(expr * e, expr_ref & result) {
     SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT));
     SASSERT(to_app(e)->get_num_args() == 3);
     expr * a0 = to_app(e)->get_arg(0);
-    m_simp.mk_eq(a0, m_bv_util.mk_numeral(1, m_bv_util.get_bv_size(a0)), result);
+    expr_ref one(m);
+    one = m_bv_util.mk_numeral(1, m_bv_util.get_bv_size(a0));
+    m_simp.mk_eq(a0, one, result);
 }
 
 void fpa2bv_converter::mk_is_zero(expr * e, expr_ref & result) {
     expr * sgn, * sig, * exp;
     split(e, sgn, sig, exp);
-    expr_ref eq1(m), eq2(m), bot_exp(m);
+    expr_ref eq1(m), eq2(m), bot_exp(m), zero(m);
     mk_bot_exp(m_bv_util.get_bv_size(exp), bot_exp);
-    m_simp.mk_eq(sig, m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig)), eq1);
+    zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig));
+    m_simp.mk_eq(sig, zero, eq1);
     m_simp.mk_eq(exp, bot_exp, eq2);
     m_simp.mk_and(eq1, eq2, result);
 }
@@ -1478,35 +1509,40 @@ void fpa2bv_converter::mk_is_zero(expr * e, expr_ref & result) {
 void fpa2bv_converter::mk_is_nzero(expr * e, expr_ref & result) {
     expr * sgn, * sig, * exp;
     split(e, sgn, sig, exp);
-    expr_ref e_is_zero(m), eq(m);
+    expr_ref e_is_zero(m), eq(m), one_1(m);
     mk_is_zero(e, e_is_zero);
-    m_simp.mk_eq(sgn, m_bv_util.mk_numeral(1, 1), eq);
+    one_1 = m_bv_util.mk_numeral(1, 1);
+    m_simp.mk_eq(sgn, one_1, eq);
     m_simp.mk_and(eq, e_is_zero, result);
 }
 
 void fpa2bv_converter::mk_is_pzero(expr * e, expr_ref & result) {
     expr * sgn, * sig, * exp;
     split(e, sgn, sig, exp);
-    expr_ref e_is_zero(m), eq(m);
+    expr_ref e_is_zero(m), eq(m), nil_1(m);
     mk_is_zero(e, e_is_zero);
-    m_simp.mk_eq(sgn, m_bv_util.mk_numeral(0, 1), eq);
+    nil_1 = m_bv_util.mk_numeral(0, 1);
+    m_simp.mk_eq(sgn, nil_1, eq);
     m_simp.mk_and(eq, e_is_zero, result);
 }
 
 void fpa2bv_converter::mk_is_denormal(expr * e, expr_ref & result) {
     expr * sgn, * sig, * exp;
     split(e, sgn, sig, exp);
-    m_simp.mk_eq(exp, m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(exp)), result);
+    expr_ref zero(m);
+    zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(exp));
+    m_simp.mk_eq(exp, zero, result);
 }
 
 void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) {    
     expr * sgn, * sig, * exp;
     split(e, sgn, sig, exp);
 
-    expr_ref is_special(m), is_denormal(m);
+    expr_ref is_special(m), is_denormal(m), p(m);
     mk_is_denormal(e, is_denormal);
     unsigned ebits = m_bv_util.get_bv_size(exp);
-    m_simp.mk_eq(exp, m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits), ebits), is_special);
+    p = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits), ebits);
+    m_simp.mk_eq(exp, p, is_special);
 
     expr_ref or_ex(m);
     m_simp.mk_or(is_special, is_denormal, or_ex);
@@ -1557,9 +1593,12 @@ void fpa2bv_converter::mk_leading_zeros(expr * e, unsigned max_bits, expr_ref &
     if (bv_sz == 0)
         result = m_bv_util.mk_numeral(0, max_bits);
     else if (bv_sz == 1) {
-        expr_ref eq(m);
+        expr_ref eq(m), nil_1(m), one_m(m), nil_m(m);
-        m_simp.mk_eq(e, m_bv_util.mk_numeral(0, 1), eq);
+        nil_1 = m_bv_util.mk_numeral(0, 1);
-        m_simp.mk_ite(eq, m_bv_util.mk_numeral(1, max_bits), m_bv_util.mk_numeral(0, max_bits), result);
+        one_m = m_bv_util.mk_numeral(1, max_bits);
+        nil_m = m_bv_util.mk_numeral(0, max_bits);
+        m_simp.mk_eq(e, nil_1, eq);
+        m_simp.mk_ite(eq, one_m, nil_m, result);
     }
     else {
         expr_ref H(m), L(m);
@@ -1573,11 +1612,13 @@ void fpa2bv_converter::mk_leading_zeros(expr * e, unsigned max_bits, expr_ref &
         mk_leading_zeros(H, max_bits, lzH); /* recursive! */
         mk_leading_zeros(L, max_bits, lzL);
 
-        expr_ref H_is_zero(m);
+        expr_ref H_is_zero(m), nil_h(m);
-        m_simp.mk_eq(H, m_bv_util.mk_numeral(0, H_size), H_is_zero);        
+        nil_h = m_bv_util.mk_numeral(0, H_size);
+        m_simp.mk_eq(H, nil_h, H_is_zero);        
 
-        expr_ref sum(m);
+        expr_ref sum(m), h_m(m);
-        sum = m_bv_util.mk_bv_add(m_bv_util.mk_numeral(H_size, max_bits), lzL);
+        h_m = m_bv_util.mk_numeral(H_size, max_bits);
+        sum = m_bv_util.mk_bv_add(h_m, lzL);
         m_simp.mk_ite(H_is_zero, sum, lzH, result);        
     }
 
@@ -1634,25 +1675,40 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref
     mk_unbias(denormal_exp, denormal_exp);
 
     if (normalize) {
-        expr_ref is_sig_zero(m), shift(m), lz(m);
+        expr_ref is_sig_zero(m), shift(m), lz(m), zero_s(m), zero_e(m);
-        m_simp.mk_eq(m_bv_util.mk_numeral(0, sbits-1), sig, is_sig_zero);
+        zero_s = m_bv_util.mk_numeral(0, sbits-1);
+        zero_e = m_bv_util.mk_numeral(0, ebits);
+        m_simp.mk_eq(zero_s, sig, is_sig_zero);
         mk_leading_zeros(sig, ebits, lz);
-        m_simp.mk_ite(is_sig_zero, m_bv_util.mk_numeral(0, ebits), lz, shift);
+        m_simp.mk_ite(is_sig_zero, zero_e, lz, shift);
         SASSERT(is_well_sorted(m, is_sig_zero));
         SASSERT(is_well_sorted(m, lz));
         SASSERT(is_well_sorted(m, shift));
-        if (ebits < sbits) {        
+        SASSERT(m_bv_util.get_bv_size(shift) == ebits);
+        if (ebits <= sbits) {        
             expr_ref q(m);
             q = m_bv_util.mk_zero_extend(sbits-ebits, shift);
             denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, q);
         } 
         else {
-            denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, shift);
+            // the maximum shift is `sbits', because after that the mantissa
+            // would be zero anyways. So we can safely cut the shift variable down,
+            // as long as we check the higher bits.            
+            expr_ref sh(m), is_sh_zero(m), sl(m), zero_s(m), sbits_s(m), short_shift(m);
+            zero_s = m_bv_util.mk_numeral(0, sbits-1);
+            sbits_s = m_bv_util.mk_numeral(sbits, sbits);
+            sh = m_bv_util.mk_extract(ebits-1, sbits, shift);            
+            m_simp.mk_eq(zero_s, sh, is_sh_zero);
+            short_shift = m_bv_util.mk_extract(sbits-1, 0, shift);
+            m_simp.mk_ite(is_sh_zero, short_shift, sbits_s, sl);
+            denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, sl);
         }
     }
 
     SASSERT(is_well_sorted(m, normal_sig));
     SASSERT(is_well_sorted(m, denormal_sig));
+    SASSERT(is_well_sorted(m, normal_exp));
+    SASSERT(is_well_sorted(m, denormal_exp));
 
     m_simp.mk_ite(is_normal, normal_sig, denormal_sig, sig);
     m_simp.mk_ite(is_normal, normal_exp, denormal_exp, exp);
@@ -1685,6 +1741,7 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result)
 
 void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {    
     #ifdef _DEBUG
+    // return;
     expr_ref new_e(m);
     new_e = m.mk_fresh_const(prefix, m.get_sort(e));
     extra_assertions.push_back(m.mk_eq(new_e, e));    
@@ -1737,15 +1794,23 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
                                 "e_max = " << mk_ismt2_pp(e_max, m) << std::endl;);    
 
     expr_ref OVF1(m), e_top_three(m), sigm1(m), e_eq_emax_and_sigm1(m), e_eq_emax(m);
-    expr_ref e3(m), ne3(m), e2(m), e1(m), e21(m);    
+    expr_ref e3(m), ne3(m), e2(m), e1(m), e21(m), one_1(m), h_exp(m), sh_exp(m), th_exp(m);
-    m_simp.mk_eq(m_bv_util.mk_extract(ebits+1, ebits+1, exp), m_bv_util.mk_numeral(1, 1), e3);
+    one_1 = m_bv_util.mk_numeral(1, 1);
-    m_simp.mk_eq(m_bv_util.mk_extract(ebits, ebits, exp), m_bv_util.mk_numeral(1, 1), e2);
+    h_exp = m_bv_util.mk_extract(ebits+1, ebits+1, exp);
-    m_simp.mk_eq(m_bv_util.mk_extract(ebits-1, ebits-1, exp), m_bv_util.mk_numeral(1, 1), e1);
+    sh_exp = m_bv_util.mk_extract(ebits, ebits, exp);
+    th_exp = m_bv_util.mk_extract(ebits-1, ebits-1, exp);
+    m_simp.mk_eq(h_exp, one_1, e3);
+    m_simp.mk_eq(sh_exp, one_1, e2);
+    m_simp.mk_eq(th_exp, one_1, e1);
     m_simp.mk_or(e2, e1, e21);
     m_simp.mk_not(e3, ne3);
     m_simp.mk_and(ne3, e21, e_top_three);
-    m_simp.mk_eq(m_bv_util.mk_zero_extend(2, e_max), exp, e_eq_emax);
+
-    m_simp.mk_eq(m_bv_util.mk_extract(sbits+3, sbits+3, sig), m_bv_util.mk_numeral(1, 1), sigm1);
+    expr_ref ext_emax(m), t_sig(m);
+    ext_emax = m_bv_util.mk_zero_extend(2, e_max);
+    t_sig = m_bv_util.mk_extract(sbits+3, sbits+3, sig);
+    m_simp.mk_eq(ext_emax, exp, e_eq_emax);
+    m_simp.mk_eq(t_sig, one_1, sigm1);
     m_simp.mk_and(e_eq_emax, sigm1, e_eq_emax_and_sigm1);
     m_simp.mk_or(e_top_three, e_eq_emax_and_sigm1, OVF1);
     
@@ -1797,10 +1862,12 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
     SASSERT(sig_size == sbits+4);
     unsigned sigma_size = m_bv_util.get_bv_size(sigma);
 
-	expr_ref sigma_neg(m), sigma_cap(m), sigma_neg_capped(m), sigma_lt_zero(m), sig_ext(m), rs_sig(m), ls_sig(m), big_sh_sig(m);
+    expr_ref sigma_neg(m), sigma_cap(m), sigma_neg_capped(m), sigma_lt_zero(m), sig_ext(m), 
+             rs_sig(m), ls_sig(m), big_sh_sig(m), sigma_le_cap(m);
     sigma_neg = m_bv_util.mk_bv_neg(sigma);
     sigma_cap = m_bv_util.mk_numeral(sbits+2, sigma_size);
-    m_simp.mk_ite(m_bv_util.mk_sle(sigma_neg, sigma_cap), sigma_neg, sigma_cap, sigma_neg_capped);
+    sigma_le_cap = m_bv_util.mk_sle(sigma_neg, sigma_cap);
+    m_simp.mk_ite(sigma_le_cap, sigma_neg, sigma_cap, sigma_neg_capped);
     dbg_decouple("fpa2bv_rnd_sigma_neg", sigma_neg);
     dbg_decouple("fpa2bv_rnd_sigma_neg_capped", sigma_neg_capped);
     sigma_lt_zero = m_bv_util.mk_sle(sigma, m_bv_util.mk_numeral(-1, sigma_size));
@@ -1826,13 +1893,17 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
     SASSERT(is_well_sorted(m, sig));
 
     // put the sticky bit into the significand.
-	expr * tmp[] = { sig, m_bv_util.mk_zero_extend(sbits+1, sticky) };
+    expr_ref ext_sticky(m);
+    ext_sticky = m_bv_util.mk_zero_extend(sbits+1, sticky);
+    expr * tmp[] = { sig, ext_sticky };
     sig = m_bv_util.mk_bv_or(2, tmp);
     SASSERT(is_well_sorted(m, sig));
     SASSERT(m_bv_util.get_bv_size(sig) == sbits+2);    
     
     // CMW: The (OVF1 && OVFen) and (TINY && UNFen) cases are never taken.
-	m_simp.mk_ite(TINY, m_bv_util.mk_zero_extend(2, e_min), beta, exp);
+    expr_ref ext_emin(m);
+    ext_emin = m_bv_util.mk_zero_extend(2, e_min);
+    m_simp.mk_ite(TINY, ext_emin, beta, exp);
     SASSERT(is_well_sorted(m, exp));
 
     // Significand rounding
@@ -1849,13 +1920,18 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
 
     sig = m_bv_util.mk_extract(sbits+1, 2, sig);
 
+    expr_ref last_or_sticky(m), round_or_sticky(m), not_round(m), not_lors(m), not_rors(m), not_sgn(m);
     expr * last_sticky[2] = { last, sticky };
     expr * round_sticky[2] = { round, sticky };        
-	expr * last_or_sticky = m_bv_util.mk_bv_or(2, last_sticky);
+    last_or_sticky = m_bv_util.mk_bv_or(2, last_sticky);
-	expr * round_or_sticky = m_bv_util.mk_bv_or(2, round_sticky); 
+    round_or_sticky = m_bv_util.mk_bv_or(2, round_sticky); 
-	expr * round_lors[2] = { m_bv_util.mk_bv_not(round), m_bv_util.mk_bv_not(last_or_sticky) };	
+    not_round = m_bv_util.mk_bv_not(round);
-	expr * pos_args[2] = { sgn, m_bv_util.mk_bv_not(round_or_sticky) };
+    not_lors = m_bv_util.mk_bv_not(last_or_sticky);
-	expr * neg_args[2] = { m_bv_util.mk_bv_not(sgn), m_bv_util.mk_bv_not(round_or_sticky) };
+    not_rors = m_bv_util.mk_bv_not(round_or_sticky);
+    not_sgn = m_bv_util.mk_bv_not(sgn);
+    expr * round_lors[2] = { not_round, not_lors };    
+    expr * pos_args[2] = { sgn, not_rors };
+    expr * neg_args[2] = { not_sgn, not_rors };
 
     expr_ref inc_teven(m), inc_taway(m), inc_pos(m), inc_neg(m);
     inc_teven = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, round_lors));
@@ -1864,12 +1940,13 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
     inc_neg = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, neg_args));
 
     expr_ref inc(m), inc_c2(m), inc_c3(m), inc_c4(m);
-    expr_ref rm_is_to_neg(m), rm_is_to_pos(m), rm_is_away(m), rm_is_even(m);
+    expr_ref rm_is_to_neg(m), rm_is_to_pos(m), rm_is_away(m), rm_is_even(m), nil_1(m);
+    nil_1 = m_bv_util.mk_numeral(0, 1);
     mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
     mk_is_rm(rm, BV_RM_TO_POSITIVE, rm_is_to_pos);
     mk_is_rm(rm, BV_RM_TIES_TO_AWAY, rm_is_away);
     mk_is_rm(rm, BV_RM_TIES_TO_EVEN, rm_is_even);
-    m_simp.mk_ite(rm_is_to_neg, inc_neg, m_bv_util.mk_numeral(0, 1), inc_c4);
+    m_simp.mk_ite(rm_is_to_neg, inc_neg, nil_1, inc_c4);
     m_simp.mk_ite(rm_is_to_pos, inc_pos, inc_c4, inc_c3);
     m_simp.mk_ite(rm_is_away, inc_taway, inc_c3, inc_c2);
     m_simp.mk_ite(rm_is_even, inc_teven, inc_c2, inc);
@@ -1885,21 +1962,21 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
     // Post normalization    
     SASSERT(m_bv_util.get_bv_size(sig) == sbits + 1);
     expr_ref SIGovf(m);
-    m_simp.mk_eq(m_bv_util.mk_extract(sbits, sbits, sig), m_bv_util.mk_numeral(1, 1), SIGovf);
+    t_sig = m_bv_util.mk_extract(sbits, sbits, sig);
+    m_simp.mk_eq(t_sig, one_1, SIGovf);
     SASSERT(is_well_sorted(m, SIGovf));    
     dbg_decouple("fpa2bv_rnd_SIGovf", SIGovf);
 
-	m_simp.mk_ite(SIGovf,
+    expr_ref hallbut1_sig(m), lallbut1_sig(m);
-				  m_bv_util.mk_extract(sbits, 1, sig),
+    hallbut1_sig = m_bv_util.mk_extract(sbits, 1, sig);
-				  m_bv_util.mk_extract(sbits-1, 0, sig), 
+    lallbut1_sig = m_bv_util.mk_extract(sbits-1, 0, sig);
-                  sig);
+    m_simp.mk_ite(SIGovf, hallbut1_sig, lallbut1_sig, sig);
 
     SASSERT(m_bv_util.get_bv_size(exp) == ebits + 2);
 
-	m_simp.mk_ite(SIGovf, 
+    expr_ref exp_p1(m);
-				  m_bv_util.mk_bv_add(exp, m_bv_util.mk_numeral(1, ebits+2)),
+    exp_p1 = m_bv_util.mk_bv_add(exp, m_bv_util.mk_numeral(1, ebits+2));
-				  exp,
+    m_simp.mk_ite(SIGovf, exp_p1, exp, exp);
-                  exp);
 
     SASSERT(is_well_sorted(m, sig));
     SASSERT(is_well_sorted(m, exp));
@@ -1920,12 +1997,12 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
     SASSERT(is_well_sorted(m, OVF1));
     SASSERT(m.is_bool(OVF1));
 
-    expr_ref preOVF2(m), OVF2(m), OVF(m);
+    expr_ref preOVF2(m), OVF2(m), OVF(m), exp_redand(m), pem2m1(m);
-    m_simp.mk_eq(m.mk_app(m_bv_util.get_fid(), OP_BREDAND, biased_exp.get()), m_bv_util.mk_numeral(1, 1), preOVF2);
+    exp_redand = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, biased_exp.get());
+    m_simp.mk_eq(exp_redand, one_1, preOVF2);
     m_simp.mk_and(SIGovf, preOVF2, OVF2);
-    m_simp.mk_ite(OVF2, m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-2), ebits),
+    pem2m1 = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-2), ebits);
-                        biased_exp,
+    m_simp.mk_ite(OVF2, pem2m1, biased_exp, biased_exp);
-                        biased_exp);
     m_simp.mk_or(OVF1, OVF2, OVF);
     
     SASSERT(is_well_sorted(m, OVF2));
@@ -1962,15 +2039,17 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
     m_simp.mk_ite(rm_zero_or_neg, max_exp, inf_exp, max_inf_exp_neg);
     m_simp.mk_ite(rm_zero_or_pos, max_exp, inf_exp, max_inf_exp_pos);
     m_simp.mk_ite(sgn_is_zero, max_inf_exp_neg, max_inf_exp_pos, ovfl_exp);
-    m_simp.mk_eq(m_bv_util.mk_extract(sbits-1, sbits-1, sig), m_bv_util.mk_numeral(0, 1), n_d_check);
+    t_sig = m_bv_util.mk_extract(sbits-1, sbits-1, sig);
+    m_simp.mk_eq(t_sig, nil_1, n_d_check);
     m_simp.mk_ite(n_d_check, bot_exp /* denormal */, biased_exp, n_d_exp);
     m_simp.mk_ite(OVF, ovfl_exp, n_d_exp, exp);
 
-    expr_ref max_inf_sig_neg(m), max_inf_sig_pos(m), ovfl_sig(m);
+    expr_ref max_inf_sig_neg(m), max_inf_sig_pos(m), ovfl_sig(m), rest_sig(m);
     m_simp.mk_ite(rm_zero_or_neg, max_sig, inf_sig, max_inf_sig_neg);
     m_simp.mk_ite(rm_zero_or_pos, max_sig, inf_sig, max_inf_sig_pos);
     m_simp.mk_ite(sgn_is_zero, max_inf_sig_neg, max_inf_sig_pos, ovfl_sig);
-    m_simp.mk_ite(OVF, ovfl_sig, m_bv_util.mk_extract(sbits-2, 0, sig), sig);
+    rest_sig = m_bv_util.mk_extract(sbits-2, 0, sig);
+    m_simp.mk_ite(OVF, ovfl_sig, rest_sig, sig);
 
     dbg_decouple("fpa2bv_rnd_sgn_final", sgn);
     dbg_decouple("fpa2bv_rnd_sig_final", sig);
@@ -1993,11 +2072,6 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
     TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; );
 }
 
-
-fpa2bv_model_converter * fpa2bv_converter::mk_model_converter() {
-    return alloc(fpa2bv_model_converter, m, m_const2bv, m_rm_const2bv);
-}
-
 void fpa2bv_model_converter::display(std::ostream & out) {
     out << "(fpa2bv-model-converter";
     for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
@@ -2024,11 +2098,23 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator
     for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
          it != m_const2bv.end();
          it++)
-        res->m_const2bv.insert(translator(it->m_key), translator(it->m_value));    
+    {
+        func_decl * k = translator(it->m_key);
+        expr * v = translator(it->m_value);
+        res->m_const2bv.insert(k, v);
+        translator.to().inc_ref(k);
+        translator.to().inc_ref(v);
+    }
     for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
          it != m_rm_const2bv.end();
          it++)
-        res->m_rm_const2bv.insert(translator(it->m_key), translator(it->m_value));    
+    {
+        func_decl * k = translator(it->m_key);
+        expr * v = translator(it->m_value);
+        res->m_rm_const2bv.insert(k, v);
+        translator.to().inc_ref(k);
+        translator.to().inc_ref(v);        
+    }
     return res;
 }
 
@@ -2135,7 +2221,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
         float_mdl->register_decl(c, bv_mdl->get_const_interp(c));
     }
 
-    // And keep everything else
+// And keep everything else
     sz = bv_mdl->get_num_functions();
     for (unsigned i = 0; i < sz; i++)
     {
@@ -2151,3 +2237,9 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
         float_mdl->register_usort(s, u.size(), u.c_ptr());
     }
 }
+
+model_converter * mk_fpa2bv_model_converter(ast_manager & m, 
+                                            obj_map<func_decl, expr*> const & const2bv,
+                                            obj_map<func_decl, expr*> const & rm_const2bv) {
+    return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv);
+}

src/tactic/fpa/fpa2bv_converter.h

@@ -102,7 +102,8 @@ public:
     void mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
 
-    fpa2bv_model_converter * mk_model_converter();
+    obj_map<func_decl, expr*> const & const2bv() const { return m_const2bv; }
+    obj_map<func_decl, expr*> const & rm_const2bv() const { return m_rm_const2bv; }
 
     void dbg_decouple(const char * prefix, expr_ref & e);
     expr_ref_vector extra_assertions;
@@ -149,8 +150,8 @@ class fpa2bv_model_converter : public model_converter {
     obj_map<func_decl, expr*>   m_rm_const2bv;
 
 public:
-    fpa2bv_model_converter(ast_manager & m, obj_map<func_decl, expr*> & const2bv,
+    fpa2bv_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bv,
-		                                    obj_map<func_decl, expr*> & rm_const2bv) : 
+                                            obj_map<func_decl, expr*> const & rm_const2bv) : 
       m(m) {
           // Just create a copy?
           for (obj_map<func_decl, expr*>::iterator it = const2bv.begin();
@@ -198,4 +199,9 @@ protected:
     void convert(model * bv_mdl, model * float_mdl);
 };
 
+
+model_converter * mk_fpa2bv_model_converter(ast_manager & m, 
+                                            obj_map<func_decl, expr*> const & const2bv,
+                                            obj_map<func_decl, expr*> const & rm_const2bv);
+
 #endif

src/tactic/fpa/fpa2bv_tactic.cpp

@@ -90,7 +90,7 @@ class fpa2bv_tactic : public tactic {
             }
 
             if (g->models_enabled())  
-                mc = m_conv.mk_model_converter();
+                mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv());
 
             g->inc_depth();
             result.push_back(g.get());