mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 06:13:40 +00:00
Code Activity

Removed unnecessary variables.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-10-17 16:33:09 +01:00
parent 707dbd4173
commit 2f6ef0f3be
1 changed files with 1 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3295,8 +3295,6 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
void fpa2bv_converter::mk_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { void fpa2bv_converter::mk_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 0); SASSERT(num == 0);
unsigned ebits = f->get_parameter(0).get_int();
unsigned sbits = f->get_parameter(1).get_int();
unsigned width = m_bv_util.get_bv_size(f->get_range()); unsigned width = m_bv_util.get_bv_size(f->get_range());
if (m_hi_fp_unspecified) if (m_hi_fp_unspecified)
@ -3326,8 +3324,6 @@ expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits,
void fpa2bv_converter::mk_to_sbv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { void fpa2bv_converter::mk_to_sbv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 0); SASSERT(num == 0);
unsigned ebits = f->get_parameter(0).get_int();
unsigned sbits = f->get_parameter(1).get_int();
unsigned width = m_bv_util.get_bv_size(f->get_range()); unsigned width = m_bv_util.get_bv_size(f->get_range());
if (m_hi_fp_unspecified) if (m_hi_fp_unspecified)
@ -3339,7 +3335,7 @@ void fpa2bv_converter::mk_to_sbv_unspecified(func_decl * f, unsigned num, expr *
m_uf2bvuf.insert(f, fd); m_uf2bvuf.insert(f, fd);
m.inc_ref(f); m.inc_ref(f);
m.inc_ref(fd); m.inc_ref(fd);
} }
result = m.mk_const(fd); result = m.mk_const(fd);
} }