Я пытаюсь запустить последнюю версию CVC4 (1.6 на ма c os) на конечных моделях при поиске эталонов, найденных по адресу:
https://cvc4.github.io/papers/cav2013-fmf
https://cvc4.github.io/papers/cade2013-qifmf
Запуск cvc4 --finite-model-find german155.smt2 приводит к:
(error "Parse Error: german155.smt2:3.24: Too many datatypes defined in this block.
(declare-datatypes () ((UNIT (Unit))))
^
")
И это происходит для каждого файла в тесты, которые я пробовал.
Эти тесты больше нельзя использовать с CVC4?