[isabelle-dev] sledgehammer "problem malformed" message
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Fri Jul 4 15:22:18 CEST 2014
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