Z3定點：模型中公式爲false的含義是什麼？

Question

我正在嘗試使用Z3的定點引擎來檢查簡單的定時自動機的可達性。

的TA我建模是：

- >（x = 0的 = C < = 5） - [C> 2] - >（X = 1）

我想驗證狀態x = 1 & c = 3是否可達。要做到這一點我輸入以下內容Z3：

(declare-rel T (Int Real Int Real)) 
(declare-rel REACH (Int Real)) 
(declare-var x Int) 
(declare-var c Real) 
(declare-var nx Int) 
(declare-var nc Real) 
(declare-var delay Real) 
(rule (! (=> (and (= x 0) (> c 2.0)) (T x c 1 c)) :named stepint)) 
(rule (! (=> (and (REACH x c) (T x c nx nc)) (REACH nx nc)) :named tstep)) 
(rule (! (=> (and (= c 0.0) (= x 0)) (REACH x c)) :named initialstates)) 
(rule (! (let ((a!1 (and (>= delay 0.0) (= nc (+ c delay)) (or (not (= x 0)) (< nc 5.0))))) 
(=> a!1 (T x c x nc))) :named TICK)) 

(query (and (REACH x c) (= x 1) (= c 3.0)) 
:print-certificate true) 

當我在rise4fun運行上面Z3我回去：

formula false in model: (= REACH_1_0 3.0) 
formula false in model: (= REACH_0_0 1) 
formula false in model: (= query!0_0_n 1) 
formula false in model: (= query!0_1_n 3.0) 
sat 
(REACH 1 3.0) 

這表明，X = 1 & C = 3可達。 「模型中的公式是什麼意思」是什麼？這是簡單的信息還是Z3警告我關於可能形成不良的輸入？

Answer 1

錯誤出現在「opt」分支中。我還沒有將修復移植到不穩定的分支。它會發生，但如果不耐煩，請使用「opt」分支。 對不起。