Чтение функционального интервала массива z3 из модели z3

Предположим, у меня есть 2 массива в формуле, выполнимость которых я хочу проверить, используя z3. Если z3 возвращает sat, я хочу прочитать первый массив в модели z3 и довольно распечатать его как ключ, пару значений и значение по умолчанию. Позже я хочу преобразовать его в карту и провести дальнейший анализ. Вот пример, который я запускаю:

void find_model_example_arr() {
std::cout << "find_model_example_involving_array\n";
context c;
sort arr_sort = c.array_sort(c.int_sort(), c.int_sort());
expr some_array_1 = c.constant("some_array_1", arr_sort);
expr some_array_2 = c.constant("some_array_2", arr_sort);
solver s(c);

s.add(select(some_array_1, 0) > 0);
s.add(select(some_array_2, 5) < -4);
std::cout << s.check() << "\n";

model m = s.get_model();
std::cout << m << "\n";

expr some_array_1_eval = m.eval(some_array_1);

std::cout << "\nsome_array_1_eval = " << some_array_1_eval << "\n";

func_decl some_array_1_eval_func_decl = some_array_1_eval.decl();
std::cout << "\nThe Z3 expr(fun_decl) for some_array_1_eval is : " << some_array_1_eval_func_decl << "\n";

// ERROR here
func_interp fun_interp = m.get_func_interp(some_array_1_eval_func_decl);
// This works well
//func_interp fun_interp = m.get_func_interp(m.get_func_decl(0));

std::cout << "\nThe Z3 expr(fun_interp) for the array is : " << fun_interp << "\n";

unsigned num_entries = fun_interp.num_entries();
for(unsigned i = 0; i < num_entries; i++)
{
z3::func_entry entry = fun_interp.entry(i);
z3::expr k = entry.arg(0);

z3::expr v = entry.value();

std::cout << "\n(key,value): (" << k << "," << v << ")";
}

z3::expr default_value = fun_interp.else_value();
std::cout << "\nDefault value:" << default_value;
}

Я получаю следующий вывод:

find_model_example_involving_array
sat
(define-fun some_array_1 () (Array Int Int)
(_ as-array k!0))
(define-fun some_array_2 () (Array Int Int)
(_ as-array k!1))
(define-fun k!0 ((x!1 Int)) Int
(ite (= x!1 0) 1
1))
(define-fun k!1 ((x!1 Int)) Int
(ite (= x!1 5) (- 5)
(- 5)))

some_array_1_eval = (_ as-array k!0)

The Z3 expr(fun_decl) for some_array_1_eval is :
(declare-fun as-array () (Array  Int Int))
unexpected error: invalid argument

Вместо этого, если я закомментирую первую строку и использую вторую, т.е. использую следующий блок кода:

// ERROR here
// func_interp fun_interp = m.get_func_interp(some_array_1_eval_func_decl);
// This works well
func_interp fun_interp = m.get_func_interp(m.get_func_decl(0));

Я получаю вывод, который ищу:

(key,value): (0,1)
Default value:1

Вот в чем проблема? Как мне выяснить, что m.get_func_decl (0) — это тот, который соответствует some_array_1? Например, если я использую m.get_func_decl (1), я получаю неправильные пары (ключ, значение). Другими словами, как я могу получить func_interp массива (определенного как выражение z3) из модели?