mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

Add missing FP conversion. Fixes #4470.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2020-07-08 17:56:25 +00:00
parent 688d38d868
commit c59519bf9c
No known key found for this signature in database
GPG key ID: BCF6360F86294467
1 changed files with 12 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -2429,6 +2429,18 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
// rm + real + int -> float
mk_to_fp_real_int(f, num, args, result);
}
else if (num == 3 &&
m_util.is_rm(args[0]) &&
m_arith_util.is_int_real(args[1]) &&
m_arith_util.is_int_real(args[2]))
{
expr_ref sig(m), exp(m), two(m), v(m);
sig = args[1];
exp = args[2];
two = m_arith_util.mk_numeral(rational(2), true);
v = m_arith_util.mk_mul(sig, m_arith_util.mk_power(two, exp));
mk_to_fp_real(f, f->get_range(), args[0], v, result);
}
else
UNREACHABLE();