[isabelle] RC5: Sledgehammer and HOL-Library.Word problems

Trying to prove the following (obvious) lemma results in funny
sledgehammer error messages:

theory Scratch
  imports "HOL-Library.Word"

lemma word1_NOT_eq: "NOT (x::1 word) = x+1"
Proof found... 
"cvc4": One-line proof reconstruction failed: by (smt (z3)) 
"z3": A prover error occurred:
bad SMT term: bvnot 


On Mon, 2021-02-08 at 22:42 +0100, Makarius wrote:
> Dear Isabelle users,
> the end of the Isabelle2021 release process is getting pretty close.
> Presumably the last release candidate is
> https://isabelle.sketis.net/website-Isabelle2021-RC5
> See again
> https://isabelle-dev.sketis.net/phame/post/view/28/release_candidates_for_isabelle2021
> and 4 for further details.
> Any feedback about release candidates should be posted with a
> meaningful
> Subject including the version (not just a clone of this
> announcement).
> People who have tested earlier release candidates should definitely
> follow
> this one, otherwise some last-minute problems might remain
> undetected.
> 	Makarius

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.