Z3 4.3.2 中的潜在配置错误

Question

我可能发现了与 mbqi 相关的配置错误。考虑以下短程序：

(set-option :smt.mbqi true)
  ; Set to false and the warnings disappear
(set-option :smt.relevancy 2)
  ; On my local machine I got
  ;   0 and 1 - three times the same warning
  ;   2 (or higher) - one warning
  ; but on rise4fun I always got the same warning three times
(set-option :smt.case_split 3)
  ; WARNING: relevacy must be enabled to use option CASE_SPLIT=3, 4 or 5

(declare-fun fun (Int) Bool)
(assert (forall ((x Int)) (fun x)))

(check-sat)

运行它在 Windows 7 x64 上使用 Z3 4.3.2 的官方下载版本在本地使用我收到有关未启用相关性的意外警告。更改 relevancy 的值只会影响我收到的警告数量（三个或一个）。

运行 script on rise4fun 总是产生三次相同的警告，无论为 relevancy 选择的值如何。

这实际上是一个错误还是我在这里遗漏了什么？

Answer 1

这很可能是一个错误，但与 mbqi 无关的可能性很小；当它设置为 false 时你得到较少警告的原因是它只是更早地放弃，永远不会到达抛出额外警告的部分。

虽然参数没有达到所有必需的部分，但存在很多问题，所以我怀疑这是另一个问题。

请注意，auto_config 也必须为 smt.case_split=3,4,5 禁用（但这是调试版本中的默认设置）。

编辑：原来警告消息是虚假的；这现在已在不稳定中修复（截至 this 提交）。

Z3 4.3.2 中的潜在配置错误

Potential configuration bug in Z3 4.3.2

configuration

warnings

z3