[isabelle-dev] sledgehammer "problem malformed" message

[Leo Freitas]

Hi,

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   

theory Scratch
imports Main Word "~~/src/HOL/Word/WordBitwise"
begin

type_synonym word32 = "32 word"

lemma "(sint (TrueMSB :: 32 word)) ≤ 263 ⟹ ¬ (8::word32) ≤ (Word.Word (sint ((TrueMSB << 5) :: 32 word))) OR 7"
apply (word_bitwise)
apply safe
sledgehammer
oops

end

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.

Best,
Leo
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140704/dfc41b3a/attachment.asc>