[isabelle] RC5: Sledgehammer and HOL-Library.Word problems
Trying to prove the following (obvious) lemma results in funny
sledgehammer error messages:
lemma word1_NOT_eq: "NOT (x::1 word) = x+1"
"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
> See again
> and 4 for further details.
> Any feedback about release candidates should be posted with a
> Subject including the version (not just a clone of this
> People who have tested earlier release candidates should definitely
> this one, otherwise some last-minute problems might remain
This archive was generated by a fusion of
Pipermail (Mailman edition) and