导出 FRAMA-C/WP 发送到求解器的 SAT/SMT 方程

Question

是否可以导出或记录由 FRAMA-C/WP 和 Why3 生成的 SAT/SMT 方程，发送到 SAT-SMT-Solver（如 Alt-Ergo 或 Z3）？

如果使用求解器 Z3（例如通过命令

frama-c -wp -wp-prover z3 test.c

）是否也可以以 smt-lib 格式导出生成的 SMT 方程？

我想知道这些导出的方程是否可以进一步用于获得反例？

我尝试使用

-wp-out dir

标志，但没有生成任何输出。我的 frama-c 版本是：26.1（Iron），为什么3：1.5.1

Answer 1

目前尚未实现导出 SMT 求解器文件。添加并不难，但需要为此向 Frama-C 添加一个新选项。利用这些文件来获取反例可能是可能的，但这不会那么直接，因为如果没有正确的证明上下文描述，它可能会给出不那么有趣的反例。

WP 中已有反例实现的工作，但尚未准备好发布，需要更多的开发工作。