Z3 Prover 在命令行中增加时间和内存

【问题标题】：Z3 Prover Increase Time and Memory in Command LineZ3 Prover 在命令行中增加时间和内存
【发布时间】：2020-02-08 08:24:50
【问题描述】：

我正在尝试使用 Z3Prover 验证 003-23-80.cnf 是否可以满足。我已经验证了使用 Minisat 可以满足要求，但它需要大约 2 小时和 500 MB 内存。

我在 bash 中写道：

z3 -wcnf -st -T:9000 -memory:500 003-23-80.cnf

我相信这应该将时间延长到 9000 秒，内存延长到 500 兆字节，但我的输出不满足：

Terminal Output

我做错了什么？

【问题讨论】：

标签： z3

【解决方案1】：

不管内存/时间等；如果 minisat 说这个基准是 sat 而 z3 说它是 unsat，那么其中一个有错误！根据实际预期的情况，您应该将此作为错误报告给错误方。（如果您不确定，只需向 z3 人员报告他们不同意 minisat。在此处使用问题跟踪器：https://github.com/Z3Prover/z3/issues）

【讨论】：