mk_eq method

Z3_ast mk_eq(Z3_context c, Z3_ast l, Z3_ast r)

\brief Create an AST node representing \ccode{l = r}.

The nodes \c l and \c r must have the same type.

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

Implementation

Z3_ast mk_eq(
  Z3_context c,
  Z3_ast l,
  Z3_ast r,
) {
  return _mk_eq(
    c,
    l,
    r,
  );
}