message: smt expr: optimize FP (if cond (neg x) x) for some ops:
  isNaN, isInf, isFPZero, fabs
  These show up with fast-math
diff: @@ -979,15 +979,25 @@ expr expr::abs() const {
  return mkIf(sge(mkUInt(0, s)), *this, mkInt(-1, s) * *this);
  }
  +#define fold_fp_neg(fn) \
  + do { \
  + expr cond, neg, v, v2; \
  + if (isIf(cond, neg, v) && neg.isFPNeg(v2) && v.eq(v2)) \
  + return v.fn(); \
  +} while (0)
  +
  expr expr::isNaN() const {
  + fold_fp_neg(isNaN);
  return unop_fold(Z3_mk_fpa_is_nan);
  }
  expr expr::isInf() const {
  + fold_fp_neg(isInf);
  return unop_fold(Z3_mk_fpa_is_infinite);
  }
  expr expr::isFPZero() const {
  + fold_fp_neg(isFPZero);
  return unop_fold(Z3_mk_fpa_is_zero);
  }
  @@ -1040,6 +1050,7 @@ expr expr::fdiv(const expr &rhs, const expr &rm) const {
  }
  expr expr::fabs() const {
  + fold_fp_neg(fabs);
  return unop_fold(Z3_mk_fpa_abs);
  }
  