Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] sledgehammer (or Z3) internal error


view this post on Zulip 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: Jul 15 2022 at 23:21 UTC