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.to_sbv

Browse source 
Fixes #162
This commit is contained in:
Christoph M. Wintersteiger 2015-09-17 12:21:59 +01:00
parent e9565d6a7f
commit 4d39108808
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/fpa/fpa2bv_converter.cpp
View file

@ -2876,7 +2876,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
else else
c_in_limits = m.mk_or(m_bv_util.mk_sle(m_bv_util.mk_numeral(1, ebits + 2), shift), c_in_limits = m.mk_or(m_bv_util.mk_sle(m_bv_util.mk_numeral(1, ebits + 2), shift),
m.mk_and(m.mk_eq(m_bv_util.mk_numeral(0, ebits + 2), shift), m.mk_and(m.mk_eq(m_bv_util.mk_numeral(0, ebits + 2), shift),
m.mk_eq(sig, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, sbits-1))))); m.mk_eq(sig, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, sig_sz-1)))));
dbg_decouple("fpa2bv_to_bv_in_limits", c_in_limits); dbg_decouple("fpa2bv_to_bv_in_limits", c_in_limits);
expr_ref r_shifted_sig(m), l_shifted_sig(m); expr_ref r_shifted_sig(m), l_shifted_sig(m);