z3 - Z3中的分段错误

Question

我正在使用带有位向量算术的 Quantified 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)) ))

有问题的完整基准可以在这里找到： 示例

Answer 1

感谢您报告崩溃。我修复了错误。该修复程序已在不稳定（正在进行中）分支中可用。以下是有关如何构建不稳定分支的说明。该修复程序也将于明天在 Z3 夜间版本中提供。

可以在以下位置下载每晚构建：http: //z3.codeplex.com/releases。我们必须点击“计划中的”链接。我在这里写了一些说明。