Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] cvc4 always crashing

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

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: Jan 04 2025 at 20:18 UTC