[isabelle-dev] sledgehammer "problem malformed" message

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Fri Jul 4 15:22:18 CEST 2014

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).



More information about the isabelle-dev mailing list