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。