(set-option :bv-enable-int2bv-propagation true) работает онлайн. Но моя локальная версия жалуется на это, говоря:
(ошибка «строка 1, столбец 43: неизвестный параметр« bv_enable_int2bv_propagation », это старое имя параметра, вызовите« z3 -p », чтобы получить новый список параметров»)
Какое новое имя параметра? Я пытался найти его в выводе z3 -p, но не уверен.
Я предполагаю, что вы используете ветку unstable (в разработке) или одну из ночных сборок. Ночные сборки производятся с использованием ветки unstable. Эта ветка содержит модификации, которые будут доступны в следующем релизе (Z3 v4.3.2). Rise4fun использует официальную версию (т. е. ветвь master). Следующий выпуск (v4.3.2) будет содержать новую инфраструктуру настройки параметров. Опции организованы в разных модулях. Более того, я перенес в новый фреймворк только наиболее часто используемые параметры. Я думал никто не использует параметр :bv-enable-int2bv-propagation :)
В любом случае, я исправил эту проблему. Я добавил параметр smt.bv.enable-int2bv в ветку unstable. Вы можете получить исправление сейчас, перекомпилировав ветку unstable или подождав, пока исправление будет доступно в ночных сборках. Параметр smt.bv.enable-int2bv также будет в следующем официальном релизе v4.3.2. Здесь инструкции по сборке ветки unstable.
