Email Gateway (Aug 22 2022 at 19:28): 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.
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: Apr 25 2024 at 04:18 UTC