在命令行提示符下执行 Z3 脚本答案

【问题标题】：Executing a Z3 script in command line prompt在命令行提示符下执行 Z3 脚本
【发布时间】：2015-09-08 23:26:14
【问题描述】：

我有一个非常简单的 Z3 程序示例如下：

(declare-const a Int)
(declare-fun f (Int Bool) Int)
(assert (> a 10))
(assert (< (f a true) 100))
(check-sat)

这个示例程序可以在Z3在线编译器中执行，没有任何问题。但是当我想使用命令行提示符执行相同的程序时，使用以下命令：

Z3 <script path>

我收到错误消息：

ERROR: line 1 column 21: could not match expression to benchmark .

并且程序中的每一行都会重复此错误。谁能帮我看看我做错了什么？

【问题讨论】：

标签： z3

【解决方案1】：

您使用的是 SMT2 格式。打电话

z3 -smt2 <script path>

【讨论】：

谢谢，太好了。另一个问题你知道我如何为模型的可能答案生成所有不同的变体吗？
感谢您的回答，但这是 Z3 python 中的代码。我不能在正常的 Z3 语法中使用它
Z3 只会产生一个模型，但是在第一次之后，您可以添加一个排除之前模型的约束（例如，...（and (not (= x 3))））；那就是基本上是另一篇文章中的 Python 代码所做的。