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

[Thomas Sewell <tals4 at cam.ac.uk>]

I'm a little confused about this. There has never been support for
reconstruction of Z3's proofs involving the word/bitvector theory.
There is experimental support to convert goals into SMT problems,
but since the reconstruction is missing, I thought that feature was
disabled by default, but, I can reproduce the error you posted.
I had thought that declare [[z3_extensions]] was required to cause
bitvector constants to appear in generated SMT problems.

I've been making use of this experimental support as a kind of
fiddly quickcheck/nitpick for some proofs I've been doing. I'm planning
to commit some improvements on that, which might include a fix for this
issue. However, none of that will make it into this release round.

Best regards,
    Thomas.

On 2021-02-12 12:52, Mathias Fleury wrote:
> 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