[isabelle-dev] sledgehammer "problem malformed" message

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Sat Jul 12 14:10:21 CEST 2014


Dear Leo,

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

> Sledgehammering... 
> "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.

Cheers,

Jasmin




More information about the isabelle-dev mailing list