mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

variable naming

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-05-23 15:08:27 +01:00
parent cb6d008da8
commit 184aebab59
1 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1178,10 +1178,10 @@ expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y)
pn = m_util.mk_fp(decls.first, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1));
np = m_util.mk_fp(decls.second, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1));
expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m);
expr_ref x_is_pzero(m), y_is_nzero(m), xyzero(m);
mk_is_pzero(x, x_is_pzero);
mk_is_nzero(y, x_is_nzero);
m_simp.mk_and(x_is_pzero, x_is_nzero, xyzero);
mk_is_nzero(y, y_is_nzero);
m_simp.mk_and(x_is_pzero, y_is_nzero, xyzero);
mk_ite(xyzero, pn, np, res);
return res;
@ -1259,10 +1259,10 @@ expr_ref fpa2bv_converter::mk_max_unspecified(func_decl * f, expr * x, expr * y)
pn = m_util.mk_fp(decls.first, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1));
np = m_util.mk_fp(decls.second, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1));
expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m);
expr_ref x_is_pzero(m), y_is_nzero(m), xyzero(m);
mk_is_pzero(x, x_is_pzero);
mk_is_nzero(y, x_is_nzero);
m_simp.mk_and(x_is_pzero, x_is_nzero, xyzero);
mk_is_nzero(y, y_is_nzero);
m_simp.mk_and(x_is_pzero, y_is_nzero, xyzero);
mk_ite(xyzero, pn, np, res);
return res;