Леонардо: Согласно http://goedel.cs.uiowa.edu/smtlib/papers/smt-lib-reference-v2.0-r10.12.21.pdf, разделу 3.7.1, => является ассоциативным справа, а = цепнымТем не менее, похоже, что онлайн-версия Z3 не поддерживает такое использование.Есть ли параметр, который мне нужно установить, чтобы получить такое поведение?
=>
=
Спасибо ..
Нет, Z3 3.1 (и более старые версии) не поддерживают эти две «функции». Я добавлю их в Z3 3.2.