[isabelle-dev] sledgehammer "problem malformed" message
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Sat Jul 12 14:10:21 CEST 2014
Am 04.07.2014 um 07:48 schrieb Leo Freitas <leo.freitas at newcastle.ac.uk>:
> "z3": The generated problem is malformed. Please report this to the Isabelle developers.
> I wasn’t sure whether the cast I was making for the shift operation was right or not, but anyhow I thought to send it to the list as suggested.
This was easy to fix (at least for Z3; I will push a change soon). Thank you again for your report.
More information about the isabelle-dev