Ваша программа проверяет, когда я добавляю флаг -arith:2, который добавляет символические синонимы для арифметических символов и позволяет использовать их в триггерах.
Редактировать: Более общий ответв том, что ваша задача использует нелинейную арифметику, которая в общем неразрешима. В * 1007 есть несколько советов по работе с ними:
У меня нет особого опыта работы с Дафни и нелинейной арифметикой. *1008* *1009* Я не знаю, почему ваш файл имеетработал раньше, но для исследования можно было распечатать SMT-кодировку Dafny-каналов в Z3 (см. Дафни-вывод в виде SMT-файла ) и сравнить разные версии, если нет разницы, возможно, есть разница между версиями Z3.
Может быть, есть способ по-разному кодировать вашу проблему, который работает более стабильно между различными версиями решателя, при условии, что ни в одном из инструментов нет ошибок.