Я успешно написал проверенную программу Dafny, которая по массиву целых чисел возвращает длину самого длинного монотонного префикса. Постоянная ссылка здесь. Я хочу иметь возможность проверить файл SMT, который использовал Дафни, даже если в нем не было ошибок. Я пробовал различные варианты флагов, такие как:
$ dafny example_longest_monotone.dfy /useSmtOutputFormat /printModelToFile:smt_file.smt
Но ни один, кажется, не работает? Я ошибаюсь, думая, что в случае успеха Дафни есть должен быть какой-то базовый SMT-запрос, возвращающий unsat
?
Флаг командной строки для вывода ввода прувера — /proverLog:<file>
.
Вы также можете распечатать файл Boogie, созданный Дафни, с помощью /print:<file>
.