Создайте массив фиксированного размера и инициализируйте его.

Я собираюсь создать массив фиксированного размера и инициализировать его некоторыми значениями.

Например, следующий код C++:

a[0] = 10;
a[1] = 23;
a[2] = 27;
a[3] = 12;
a[4] = 19;
a[5] = 31;
a[6] = 41;
a[7] = 7;

Есть ли какие-нибудь утилиты в Z3 для его моделирования?