[isabelle-dev] sledgehammer "problem malformed" message

[Jasmin Christian Blanchette]

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