Searched refs:ye_neq_zero (Results 1 – 2 of 2) sorted by relevance
| /dports/math/z3/z3-z3-4.8.13/src/ast/fpa/ |
| H A D | fpa2bv_converter.cpp | 1096 expr_ref one_ebits(m), y_exp_m1(m), xe_lt_yem1(m), ye_neq_zero(m); in mk_rem() local
1100 ye_neq_zero = m.mk_not(m.mk_eq(y_exp, m_bv_util.mk_numeral(0, ebits))); in mk_rem()
1101 c6 = m.mk_and(ye_neq_zero, xe_lt_yem1); in mk_rem()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/fpa/ |
| H A D | fpa2bv_converter.cpp | 1095 expr_ref one_ebits(m), y_exp_m1(m), xe_lt_yem1(m), ye_neq_zero(m);
1099 ye_neq_zero = m.mk_not(m.mk_eq(y_exp, m_bv_util.mk_numeral(0, ebits)));
1100 c6 = m.mk_and(ye_neq_zero, xe_lt_yem1);
|