Re: [isabelle] cvc4 crashing



Unfortunately, the --no-statistics option does not work to suppress the aborts.
With Isabelle-2016-1-RC3:

ERROR: apport (pid 3688) Sat Nov 26 08:39:13 2016: this executable already crashed 2 times, ignoring
ERROR: apport (pid 3700) Sat Nov 26 08:39:20 2016: called for pid 3695, signal 6, core limit 0
ERROR: apport (pid 3700) Sat Nov 26 08:39:20 2016: executable:
/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 (command line
"/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 --full-saturate-quant --inst-when=full-last-call
--inst-no-entail --term-db-mode=relevant --no-statistics --random-seed=1 --lang=smt2 --continued-execution --tlimit 6418
/tmp/isabelle-gene/process7458968389934499957/cache-io-3949674")
ERROR: apport (pid 3700) Sat Nov 26 08:39:20 2016: debug: session gdbus call: (true,)

ERROR: apport (pid 3700) Sat Nov 26 08:39:20 2016: this executable already crashed 2 times, ignoring
ERROR: apport (pid 3712) Sat Nov 26 08:39:24 2016: called for pid 3711, signal 6, core limit 0
ERROR: apport (pid 3712) Sat Nov 26 08:39:24 2016: executable:
/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 (command line
"/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 --full-saturate-quant --inst-when=full-last-call
--inst-no-entail --term-db-mode=relevant --no-statistics --random-seed=1 --lang=smt2 --continued-execution --tlimit 4058
/tmp/isabelle-gene/process7458968389934499957/cache-io-3952234")
ERROR: apport (pid 3712) Sat Nov 26 08:39:24 2016: debug: session gdbus call: (true,)

ERROR: apport (pid 3712) Sat Nov 26 08:39:24 2016: this executable already crashed 2 times, ignoring
ERROR: apport (pid 3728) Sat Nov 26 08:39:28 2016: called for pid 3720, signal 6, core limit 0
ERROR: apport (pid 3728) Sat Nov 26 08:39:28 2016: executable:
/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 (command line
"/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 --full-saturate-quant --inst-when=full-last-call
--inst-no-entail --term-db-mode=relevant --no-statistics --random-seed=1 --lang=smt2 --continued-execution --tlimit 3000
/tmp/isabelle-gene/process7458968389934499957/cache-io-3953574")
ERROR: apport (pid 3728) Sat Nov 26 08:39:28 2016: debug: session gdbus call: (true,)

ERROR: apport (pid 3728) Sat Nov 26 08:39:28 2016: this executable already crashed 2 times, ignoring
ERROR: apport (pid 3743) Sat Nov 26 08:39:31 2016: called for pid 3737, signal 6, core limit 0
ERROR: apport (pid 3743) Sat Nov 26 08:39:31 2016: executable:
/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 (command line
"/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 --full-saturate-quant --inst-when=full-last-call
--inst-no-entail --term-db-mode=relevant --no-statistics --random-seed=1 --lang=smt2 --continued-execution --tlimit 3000
/tmp/isabelle-gene/process7458968389934499957/cache-io-3953942")
ERROR: apport (pid 3743) Sat Nov 26 08:39:31 2016: debug: session gdbus call: (true,)

ERROR: apport (pid 3743) Sat Nov 26 08:39:31 2016: this executable already crashed 2 times, ignoring
ERROR: apport (pid 3753) Sat Nov 26 08:39:32 2016: called for pid 3752, signal 6, core limit 0
ERROR: apport (pid 3753) Sat Nov 26 08:39:32 2016: executable:
/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 (command line
"/opt/Isabelle2016-1-RC3/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 --full-saturate-quant --inst-when=full-last-call
--inst-no-entail --term-db-mode=relevant --no-statistics --random-seed=1 --lang=smt2 --continued-execution --tlimit 1071
/tmp/isabelle-gene/process7458968389934499957/cache-io-3954988")
ERROR: apport (pid 3753) Sat Nov 26 08:39:32 2016: debug: session gdbus call: (true,)

ERROR: apport (pid 3753) Sat Nov 26 08:39:32 2016: this executable already crashed 2 times, ignoring


On 11/04/2016 10:12 AM, Jasmin Blanchette wrote:
> 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.