search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

Error "unknown constant Int" when working with Sequences. #1896

Closed bj2015 closed 5 years ago

bj2015 commented 5 years ago

The following rather small piece of SMTLIB surprised me when Z3 answered (error "line 3 column 38: unknown constant Int"): instead of the expected unsat.

(set-logic LIA)

(assert (seq.contains (seq.empty (Seq Int)) (seq.unit 7))

(check-sat)

I added the (set-logic LIA)-part to ensure that Ints were availlable, but to no avail...

Can someone tell we what's going on?

I am using Z3 version 4.7.1 - 64 bit on MacOS Sierra Version 10.12.6.

bj2015 commented 5 years ago

Update: I just found out that

(assert (seq.contains (as seq.empty (Seq Int)) (seq.unit 7)))

(check-sat)

works. Sorry, I did not know that the "as" keyword was that important.