Re: [isabelle] Isabelle2021: cvc4 crashing (fixed)
- To: Ujkan Sulejmani <ujkan99 at gmail.com>, cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Isabelle2021: cvc4 crashing (fixed)
- From: Makarius <makarius at sketis.net>
- Date: Thu, 25 Nov 2021 16:58:05 +0100
- Authentication-results: cam.ac.uk; iprev=pass (relay.yourmailgateway.de) smtp.remote-ip=188.8.131.52; spf=pass smtp.mailfrom=sketis.net; dkim=pass header.d=sketis.net header.s=key2 header.a=rsa-sha256; arc=none
- Authentication-results: mx2f26; spf=pass (sender IP is 184.108.40.206) smtp.mailfrom=makarius at sketis.net smtp.helo=[192.168.179.20]
- In-reply-to: <CAAORPwxaAqc1=y5G0zxfqJx6HOdXbrOW+8Yi=17-t7hr21O50Q@mail.gmail.com>
- References: <CAAORPwxaAqc1=y5G0zxfqJx6HOdXbrOW+8Yi=17-t7hr21O50Q@mail.gmail.com>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.14.0
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>] (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.
For Isabelle2021-1 (December 2021) it is too late: We have updated so many
provers for that, but could not revisit cvc4, z3, smbc.
This archive was generated by a fusion of
Pipermail (Mailman edition) and