mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
commit
d9e4648d8d
|
@ -923,7 +923,8 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
|
|||
m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext));
|
||||
|
||||
expr_ref quotient(m);
|
||||
quotient = m.mk_app(m_bv_util.get_fid(), OP_BUDIV, a_sig_ext, b_sig_ext);
|
||||
// b_sig_ext can't be 0 here, so it's safe to use OP_BUDIV_I
|
||||
quotient = m.mk_app(m_bv_util.get_fid(), OP_BUDIV_I, a_sig_ext, b_sig_ext);
|
||||
|
||||
dbg_decouple("fpa2bv_div_quotient", quotient);
|
||||
|
||||
|
|
|
@ -384,7 +384,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
|
|||
if (!seen.contains(f))
|
||||
{
|
||||
TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl;);
|
||||
func_interp * val = bv_mdl->get_func_interp(f);
|
||||
func_interp * val = bv_mdl->get_func_interp(f)->copy();
|
||||
float_mdl->register_decl(f, val);
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue