Function z3_sys::Z3_mk_array_sort

pub unsafe extern "C" fn Z3_mk_array_sort(
    c: Z3_context, 
    domain: Z3_sort, 
    range: Z3_sort
) -> Z3_sort

Create an array type.

We usually represent the array type as: [domain -> range]. Arrays are usually used to model the heap/memory in software verification.

See also:

• Z3_mk_select
• Z3_mk_store