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 starkeffect.com> 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
https://bitbucket.org/isabelle_project/isabelle-release/commits/be149db8207a36
and thus scheduled for the next release candidate.


Here is also a document about signal handlers in C:
https://docs.oracle.com/cd/E19455-01/806-5257/gen-26/index.html

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
handlers.


	Makarius





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