(set-option :bv-enable-int2bv-propagation true) 在线工作。但是，我的本地版本对此抱怨说：
(error "line 1 column 43: 未知参数 'bv_enable_int2bv_propagation'，这是一个旧的参数名称，调用 'z3 -p' 获取新参数列表")
新的参数名称是什么？我试图在z3 -p 的输出中找到它，但我不确定。
【问题讨论】：
标签： z3
我假设您使用的是 unstable（工作中）分支，或者夜间构建之一。每晚构建是使用unstable 分支生成的。
此分支包含将在下一个版本 (Z3 v4.3.2) 中可用的修改。 Rise4fun 正在运行官方版本（即master 分支）。下一个版本 (v4.3.2) 将包含一个新的参数设置基础结构。这些选项被组织在不同的模块中。
而且，我只将最常用的参数移植到了新框架中。
我以为没有人使用参数:bv-enable-int2bv-propagation :)
无论如何，
I fixed this issue。我在unstable 分支中添加了参数smt.bv.enable-int2bv。
您现在可以通过重新编译 unstable 分支来获得修复，或者等待修复在夜间构建中可用。参数smt.bv.enable-int2bv也将在下一个正式版本v4.3.2中。 Here 是关于如何编译 unstable 分支的说明。
【讨论】：