Z3中的分段錯誤

Question

我正在使用位矢量算法進行量化BitVector公式的基準測試。該基準與Z3 4.3.0在Linux 64位中產生了分段錯誤。我認爲問題是由於平等的傳遞使用而發生的。

... 
(assert (= (bvadd (capacity this) (_ bv1 5)) (EAO.length (elements this)) )) 
(assert (= (EAO.length (elements this)) (IKAO.length (heap this)))) 

有問題的完整的基準可以在這裏找到： example

Answer 1

感謝您報告崩潰。 I fixed the bug。該修復程序已在不穩定（正在進行中）分支中提供。 Here是關於如何構建不穩定分支的說明。該修補程序也將在Z3夜間版本中提供。

每晚的構建可以在：http://z3.codeplex.com/releases下載。我們必須點擊「計劃」鏈接。我寫了一些指示here。