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

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Fri Oct 5 10:59:25 CEST 2012

Am 05.10.2012 um 10:47 schrieb Lukas Bulwahn:

> Solver z3: Z3 proof parser (line 87): unknown sort: "Bool"
> Although it is possible to work around it, it might be worthwhile to investigate.

Thanks for the report. See 6279490e0438.


More information about the isabelle-dev mailing list