peephole for isNaN
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -748,8 +748,8 @@ static StateValue fm_poison(State &s, const expr &a, const expr &ap,
bool only_input = false,
bool flush_denormal = true,
bool convert_output_bv = true) {
- return fm_poison(s, a, ap, std::move(b), bp, expr(), expr(),
- [&](auto &a, auto &b, auto &c) { return fn(a, b); },
+ return fm_poison(s, a, ap, b, bp, expr(), expr(),
+ [fn](auto &a, auto &b, auto &c) { return fn(a, b); },
ty, fmath, only_input, flush_denormal, convert_output_bv, 2);
}
@@ -759,7 +759,7 @@ static StateValue fm_poison(State &s, const expr &a, const expr &ap,
bool flush_denormal = true,
bool convert_output_bv = true) {
return fm_poison(s, a, ap, expr(), expr(), expr(), expr(),
- [&](auto &a, auto &b, auto &c) { return fn(a); },
+ [fn](auto &a, auto &b, auto &c) { return fn(a); },
ty, fmath, only_input, flush_denormal,
convert_output_bv, 1);
}

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1057,6 +1057,8 @@ expr expr::abs() const {
expr cond, neg, v, v2; \
if (isIf(cond, neg, v) && neg.isFPNeg(v2) && v.eq(v2)) \
return v.fn(); \
+ if (isFPNeg(v)) \
+ return v.fn(); \
} while (0)
expr expr::isNaN() const {
@@ -1070,7 +1072,6 @@ expr expr::isInf() const {
}
expr expr::isFPZero() const {
- fold_fp_neg(isFPZero);
return unop_fold(Z3_mk_fpa_is_zero);
}

peephole for isNaN