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
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
