MicroTESK

В модели RISC-V в массив памяти с 62-х битным индексом производится запись по индексу размерностью 64 бит, что обрабатывается MicroTESK при компиляции и генерации модели, однако Symexecute не учитывает то, что smt-lib таких неявных преобразований не позволяет. Пример из файла riscv_rv32i.nml (строка 350).

tmp_index = tmp_address >> 2;

if tmp_address<1..0> == 0 then // Word-aligned address
tmp_word = MEM[tmp_index];

Генерация smt по данному коду приводит к ошибке солвера:
(error "array select not indexed with correct type for array")

На всякий случай прикладываю бинарный код.