Email Gateway (Jan 03 2021 at 12:00): Email Gateway (Jan 03 2021 at 12:00):From: Makarius <makarius@sketis.net>
Trying this with Isabelle2021-RC1 from
https://isabelle.in.tum.de/website-Isabelle2021-RC1 I still see the breakdown:
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 don't understand the setup myself. If an expert on Isabelle/Z3 wants to do
something about it, we still have 1-2 weeks time on the Isabelle2021 release
train.
Makarius
Z3bug.thy
Last updated: Jan 04 2025 at 20:18 UTC