Email Gateway (Feb 12 2021 at 12:38): 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
*)
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
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: Jul 15 2022 at 23:21 UTC