[isabelle-dev] sledgehammer "problem malformed" message

[Jasmin Christian Blanchette]

Hi Leo,

Am 04.07.2014 um 07:48 schrieb Leo Freitas <leo.freitas at newcastle.ac.uk>:

> I was playing with HOL-Word to see if I could bring some discharged VCs from another tool into Isabelle.
> When I tried sledgehammer on it I got the error message for Z3

Thanks for the report! We will look into this. It may take some time because of a deadline, though. And do let us know should you run into more issues with Z3 (which we upgraded to 4.3 from 3.2 in this version, requiring a major overhaul of our infrastructure).

Cheers,

Jasmin