[isabelle-dev] strange behaviour with Z3 and smt method

[Lukas Bulwahn]

Hi all,

on the current Isabelle development version b2135b2730e8, I noticed a 
strange behavior with the smt proof method. It replies

Solver z3: Z3 proof parser (line 87): unknown sort: "Bool"

Although it is possible to work around it, it might be worthwhile to 
investigate.


Lukas

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Z3_Bug.thy
Type: application/isabelle-theory
Size: 2334 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20121005/79100265/attachment.bin>