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 FP rewriter.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-09-15 16:23:24 +01:00
parent 406cd00b3a
commit a1073206f9
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -739,7 +739,7 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_
m_util.is_numeral(arg2, v)) { m_util.is_numeral(arg2, v)) {
if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v)) { if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v)) {
result = m_util.mk_internal_to_ubv_unspecified(bv_sz); mk_to_ubv_unspecified(f, result);
return BR_REWRITE_FULL; return BR_REWRITE_FULL;
} }
@ -754,7 +754,7 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_
if (r >= ll && r <= ul) if (r >= ll && r <= ul)
result = bu.mk_numeral(r, bv_sz); result = bu.mk_numeral(r, bv_sz);
else else
result = m_util.mk_internal_to_ubv_unspecified(bv_sz); mk_to_ubv_unspecified(f, result);
return BR_DONE; return BR_DONE;
} }
@ -772,7 +772,7 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
m_util.is_numeral(arg2, v)) { m_util.is_numeral(arg2, v)) {
if (m_fm.is_nan(v) || m_fm.is_inf(v)) { if (m_fm.is_nan(v) || m_fm.is_inf(v)) {
result = m_util.mk_internal_to_sbv_unspecified(bv_sz); mk_to_sbv_unspecified(f, result);
return BR_REWRITE_FULL; return BR_REWRITE_FULL;
} }
@ -787,7 +787,7 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
if (r >= ll && r <= ul) if (r >= ll && r <= ul)
result = bu.mk_numeral(r, bv_sz); result = bu.mk_numeral(r, bv_sz);
else else
result = m_util.mk_internal_to_sbv_unspecified(bv_sz); mk_to_sbv_unspecified(f, result);
return BR_DONE; return BR_DONE;
} }