Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2018 RC3: "verit: Abnormal termination...


view this post on Zulip Email Gateway (Aug 22 2022 at 18:09):

From: Michal Wallace <michal.wallace@gmail.com>
Running sledgehammer on windows on a fresh copy of Isabelle2018 RC3 gives me
the following error message:

"verit": A prover error occurred:
Abnormal termination with exit code 127

Oddly, "verit" is not configured as one of the sledgehammer provers in
jedit:

cvc4 z3 spass e remote_vampire

(I think the problem first appeared in RC2, but not sure...)

view this post on Zulip Email Gateway (Aug 22 2022 at 18:09):

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Wallace,

On 3. Aug 2018, at 08:46, Michal Wallace <michal.wallace@gmail.com> wrote:

Running sledgehammer on windows on a fresh copy of Isabelle2018 RC3 gives me
the following error message:

We've independently noted the problem yesterday. The decision has been to take out veriT (whose support is experimental and undocumented) from the release, and reintroduce it afterwards once we have sorted out the issues.

Oddly, "verit" is not configured as one of the sledgehammer provers in
jedit:

cvc4 z3 spass e remote_vampire

If this configuration was done in the Sledgehammer panel, it affects only the Sledgehammer panel, not the "sledgehammer" command. (See also "sledgehammer_params".)

Cheers,

Jasmin


Last updated: Mar 29 2024 at 12:28 UTC