Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] cvc4 always crashing


view this post on Zulip Email Gateway (Apr 06 2022 at 19:25):

From: Angeliki Koutsoukou Argyraki <ak2110@cam.ac.uk>
An automation question, please:
Whenever I run Sledgehammer, cvc4
always crashes (almost immediately) while the rest of the provers either time out or find a proof (but never crash).
Any guesses why this is happening with cvc4? Any parameters
I should change?

Many thanks in advance,
Angeliki

view this post on Zulip Email Gateway (Apr 07 2022 at 07:27):

From: Jasmin Blanchette <cl-isabelle-users@lists.cam.ac.uk>
Dear Angeliki,

This sounds like a specific issue on your machine. For the next release, we will likely replace the rather old version of CVC4 with cvc5. This will likely be enough to solve the issue. If you're impatient to have a working cvc4, we could try to investigate the issue closer (e.g. via Zoom), in case we find something obvious. Let me know.

Cheers,

Jasmin


Last updated: Mar 29 2024 at 12:28 UTC