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 bv2fpa_converter. Fixes #767.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-10-26 16:32:44 +01:00
parent e381cef92c
commit bea7bc5e30
1 changed files with 11 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/ast/fpa/bv2fpa_converter.cpp
View file

@ -322,10 +322,17 @@ void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model
v2 = mc->get_const_interp(a2->get_decl());
#else
expr * bv = mc->get_const_interp(to_app(to_app(a0)->get_arg(0))->get_decl());
unsigned bv_sz = m_bv_util.get_bv_size(bv);
v0 = m_bv_util.mk_extract(bv_sz-1, bv_sz-1, bv);
v1 = m_bv_util.mk_extract(bv_sz-2, sbits-1, bv);
v2 = m_bv_util.mk_extract(sbits-2, 0, bv);
if (bv == 0) {
v0 = m_bv_util.mk_numeral(0, 1);
v1 = m_bv_util.mk_numeral(0, ebits);
v2 = m_bv_util.mk_numeral(0, sbits-1);
}
else {
unsigned bv_sz = m_bv_util.get_bv_size(bv);
v0 = m_bv_util.mk_extract(bv_sz-1, bv_sz-1, bv);
v1 = m_bv_util.mk_extract(bv_sz-2, sbits-1, bv);
v2 = m_bv_util.mk_extract(sbits-2, 0, bv);
}
#endif
if (!v0) v0 = m_bv_util.mk_numeral(0, 1);