[isabelle-dev] smt for word
gerwin.klein at nicta.com.au
Wed Oct 5 01:26:15 CEST 2011
lemma "(x :: 8 word) + x = 2 * x"
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