mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

fix crash in BV internalizer due to unknown bv_neg symbol

Browse source
This commit is contained in:
Nuno Lopes 2019-11-16 16:24:24 +00:00
parent cb600a9329
commit b9bc6975e9
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -773,7 +773,7 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu
if (m_fm.is_nan(v)) { if (m_fm.is_nan(v)) {
if (m_hi_fp_unspecified) { if (m_hi_fp_unspecified) {
expr * args[4] = { bu.mk_numeral(0, 1), expr * args[4] = { bu.mk_numeral(0, 1),
bu.mk_bv_neg(bu.mk_numeral(1, x.get_ebits())), bu.mk_numeral(rational::minus_one(), x.get_ebits()),
bu.mk_numeral(0, x.get_sbits() - 2), bu.mk_numeral(0, x.get_sbits() - 2),
bu.mk_numeral(1, 1) }; bu.mk_numeral(1, 1) };
result = bu.mk_concat(4, args); result = bu.mk_concat(4, args);