z3 - bv-enable-int2bv-传播选项

Question

(set-option :bv-enable-int2bv-propagation true) 在线工作。但是，我的本地版本对此有所提示，说:

(error "line 1 column 43: unknown parameter 'bv_enable_int2bv_propagation', this is an old parameter name, invoke 'z3 -p' to obtain the new parameter list")

新参数名称是什么？我试图在 z3 -p 的输出中找到它，但我不确定。

Answer 1

我假设您正在使用不稳定(正在进行中)分支或夜间构建之一。每晚构建是使用 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有关如何编译不稳定分支的说明。