執行在命令行腳本Z3提示

我有一個非常簡單的例子Z3方案，其中如下：執行在命令行腳本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 .

，重複程序中的每一行此錯誤。任何人都可以幫助我看到我做錯了什麼？

您正在使用SMT2格式。致電

z3 -smt2 <script path>

2015-06-23 08:59:03 dejvuth

非常感謝。你還知道另外一個問題：如何爲模型的可能答案生成所有不同的變體？ –

查看http://stackoverflow.com/questions/13395391/z3-finding-all-satisfying-models – dejvuth

感謝您的回答，但這是Z3 python中的代碼。我不能在正常的Z3語法中使用它 –

回答