z3 - 递归 Horn 子句的求解器

Question

如今，在自动程序验证中，将问题作为 Horn 子句系统的解决方案是很流行的，其中大多数 Horn 子句定义了不变量的归纳条件，然后一些约束定义了要匹配的安全条件。

一种文件格式是 SMT-LIB:子句只是 assert谓词上的语句，被视为映射到 bool 值的函数。

实现这一点的求解器包括 vanilla Z3 和 Spacer。

能够解决此类问题的其他合理成熟、文档化和可下载的求解器是什么？

Answer 1

甚至 Z3 也有多个求解器，例如 BMC、PDR(默认？)、CLP(序言式推理)、Datalog 和 Duality。选择fixedpoint.engine=xx。
还有另一个引擎即将推出，它是 HSF 到 Z3 的端口。 (原来的HSF也有，很靠谱)

还有其他求解器，但我对它们没有太多经验。
例如，Eldarica、VeriMAP 等。