Re: [isabelle] cvc4 crashing



Dear Eugene,

> On 26.11.2016, at 20:37, Eugene W. Stark <isabelle-users at starkeffect.com> wrote:
> 
> Unfortunately, the --no-statistics option does not work to suppress the aborts.

That's a pity. Looking at the code, I was overly confident this would do the trick. Regardless, I had filed a bug report to the CVC4 developers and have now updated it:

	http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=767

There's also a thread on the CVC-USERS mailing list that discussed the issue. To summarize the thread, CVC4 developer Tim King wrote

> But if users want an alternative nice death, i.e. exit with a non-zero
> code, we might be able to support that. It would probably need to come in
> the form of a compile time flag.

And user Johannes Kanig wrote

> we (the AdaCore SPARK team, heavy users of cvc4) would definitely welcome such a compile time flag.

I'm sorry we don't have a better resolution for Isabelle2016-1, but we're very much dependent on the CVC4 developers cleaning up their act.

Cheers,

Jasmin





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