Re: [isabelle] cvc4 crashing

On 04/11/16 15:12, Jasmin Blanchette wrote:
>> On 04.11.2016, at 14:38, Eugene W. Stark <isabelle-users at> wrote:
>>> /** Handler for SIGINT, i.e., when the user hits control C. */
>>> void sigint_handler(int sig, siginfo_t* info, void*) {
>>>  fprintf(stderr, "CVC4 interrupted by user.\n");
>>>  if(pOptions->getStatistics() && pExecutor != NULL) {
>>>    pTotalTime->stop();
>>>    pExecutor->flushStatistics(cerr);
>>>  }
>>>  abort();
>>> }
> Aha ! This shows that passing "--no-statistics" to CVC4 is enough to disable this behavior. I'll prepare a changeset for RC2 and send it to Makarius.

OK, the change is here
and thus scheduled for the next release candidate.

Here is also a document about signal handlers in C:

High-level things like printf are not allowed, so the above fprintf
might cause problems again at some point. E prover used to have similar
problems some years ago.

For the Isabelle2016-1 the present workaround should be OK, but the CVC4
guys should be informed about these inherent weaknesses of the signal


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