From f5ff9fae3477850d849d217193857f37c2ee5e0d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 17 Nov 2017 21:15:30 +0000 Subject: [PATCH] Fixed bug check in bv2fpa converter. Fixes #1291. --- src/ast/fpa/bv2fpa_converter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 2f5a7c3c1..d87929864 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -297,7 +297,7 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl * // The BV model may have multiple equivalent entries using different // representations of NaN. We can only keep one and we check that // the results for all those entries are the same. - if (ft_fres != fe->get_result()) + if (m_fpa_util.is_float(rng) && ft_fres != fe->get_result()) throw default_exception("BUG: UF function entries disagree with each other"); } }