[isabelle-dev] smt for word

[Gerwin Klein]

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.

Cheers,
Gerwin