CODEWITHSUNDEEP
z3smt
Ranjit Jhala
Ranjit Jhala

Reputation: 1242

z3 @ command line behaving differently than online

the (rather small) query that I have here:

http://rise4fun.com/Z3/W4sf

works just fine on the website (above) but hangs when I run it on my mac, with 

z3 -in

followed by pasting in the exact text above, which is:

(declare-const x Real)
(assert (not (= 0.0 x)))
(assert (not (< 0.0 (* x x))))
(check-sat)

Any ideas? I thought it might be that I have an old version but its 4.3.2

rjhala@borscht ~/bin [130]> z3 -help
Z3 [version 4.3.2 - 64 bit - build hashcode 5b5a474b5443].

Am I missing some parameters? Or any other suggestions? Many thanks!

Ranjit.

Upvotes: 1

Views: 272

Answers (1)

Taylor T. Johnson
Taylor T. Johnson

Reputation: 2884

It also seemed not to return for me using that, but it seems to work as:

z3 -in -smt2

Followed by pasting the query, so I think it may need the -smt2 parameter. I tried it on Windows with 4.3.3 (I thought I had 4.3.2, but it seems I updated from the latest unstable branch):

C:\Users\tjohnson>z3 -in -smt2
(declare-const x Real)
(assert (not (= 0.0 x)))
(assert (not (< 0.0 (* x x))))
(check-sat)
unsat

It also worked for me by pasting the query into test.smt and running:

C:\Users\tjohnson>z3 -smt2 test.smt
unsat

Upvotes: 1

Related Questions