mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Bugfix for FPA UFs

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-10-08 14:14:39 +01:00
parent c787ea1a3b
commit 883514c195
1 changed files with 14 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/ast/fpa/fpa2bv_rewriter.h
View file

@ -81,11 +81,16 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
if (f->get_family_id() == null_family_id) { if (f->get_family_id() == null_family_id) {
if (num == 0) { if (num == 0) {
if (m_conv.is_float(f->get_range())) if (m_conv.is_float(f->get_range())) {
m_conv.mk_const(f, result); m_conv.mk_const(f, result);
else if (m_conv.is_rm(f->get_range())) return BR_DONE;
}
else if (m_conv.is_rm(f->get_range())) {
m_conv.mk_rm_const(f, result); m_conv.mk_rm_const(f, result);
return BR_DONE; return BR_DONE;
}
else
return BR_FAILED;
} }
else { else {
bool is_float_uf = m_conv.is_float(f->get_range()) || m_conv.is_rm(f->get_range()); bool is_float_uf = m_conv.is_float(f->get_range()) || m_conv.is_rm(f->get_range());
@ -95,11 +100,13 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
is_float_uf |= m_conv.is_float(di) || m_conv.is_rm(di); is_float_uf |= m_conv.is_float(di) || m_conv.is_rm(di);
} }
if (is_float_uf) if (is_float_uf) {
m_conv.mk_uninterpreted_function(f, num, args, result); m_conv.mk_uninterpreted_function(f, num, args, result);
return BR_DONE;
return BR_DONE; }
} else
return BR_FAILED;
}
} }
if (m().is_eq(f)) { if (m().is_eq(f)) {