[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"
begin

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

--
  Peter


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.