fix #3199

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/ast.cpp

@@ -1800,7 +1800,7 @@ static void track_id(ast* n, unsigned id) {
     if (n->get_id() != id) return;
     ++s_count;
     std::cout << s_count << "\n";
-    //SASSERT(s_count != 1);
+    //SASSERT(s_count != 2);
 }
 #endif
 
@@ -1834,7 +1834,7 @@ ast * ast_manager::register_node_core(ast * n) {
 
     n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
 
-    //track_id(n, 1354);
+    // track_id(n, 48);
 
     TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
     TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);

src/ast/fpa/bv2fpa_converter.cpp

@@ -101,14 +101,13 @@ expr_ref bv2fpa_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp, expr
     rational exp_unbiased_q;
     exp_unbiased_q = exp_q - m_fpa_util.fm().m_powers2.m1(ebits - 1);
 
-    mpz sig_z; mpf_exp_t exp_z;
+    scoped_mpz sig_z(mpzm); 
+    mpf_exp_t exp_z;
     mpzm.set(sig_z, sig_q.to_mpq().numerator());
     exp_z = mpzm.get_int64(exp_unbiased_q.to_mpq().numerator());
 
     m_fpa_util.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), exp_z, sig_z);
 
-    mpzm.del(sig_z);
-
     res = m_fpa_util.mk_value(fp_val);
 
     TRACE("bv2fpa", tout << "[" << mk_ismt2_pp(sgn, m) <<
@@ -257,7 +256,7 @@ bv2fpa_converter::array_model bv2fpa_converter::convert_array_func_interp(model_
 
 func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl * f, func_decl * bv_f) {
     SASSERT(f->get_arity() > 0);
-    func_interp * result = nullptr;
+    scoped_ptr<func_interp> result = nullptr;
     sort * rng = f->get_range();
     sort * const * dmn = f->get_domain();
 
@@ -322,7 +321,7 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
         }
     }
 
-    return result;
+    return result.detach();
 }
 
 void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model, obj_hashtable<func_decl> & seen) {
@@ -444,8 +443,7 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode
         func_decl * f_uf = kv.m_value;
         seen.insert(f_uf);
 
-        if (f->get_arity() == 0)
-        {
+        if (f->get_arity() == 0) {
             array_util au(m);
             if (au.is_array(f->get_range())) {
                 array_model am = convert_array_func_interp(mc, f, f_uf);

src/ast/fpa_decl_plugin.cpp

@@ -1073,12 +1073,12 @@ bool fpa_util::is_considered_uninterpreted(func_decl * f, unsigned n, expr* cons
         expr* x = args[1];
         unsigned bv_sz = f->get_parameter(0).get_int();
         mpf_rounding_mode rmv;
-        mpf v;
-        if (!is_rm_numeral(rm, rmv) || !is_numeral(x, v)) return false;
+        scoped_mpf sv(fm());
+        if (!is_rm_numeral(rm, rmv) || !is_numeral(x, sv)) return false;
         if (is_nan(x) || is_inf(x)) return true;
         unsynch_mpq_manager& mpqm = plugin().fm().mpq_manager();
         scoped_mpq r(mpqm);
-        plugin().fm().to_sbv_mpq(rmv, v, r);
+        plugin().fm().to_sbv_mpq(rmv, sv, r);
         if (is_signed)
             return mpqm.bitsize(r) >= bv_sz;
         else

src/tactic/fpa/fpa2bv_model_converter.h

@@ -38,8 +38,8 @@ public:
     }
 
     void operator()(model_ref & md) override {
-        model * new_model = alloc(model, m);
-        convert(md.get(), new_model);
+        model_ref new_model = alloc(model, m);
+        convert(md.get(), new_model.get());
         md = new_model;
     }
 

src/util/mpf.cpp

@@ -1189,6 +1189,8 @@ void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o
 
     set(t, x);
     unpack(t, true);
+    if (t.exponent() >= INT_MAX)
+        throw default_exception("exponents over 31 bits are not supported");
 
     SASSERT(t.exponent() < INT_MAX);