Method isNaNCheck

smt/expr.cpp:635–641

}

bool expr::isNaNCheck(expr &fp) const {
  if (auto app = isAppOf(Z3_OP_FPA_IS_NAN)) {
    fp = Z3_get_app_arg(ctx(), app, 0);
    return true;
  }
  return false;
}

bool expr::isfloat2BV(expr &fp) const {
  return isUnOp(fp, Z3_OP_FPA_TO_IEEE_BV);