在Z3中使用量化符消除時的SegFault

我使用MacOS X 10.8中的Z3 4.3.1（來自主分支）。我得到下面的例子分段錯誤：在Z3中使用量化符消除時的SegFault

(declare-const a Int) 
(declare-const b Int) 

(assert 
    (exists ((k Int)) 
    (and 
    (= (- (* 2 k) a) 0) 
    (= (- (* 2 k) b) 0) 
    ) 
) 
) 


(check-sat-using qe)

任何想法，就如何解決這個問題？

來源

2013-02-18 user2083098

在Windows XP + Z3 4.3.0

(declare-const a Int) 
(declare-const b Int) 

(assert 
    (exists ((k Int)) 
    (and 
    (= (- (* 2 k) a) 0) 
    (= (- (* 2 k) b) 0) 
    ) 
) 
) 
(check-sat-using (then qe smt)) 
(get-model)

來源

2013-02-18 14:08:18

謝謝，但我最初的策略是（然後簡化solve-eqs qe smt）。我隔離了實際產生分段錯誤的那個（即「qe」）。 – user2083098 2013-02-18 14:58:59

'（check-sat-using qe）'也適用，但是在我的安裝中產生「未知」。 – 2013-02-18 15:24:05

'qe'是一個預處理步驟。如果我們想檢查可滿足性，我們應該在'qe'之後使用最終的遊戲策略（例如'smt'），就像Axel發佈的例子。如果我們想檢查'qe'產生的結果，我們應該用'（apply qe）'代替。 – 2013-02-19 00:35:48

以下OK作品，我設法重現您使用OSX和Z3 4.3.1中描述的錯誤。此錯誤已修復，並將在下一次正式發佈中提供。同時，您可以使用OSX的每晚構建版本或使用unstable（正在運行）分支構建Z3版本。

每晚的構建可以在：http://z3.codeplex.com/releases下載。我們必須點擊「計劃」鏈接。我寫了一些指示here。如果我們想檢查可滿足性，我們應該在qe之後使用結束遊戲策略（如smt），就像Axel發佈的示例一樣。如果我們想檢查qe產生的結果，我們應該使用(apply qe)來代替。

來源

2013-02-19 00:49:50

謝謝萊昂納多。我通過在src/muz_qe/qe_arith_plugin.cpp（第527行）的expr中添加一個缺失ref來修復此bug： // a * s + b * t +（a-1）（b-1）<= 0 expr_ref aux（m_arith.mk_add（as_bt，slack），m）; mk_le（aux，result1）; 它是你的修復嗎？ – user2083098 2013-02-19 13:50:04

我甚至用「（然後qe smt）」策略來解決這個問題。 – user2083098 2013-02-19 13:54:47

在Z3中使用量化符消除時的SegFault

回答

相關問題