Re: [isabelle] Isabelle2021: cvc4 crashing (fixed)



On 15/11/2021 16:53, Ujkan Sulejmani wrote:
> I had been experiencing regular cvc4 crashes (in prior Isabelle versions too,
> namely 2019 and 2020) when sledgehammer couldn’t find a proof. (crash log
> below). I found a fix in one of the GitHub issues raised in the cvc5 repo
> [https://github.com/cvc5/cvc5/pull/6518/files
> <https://github.com/cvc5/cvc5/pull/6518/files>] (this fix was indeed
> incorporated in cvc5) and managed to carry it over to Isabelle by building
> cvc4-1.8 from the modified source code and using that binary instead of the
> default one. This seems OK thus far—I haven’t experienced any crashes. Perhaps
> the developers could include this in the next release.

Concerning a cvc4 / cvc5 update, next release means Isabelle2022 (approx.
October 2022).

For Isabelle2021-1 (December 2021) it is too late: We have updated so many
provers for that, but could not revisit cvc4, z3, smbc.


	Makarius




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