我有一个非常简单的示例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