神祕的「未知」從Z3

Question

我正在寫一個新的程序邏輯proofchecker，處理軟弱內存。 Z3確實繁重：我在我的所有檢查翻譯成的AST，並使用ML結合在Z3扔。 （但是，見下文，我已經通過rise4fun在線查看了Z3，給出了相同的答案）。這是我想檢查，漂亮的打印，所以我能理解運營商的嵌套，稍有簡化的名稱，因此很容易，看看他們是什麼含義：

  r1=1 
     =>  y=1 
      /\ x=1 
    /\ xnew=x 
    /\ ynew=2 
=>   xnew=x 
     /\ ynew=y 
    \/ Exists(r1) 
        r1=1 
       =>  y=1 
        /\ x=1 
      /\ xnew=x 
      /\ ynew=2 

這轉化爲AST的很好（類型聲明不示，但請參閱下面的實際Z3輸入）：

(let ((a1 (and (=> (= r1 1) (and (= y 1) (= x 1))) 
       (= xnew x) 
       (= ynew 2))) 
    (a2 (exists ((r1 Int)) 
      (and (=> (= r1 1) (and (= y 1) (= x 1))) 
       (= xnew x) 
       (= ynew 2))))) 
(=> a1 (or 

（和（= xnew X）（= ynew Y））A2）））

所以這就是所有的罰款。但Z3說'未知'。奇怪的是，在我所有的測試中，這是成千上萬個查詢中唯一能夠得出這個結果的查詢。所以我用Z3的在線版本進行調查，通過rise4fun教程，它接受了這個輸入

(declare-const r1 Int) 
(declare-const y Int) 
(declare-const x Int) 
(declare-const xnew Int) 
(declare-const ynew Int) 
(define-fun a1() Bool 
    (and (=> (= r1 1) (and (= y 1) (= x 1))) 
       (= xnew x) 
       (= ynew 2)) 
) 
(define-fun a2() Bool 
    (exists ((r1 Int)) 
      (and (=> (= r1 1) (and (= y 1) (= x 1))) 
       (= xnew x) 
       (= ynew 2))) 
) 
(define-fun conjecture() Bool 
    (=> a1 (or (and (= xnew x) (= ynew y)) a2)) 
) 
(assert (not conjecture)) 
(check-sat) 

並表示'unknown'。

我是不是做一個簡單的錯誤，或者這是一個錯誤，還是什麼？

Answer 1

這似乎是在主分支，在網上使用的可執行文件中的錯誤。 行爲不會在最新的不穩定分支重現。