Z3中的PDR引擎的“官方”版本是什么？

Question

我正在尝试Z3中的PDR引擎，我不确定要使用哪个版本的Z3。

来自git的“官方”master分支似乎有效，但是日期为2012年11月。我确信自那以后有了改进。另一方面，不稳定的分支“可能包含不稳定的和/或未经测试的代码”，这似乎是正确的。

什么是最新的“稳定”版本的引擎？

例如

(declare-rel R (Real Real)) 
(declare-var x Real) 
(declare-var y Real) 

(rule 
    (=> (and (= x 0) (= y 0)) (R x y)) 
) 

(rule 
    (=> (R x y) (R (+ x 1) (+ y 1))) 
) 

(query 
    (and (R x y) (not (= x y))) 
) 

以上工作在主，返回不饱和度，但在不稳定的分支发动机跑开了不解决问题。来自最近的CAV论文的example也一样。

Answer 1

这是一个回归，并指出了这一点。 旧版本的PDR在检查归纳时使用查询中的谓词。即使该属性很容易被看作是归纳性的，但更新后的版本会省略此功能并分散。 从查询中使用谓词不是很一般，我试图用其他方法替换它。例如，你可以做一个“魔术设置”的转换，以推动适时的谓词。