From bea7bc5e30170694af655bc244a4dd9b8da1b2d8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 26 Oct 2016 16:32:44 +0100 Subject: [PATCH] Bugfix for bv2fpa_converter. Fixes #767. --- src/ast/fpa/bv2fpa_converter.cpp | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 07a24e40a..0dec98e5c 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -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);