Re: [isabelle] cvc4 crashing



Dear Eugene,

> On 04.11.2016, at 14:38, Eugene W. Stark <isabelle-users at starkeffect.com> wrote:
> 
> I decided to try replacing the cvc4 binary by a shell script that
> ran cvc4 using the "strace" utility.  I recorded the attached
> trace (edited, original was 13MB long).  It seems to show a "normal"
> termination of cvc4 by the receipt of SIGINT, which then results
> in a call to abort() from the SIGINT handler:
> 
>> /** 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.

Cheers,

Jasmin





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