mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-30 04:15:51 +00:00
Code Activity

Fixed bug check in bv2fpa converter. Fixes #1291.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-11-17 21:15:30 +00:00
parent 9ef54d7a16
commit f5ff9fae34
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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");
}
}