[isabelle-dev] smt for word

Gerwin Klein gerwin.klein at nicta.com.au
Wed Oct 5 01:26:15 CEST 2011

I'm getting 

lemma "(x :: 8 word) + x  = 2 * x"
 apply smt

Solver z3: Z3 proof parser (line 2): unknown sort: "bv" 

I was trying remote Z3 from a Mac.

This is on isabelle 20b3377b08d7, but I don't think anything relevant has changed since Sep 26.

Am I doing something wrong? Sounds like Z3 responds with something the smt method doesn't know about.


More information about the isabelle-dev mailing list