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提交）。