bv-enable-int2bv-propagation 选项 [英] bv-enable-int2bv-propagation option

问题描述

(set-option :bv-enable-int2bv-propagation true) 在线工作.但是，我的本地版本抱怨它，说:

(set-option :bv-enable-int2bv-propagation true) works online. But, my local version complaints about it, saying:

(错误第 1 行第 43 列:未知参数'bv_enable_int2bv_propagation'，这是一个旧的参数名称，调用'z3 -p' 获取新的参数列表")

(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 的输出中找到它，但我不确定.

What's the new parameter name? I tried to find it in the output of z3 -p, but I'm not sure.

推荐答案

我假设您正在使用 unstable(工作进行中)分支，或者每晚构建之一.每晚构建是使用 unstable 分支生成的.此分支包含将在下一个版本 (Z3 v4.3.2) 中可用的修改.Rise4fun 正在运行正式版本(即 master 分支).下一个版本 (v4.3.2) 将包含一个新的参数设置基础结构.这些选项组织在不同的模块中.而且，我只将最常用的参数移植到新框架中.我以为没有人在使用参数 :bv-enable-int2bv-propagation :)

I'm assuming you are using the unstable (working-in-progress) branch, or one of the nightly builds. The nightly builds are produced using the unstable branch. This branch contains modifications that will be available in the next release (Z3 v4.3.2). Rise4fun is running the official release (i.e., master branch). The next release (v4.3.2) will contain a new parameter setting infrastructure. The options are organized in different modules. Moreover, I only ported the most commonly used parameters to the new framework. I thought nobody was using the parameter :bv-enable-int2bv-propagation :)

无论如何，我解决了这个问题.我在 unstable 分支中添加了参数 smt.bv.enable-int2bv.您现在可以通过重新编译 unstable 分支来获得修复，或者等待修复在夜间构建中可用.参数 smt.bv.enable-int2bv 也将在下一个正式版本 v4.3.2 中.这里 是关于如何编译 unstable 分支的说明.

Anyway, I fixed this issue. I added the parameter smt.bv.enable-int2bv in the unstable branch. You can get the fix now by recompiling the unstable branch, or waiting the fix to be available in the nightly builds. The parameter smt.bv.enable-int2bv will also be in the next official release v4.3.2. Here are instruction on how to compile the unstable branch.

这篇关于bv-enable-int2bv-propagation 选项的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！