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



Hi Peter,


Isabelle never had reconstruction for words. So the Z3 error is expected.


The CVC4 errors you reported earlier this year are fixed, however.


Best,

Mathias


On 12/02/2021 13:38, Peter Lammich wrote:
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.