Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] a bug in Z3


view this post on Zulip Email Gateway (Aug 22 2022 at 19:28):

From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
Hello,
I do not know whether this is important to report this or not, but I was
using Isabelle2019 and I received the following error message while
invoking Sledgehammer:

"z3": A prover error occurred:
exception Fail raised (line 222 of "~~/src/HOL/Tools/SMT/z3_proof.ML"):
Replaying the proof trace produced by Z3 failed: the bound "?0" is
undeclared; this indicates a bug in Z3

I hope that this information may be helpful in the development of
Isabelle2019.

Kind Regards,
José M.

view this post on Zulip Email Gateway (Aug 22 2022 at 19:28):

From: Makarius <makarius@sketis.net>
Can you also provide the example that produced this error? Does this
also happen in Isabelle2018? What is your OS platform?

Makarius


Last updated: Nov 21 2024 at 12:39 UTC