Stream: Mirror: Isabelle Users Mailing List

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


view this post on Zulip Email Gateway (Feb 12 2021 at 12:38):

From: Peter Lammich <lammich@in.tum.de>
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
*)

view this post on Zulip Email Gateway (Feb 12 2021 at 12:53):

From: Mathias Fleury <mathias.fleury12@gmail.com>
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

view this post on Zulip Email Gateway (Feb 15 2021 at 09:57):

From: Thomas Sewell <tals4@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.


Last updated: Dec 08 2021 at 08:24 UTC