From c051876e3f92058186459a61f00cb0ebaa75dee0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 31 Jan 2013 12:49:43 +0000 Subject: [PATCH] FPA bugfix Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/fpa2bv_converter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 41871f3e1..4afdc501f 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1641,7 +1641,7 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref SASSERT(is_well_sorted(m, is_sig_zero)); SASSERT(is_well_sorted(m, lz)); SASSERT(is_well_sorted(m, shift)); - if (ebits > sbits) { + if (ebits < sbits) { expr_ref q(m); q = m_bv_util.mk_zero_extend(sbits-ebits, shift); denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, q);