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
Z3_Bug.thy
Description: application/isabelle-theory
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
