From 4cb96bfe76a1b63209f42d8186d48ea0929c0f0b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 13 Nov 2015 15:55:01 +0000 Subject: [PATCH] Fixed assertion failure in fpa2bv_converter. Partially addresses #307 --- src/ast/fpa/fpa2bv_converter.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 4ee6366f0..19b07035f 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2648,9 +2648,8 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const SASSERT(num == 2); SASSERT(m_util.is_float(f->get_range())); - SASSERT(m_bv_util.is_bv(args[0])); - SASSERT(m_bv_util.is_bv(args[1])); SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM)); + SASSERT(m_bv_util.is_bv(args[1])); expr_ref bv_rm(m), x(m); bv_rm = to_app(args[0])->get_arg(0);