(set-option :bv-enable-int2bv-propagation true)在线工作。但是，我的本地版本抱怨它，说：
（错误“第1行第43列：未知参数'bv_enable_int2bv_propagation'，这是一个旧参数名称，调用'z3 -p'获取新参数列表”）
新的参数名称是什么？我试图在 的输出中找到它z3 -p，但我不确定。
问问题
343 次
1 回答
2
我假设您正在使用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分支的说明。
于 2013-04-03T23:03:02.563 回答