mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00
Code Activity

fix #5993

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-04-23 19:33:55 +01:00
parent 8e509d34b5
commit 459cfc8eb4
1 changed files with 14 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -95,7 +95,16 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
}
void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) {
if (m_util.is_fp(t) && m_util.is_fp(f)) {
expr* c2 = nullptr, *t2 = nullptr, *f2 = nullptr;
if (m.is_ite(t, c2, t2, f2)) {
mk_ite(c2, t2, f2, result);
mk_ite(c, result, f, result);
}
else if (m.is_ite(f, c2, t2, f2)) {
mk_ite(c2, t2, f2, result);
mk_ite(c, t, result, result);
}
else if (m_util.is_fp(t) && m_util.is_fp(f)) {
expr_ref t_sgn(m), t_sig(m), t_exp(m);
expr_ref f_sgn(m), f_sig(m), f_exp(m);
split_fp(t, t_sgn, t_exp, t_sig);
@ -115,8 +124,11 @@ void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) {
m_simp.mk_ite(c, to_app(t)->get_arg(0), to_app(f)->get_arg(0), result);
result = m_util.mk_bv2rm(result);
}
else
else {
std::cout << mk_pp(t, m) << " " << mk_pp(f, m) << "\n";
UNREACHABLE();
}
}
void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {