[isabelle] a bug in Z3

  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

Kind Regards,
José M.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.