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

Fixed assertion failure in fpa2bv_converter.

Browse source 
Partially addresses #307
This commit is contained in:
Christoph M. Wintersteiger 2015-11-13 15:55:01 +00:00
parent 806016c315
commit 4cb96bfe76
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -2648,9 +2648,8 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
SASSERT(num == 2); SASSERT(num == 2);
SASSERT(m_util.is_float(f->get_range())); 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(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); expr_ref bv_rm(m), x(m);
bv_rm = to_app(args[0])->get_arg(0); bv_rm = to_app(args[0])->get_arg(0);