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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
