From eacde16b3e32015edc3bdc0262ecb238971b089b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 4 Apr 2020 23:55:44 -0700
Subject: [PATCH] fix #3199
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/ast.cpp | 4 ++--
src/ast/fpa/bv2fpa_converter.cpp | 12 +++++-------
src/ast/fpa_decl_plugin.cpp | 6 +++---
src/tactic/fpa/fpa2bv_model_converter.h | 4 ++--
src/util/mpf.cpp | 2 ++
5 files changed, 14 insertions(+), 14 deletions(-)
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 871056f6b..50dd3d6eb 100644
--- a/src/ast/ast.cpp
+++ b/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";);
diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp
index d4fd3d5f1..3e05fedcc 100644
--- a/src/ast/fpa/bv2fpa_converter.cpp
+++ b/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);
diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp
index 7b8cde038..941140a82 100644
--- a/src/ast/fpa_decl_plugin.cpp
+++ b/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
diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h
index 2020657b7..cad7888e3 100644
--- a/src/tactic/fpa/fpa2bv_model_converter.h
+++ b/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;
}
diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp
index df0b8fd3b..cdd8f5f3e 100644
--- a/src/util/mpf.cpp
+++ b/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);