5

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?

Amir Ebrahimi
  • 115
  • 1
  • 10

1 Answers1

6

You're using SMT2 format. Call

z3 -smt2 <script path>
dejvuth
  • 6,986
  • 3
  • 33
  • 36
  • Thanks that was great. One other question do you know how I can generate all the different variations for possible answers of the model? – Amir Ebrahimi Jun 23 '15 at 09:04
  • Thanks for your answer, but this is a code in Z3 python. I can't use it in normal Z3 syntax – Amir Ebrahimi Jun 23 '15 at 11:37
  • Z3 will produce only one model, but after the first time, you can add a constraint that excludes the previous model (e.g., ... (and (not (= x 3))); that's essentially what the Python code in the other post does. – Christoph Wintersteiger Jun 24 '15 at 13:54