Re: [isabelle] a bug in Z3



On 18/04/2019 05:23, José Manuel Rodríguez Caballero wrote:
>   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

Can you also provide the example that produced this error? Does this
also happen in Isabelle2018? What is your OS platform?


	Makarius





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