mk_div method

Z3_ast mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)

\brief Create an AST node representing \ccode{arg1 div arg2}.

The arguments must either both have int type or both have real type. If the arguments have int type, then the result type is an int type, otherwise the the result type is real.

def_API('Z3_mk_div', AST, (_in(CONTEXT), _in(AST), _in(AST)))

Implementation

Z3_ast mk_div(
  Z3_context c,
  Z3_ast arg1,
  Z3_ast arg2,
) {
  return _mk_div(
    c,
    arg1,
    arg2,
  );
}