Стратегия по умолчанию для логики UFBV не эффективна для ваших проблем. На самом деле, стратегия по умолчанию решает все из них менее чем за 1 сек. Чтобы заставить Z3 использовать стратегию по умолчанию, вам просто нужно прокомментировать следующие строки в вашем скрипте.
; (set-logic UFBV)
; (set-option :pull-nested-quantifiers true)
; (set-option :macro-finder true)
Если предупреждающие сообщения вас беспокоят, вы можете добавить:
(set-option :print-warning false)
При этом я постараюсь решить поднятые вами вопросы.
Влияет ли имя идентификатора на поведение Z3? Да, они делают.
Начиная с версии 3.0, мы начали использовать полный порядок выражений Z3 для выполнения таких операций, как: сортировка аргументов ассоциативно-коммутативных операторов.
Этот общий порядок основан на именах идентификаторов.
По иронии судьбы, эта модификация была мотивирована отзывами пользователей. В предыдущих версиях мы использовали внутренний идентификатор для выполнения таких операций, как сортировка и разрыв связей во многих различных эвристиках. Однако эти идентификаторы основаны на порядке, в котором Z3 создает / удаляет выражения, который основан на порядке, в котором пользователи объявляют символы. Таким образом, на поведение Z3 2.x будут влиять тривиальные модификации, такие как удаление неиспользуемых объявлений.
Что касается iff, он не является частью стандарта SMT-LIB 2.0. В SMT-LIB 2.0 = используется для формул и терминов. Чтобы убедиться, что Z3 полностью совместим со стандартом SMT-LIB 2.0, всякий раз, когда пользователи задают логику, поддерживаемую SMT-LIB (или скоро будет поддерживаться, например, UFBV), Z3 только «загружает» символы, определенные в нем. Когда логика не указана, Z3 предполагает, что пользователь использует «логику Z3», которая содержит все поддерживаемые теории в Z3 и многие дополнительные aliases, такие как: iff для логического значения =, if для ite и др.