Searched refs:exp_diff_ge_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 | 1135 …expr_ref exp_diff(m), neg_exp_diff(m), exp_diff_is_neg(m), exp_diff_ge_zero(m), exp_diff_is_zero(m… in mk_rem() local
1142 …exp_diff_ge_zero = m_bv_util.mk_sle(m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(exp_diff)), exp_… in mk_rem()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/fpa/ |
| H A D | fpa2bv_converter.cpp | 1134 …expr_ref exp_diff(m), neg_exp_diff(m), exp_diff_is_neg(m), exp_diff_ge_zero(m), exp_diff_is_zero(m…
1141 …exp_diff_ge_zero = m_bv_util.mk_sle(m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(exp_diff)), exp_…
|