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

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,

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.



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"

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

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 MHonArc.