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

[Jasmin Christian Blanchette]

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.

Jasmin