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,
    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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.