Method lambdaIdxType

smt/expr.cpp:577–581

}

expr expr::lambdaIdxType() const {
  C();
  assert(Z3_get_quantifier_num_bound(ctx(), ast()) == 1);
  return ::mkVar("sort", Z3_get_quantifier_bound_sort(ctx(), ast(), 0));
}

bool expr::isFPAdd(expr &rounding, expr &lhs, expr &rhs) const {
  return isTernaryOp(rounding, lhs, rhs, Z3_OP_FPA_ADD);