mk_array_default method

Z3_ast mk_array_default(
  1. Z3_context c,
  2. Z3_ast array
)

\brief Access the array default value. Produces the default range value, for arrays that can be represented as finite maps with a default range value.

\param c logical context. \param array array value whose default range value is accessed.

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

Implementation

Z3_ast mk_array_default(
  Z3_context c,
  Z3_ast array,
) {
  return _mk_array_default(
    c,
    array,
  );
}