stp.K

stp.K(sort, element)

A constant array. K(ArraySort(I, E), literal_or_value) coerces the literal by the array’s element sort; K(index_sort, value) is z3py’s form (the range sort is the value’s). The element may be symbolic; every index has the same element value. Defaults with UF applications, Real terms or array-equality conditions raise Unsupported.