Executing a Z3 script in command line prompt

Question

I have a very simple example Z3 program which is as follows:

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

This sample program can be executed in the Z3 online compiler and there are no problems. But when I want to execute the same program using command line prompt with the following command:

Z3 <script path>

I get the error saying:

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

and this error is repeated for each line in the program. Can anyone help me to see what I am doing wrong?

Answer 1

You're using SMT2 format. Call

z3 -smt2 <script path>