Re: [isabelle] cvc4 crashing



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();
> }

So as far as Ubuntu is concerned, cvc4 terminated abnormally via SIGABRT.
It logs the crash and pops up a warning dialog on the desktop.

I wonder why cvc4 is programmed so that SIGINT ("user hits control C")
causes an abort as opposed to just plain termination.

						- Gene Stark




On 11/04/2016 08:55 AM, Jasmin Blanchette wrote:
> Dear Eugene, Makarius,
> 
> First, thank you, Eugene, for taking the time to reproduce the issue.
> 
> Makarius wrote:
> 
>> Shall we hand this over to the cvc4 guys? There might be still enough
>> time for our release, to get a clarification of this important fine point.
> 
> Indeed. I'll write to them right now on the CVC4 users mailing list. Indeed, I should have done so long ago.
> 
> Cheers,
> 
> Jasmin
> 
> 

execve("/opt/Isabelle2016-1-RC1/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4_real", ["/opt/Isabelle2016-1-RC1/contrib/"..., "--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--random-seed=1", "--lang=smt2", "--continued-execution", "--tlimit", "5757", "/tmp/isabelle-gene/process397010"...], [/* 176 vars */]) = 0
uname({sysname="Linux", nodename="home.starkeffect.com", ...}) = 0
brk(NULL)                               = 0x2cd3000
brk(0x2cd41c0)                          = 0x2cd41c0
arch_prctl(ARCH_SET_FS, 0x2cd3880)      = 0
brk(0x2cf51c0)                          = 0x2cf51c0
brk(0x2cf6000)                          = 0x2cf6000
gettimeofday({1478265799, 105987}, NULL) = 0
getpid()                                = 14765
mmap(NULL, 790528, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fc3f7253000
gettimeofday({1478265799, 106208}, NULL) = 0
clock_gettime(CLOCK_MONOTONIC, {574344, 268960906}) = 0
brk(0x2d18000)                          = 0x2d18000
sigaltstack({ss_sp=0x2cf5ac0, ss_flags=0, ss_size=8192}, NULL) = 0
getrlimit(RLIMIT_STACK, {rlim_cur=8192*1024, rlim_max=RLIM64_INFINITY}) = 0
setrlimit(RLIMIT_STACK, {rlim_cur=RLIM64_INFINITY, rlim_max=RLIM64_INFINITY}) = 0
getrlimit(RLIMIT_STACK, {rlim_cur=RLIM64_INFINITY, rlim_max=RLIM64_INFINITY}) = 0
rt_sigaction(SIGINT, {0x431ff0, [], SA_RESTORER|SA_SIGINFO, 0xdf9190}, NULL, 8) = 0
rt_sigaction(SIGXCPU, {0x431f90, [], SA_RESTORER|SA_SIGINFO, 0xdf9190}, NULL, 8) = 0
rt_sigaction(SIGSEGV, {0x432050, [], SA_RESTORER|SA_STACK|SA_SIGINFO, 0xdf9190}, NULL, 8) = 0
rt_sigaction(SIGILL, {0x432050, [], SA_RESTORER|SA_SIGINFO, 0xdf9190}, NULL, 8) = 0
gettimeofday({1478265799, 106439}, NULL) = 0
brk(0x2d39000)                          = 0x2d39000
brk(0x2d5d000)                          = 0x2d5d000
brk(0x2d81000)                          = 0x2d81000
brk(0x2da7000)                          = 0x2da7000
brk(0x2dd3000)                          = 0x2dd3000
mmap(NULL, 4460544, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fc3f6e12000
mmap(NULL, 4460544, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fc3f69d1000
brk(0x2df5000)                          = 0x2df5000
brk(0x2e17000)                          = 0x2e17000
brk(0x2e4d000)                          = 0x2e4d000
brk(0x2e77000)                          = 0x2e77000
brk(0x2e98000)                          = 0x2e98000
brk(0x2eb9000)                          = 0x2eb9000
brk(0x2eda000)                          = 0x2eda000
open("/tmp/isabelle-gene/process3970109973954785755/cache-io-31231432", O_RDONLY) = 4
stat("/tmp/isabelle-gene/process3970109973954785755/cache-io-31231432", {st_mode=S_IFREG|0664, st_size=67267, ...}) = 0
fstat(4, {st_mode=S_IFREG|0664, st_size=67267, ...}) = 0
mmap(NULL, 4096, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fc3f69d0000
read(4, "; --full-saturate-quant --inst-w"..., 65536) = 65536
read(4, "omp$ (pair$ (fun_app$ ?v6 (comp$"..., 4096) = 1731
close(4)                                = 0
munmap(0x7fc3f69d0000, 4096)            = 0
mmap(NULL, 274432, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fc3f698e000
munmap(0x7fc3f698e000, 274432)          = 0
brk(0x2efb000)                          = 0x2efb000
gettimeofday({1478265799, 107688}, NULL) = 0
gettimeofday({1478265799, 107725}, NULL) = 0
gettimeofday({1478265799, 107743}, NULL) = 0
gettimeofday({1478265799, 107759}, NULL) = 0
gettimeofday({1478265799, 107775}, NULL) = 0
gettimeofday({1478265799, 107793}, NULL) = 0
gettimeofday({1478265799, 107810}, NULL) = 0
gettimeofday({1478265799, 107826}, NULL) = 0
gettimeofday({1478265799, 107843}, NULL) = 0
gettimeofday({1478265799, 107859}, NULL) = 0

...

gettimeofday({1478265799, 151033}, NULL) = 0
gettimeofday({1478265799, 151150}, NULL) = 0
brk(0x306c000)                          = 0x306c000
gettimeofday({1478265799, 151195}, NULL) = 0
gettimeofday({1478265799, 151319}, NULL) = 0
gettimeofday({1478265799, 151351}, NULL) = 0
gettimeofday({1478265799, 151663}, NULL) = 0
gettimeofday({1478265799, 151702}, NULL) = 0
gettimeofday({1478265799, 152005}, NULL) = 0
gettimeofday({1478265799, 152042}, NULL) = 0
gettimeofday({1478265799, 152350}, NULL) = 0
gettimeofday({1478265799, 152388}, NULL) = 0
gettimeofday({1478265799, 152539}, NULL) = 0
gettimeofday({1478265799, 152568}, NULL) = 0
gettimeofday({1478265799, 152702}, NULL) = 0
gettimeofday({1478265799, 152733}, NULL) = 0
gettimeofday({1478265799, 152886}, NULL) = 0
gettimeofday({1478265799, 152917}, NULL) = 0
gettimeofday({1478265799, 153074}, NULL) = 0
gettimeofday({1478265799, 153104}, NULL) = 0
gettimeofday({1478265799, 153253}, NULL) = 0
gettimeofday({1478265799, 153321}, NULL) = 0
gettimeofday({1478265799, 153339}, NULL) = 0
gettimeofday({1478265799, 153351}, NULL) = 0
gettimeofday({1478265799, 153359}, NULL) = 0
times({tms_utime=3, tms_stime=0, tms_cutime=0, tms_cstime=0}) = 1775391350
times({tms_utime=3, tms_stime=0, tms_cutime=0, tms_cstime=0}) = 1775391350
clock_gettime(CLOCK_MONOTONIC, {574344, 316111956}) = 0
times({tms_utime=3, tms_stime=0, tms_cutime=0, tms_cstime=0}) = 1775391350
clock_gettime(CLOCK_MONOTONIC, {574344, 316130143}) = 0
times({tms_utime=3, tms_stime=0, tms_cutime=0, tms_cstime=0}) = 1775391350
times({tms_utime=3, tms_stime=0, tms_cutime=0, tms_cstime=0}) = 1775391350
times({tms_utime=3, tms_stime=0, tms_cutime=0, tms_cstime=0}) = 1775391350

...

times({tms_utime=66, tms_stime=31, tms_cutime=0, tms_cstime=0}) = 1775391565
times({tms_utime=66, tms_stime=31, tms_cutime=0, tms_cstime=0}) = 1775391565
times({tms_utime=66, tms_stime=31, tms_cutime=0, tms_cstime=0}) = 1775391565
times({tms_utime=66, tms_stime=31, tms_cutime=0, tms_cstime=0}) = 1775391565
times({tms_utime=66, tms_stime=31, tms_cutime=0, tms_cstime=0}) = 1775391565
times({tms_utime=66, tms_stime=31, tms_cutime=0, tms_cstime=0}) = 1775391565
clock_gettime(CLOCK_MONOTONIC, {574346, 470405093}) = 0
brk(0x3e8d000)                          = 0x3e8d000
brk(0x3ebe000)                          = 0x3ebe000
brk(0x3eea000)                          = 0x3eea000
brk(0x3f10000)                          = 0x3f10000
brk(0x3f31000)                          = 0x3f31000
brk(0x3f54000)                          = 0x3f54000
brk(0x3f75000)                          = 0x3f75000
brk(0x3f96000)                          = 0x3f96000
brk(0x3fb9000)                          = 0x3fb9000
times({tms_utime=67, tms_stime=31, tms_cutime=0, tms_cstime=0}) = 1775391566
brk(0x3fda000)                          = 0x3fda000
brk(0x4000000)                          = 0x4000000
brk(0x4024000)                          = 0x4024000
brk(0x404c000)                          = 0x404c000
brk(0x4082000)                          = 0x4082000
brk(0x40c2000)                          = 0x40c2000
brk(0x40fa000)                          = 0x40fa000
brk(0x412a000)                          = 0x412a000
brk(0x414b000)                          = 0x414b000
brk(0x4170000)                          = 0x4170000
brk(0x4191000)                          = 0x4191000
brk(0x41d5000)                          = 0x41d5000
brk(0x41f9000)                          = 0x41f9000
brk(0x421a000)                          = 0x421a000
brk(0x423b000)                          = 0x423b000
brk(0x425f000)                          = 0x425f000
brk(0x4280000)                          = 0x4280000
brk(0x42a3000)                          = 0x42a3000
brk(0x42c4000)                          = 0x42c4000
brk(0x42e5000)                          = 0x42e5000
brk(0x431b000)                          = 0x431b000
brk(0x435b000)                          = 0x435b000
brk(0x4393000)                          = 0x4393000
brk(0x43b5000)                          = 0x43b5000
brk(0x43dd000)                          = 0x43dd000
brk(0x440d000)                          = 0x440d000
brk(0x448d000)                          = 0x448d000
brk(0x44cd000)                          = 0x44cd000
brk(0x44ee000)                          = 0x44ee000
brk(0x450f000)                          = 0x450f000
brk(0x4536000)                          = 0x4536000
brk(0x4557000)                          = 0x4557000
brk(0x4578000)                          = 0x4578000
brk(0x45c4000)                          = 0x45c4000
brk(0x460d000)                          = 0x460d000
brk(0x463f000)                          = 0x463f000
brk(0x4662000)                          = 0x4662000
brk(0x46d8000)                          = 0x46d8000
brk(0x4711000)                          = 0x4711000
brk(0x473f000)                          = 0x473f000
brk(0x4760000)                          = 0x4760000
brk(0x4781000)                          = 0x4781000
brk(0x47a2000)                          = 0x47a2000
brk(0x47ce000)                          = 0x47ce000
brk(0x47ef000)                          = 0x47ef000
brk(0x4824000)                          = 0x4824000
brk(0x4848000)                          = 0x4848000
brk(0x4887000)                          = 0x4887000
brk(0x48e7000)                          = 0x48e7000
brk(0x4937000)                          = 0x4937000
brk(0x4958000)                          = 0x4958000
brk(0x49c1000)                          = 0x49c1000
brk(0x4a01000)                          = 0x4a01000
mmap(NULL, 790528, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fc3f634c000
mmap(NULL, 528384, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fc3f62cb000
brk(0x4a24000)                          = 0x4a24000
brk(0x4a47000)                          = 0x4a47000
brk(0x4a8d000)                          = 0x4a8d000
times({tms_utime=74, tms_stime=31, tms_cutime=0, tms_cstime=0}) = 1775391574
brk(0x4aae000)                          = 0x4aae000
brk(0x4acf000)                          = 0x4acf000
brk(0x4af0000)                          = 0x4af0000
brk(0x4b11000)                          = 0x4b11000
brk(0x4b32000)                          = 0x4b32000
brk(0x4b53000)                          = 0x4b53000
brk(0x4b74000)                          = 0x4b74000
brk(0x4b95000)                          = 0x4b95000
brk(0x4bb6000)                          = 0x4bb6000
brk(0x4bd8000)                          = 0x4bd8000
brk(0x4bf9000)                          = 0x4bf9000
brk(0x4c1a000)                          = 0x4c1a000
brk(0x4c3b000)                          = 0x4c3b000
brk(0x4c7a000)                          = 0x4c7a000
brk(0x4c9b000)                          = 0x4c9b000
clock_gettime(CLOCK_MONOTONIC, {574346, 573323696}) = 0
clock_gettime(CLOCK_MONOTONIC, {574346, 573339863}) = 0
times({tms_utime=76, tms_stime=31, tms_cutime=0, tms_cstime=0}) = 1775391576
brk(0x4cd9000)                          = 0x4cd9000
brk(0x4cfa000)                          = 0x4cfa000
brk(0x4d1b000)                          = 0x4d1b000
brk(0x4d3c000)                          = 0x4d3c000
brk(0x4d5d000)                          = 0x4d5d000
brk(0x4d81000)                          = 0x4d81000
brk(0x4da3000)                          = 0x4da3000
brk(0x4dc6000)                          = 0x4dc6000
brk(0x4de7000)                          = 0x4de7000
brk(0x4e08000)                          = 0x4e08000
brk(0x4e29000)                          = 0x4e29000
brk(0x4e4a000)                          = 0x4e4a000
brk(0x4e73000)                          = 0x4e73000
brk(0x4e95000)                          = 0x4e95000
brk(0x4ebe000)                          = 0x4ebe000
brk(0x4edf000)                          = 0x4edf000
brk(0x4f19000)                          = 0x4f19000
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
clock_gettime(CLOCK_MONOTONIC, {574346, 634706517}) = 0
brk(0x4f3a000)                          = 0x4f3a000
mmap(NULL, 790528, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, -1, 0) = 0x7fc3f620a000
brk(0x4f81000)                          = 0x4f81000
clock_gettime(CLOCK_MONOTONIC, {574346, 639091777}) = 0
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
clock_gettime(CLOCK_MONOTONIC, {574346, 639148374}) = 0
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
clock_gettime(CLOCK_MONOTONIC, {574346, 639505911}) = 0
clock_gettime(CLOCK_MONOTONIC, {574346, 639524027}) = 0
clock_gettime(CLOCK_MONOTONIC, {574346, 639534898}) = 0
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582
times({tms_utime=82, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391582

...

clock_gettime(CLOCK_MONOTONIC, {574346, 664332065}) = 0
clock_gettime(CLOCK_MONOTONIC, {574346, 664339639}) = 0
times({tms_utime=83, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391585
clock_gettime(CLOCK_MONOTONIC, {574346, 664355428}) = 0
clock_gettime(CLOCK_MONOTONIC, {574346, 664364971}) = 0
clock_gettime(CLOCK_MONOTONIC, {574346, 664373588}) = 0
clock_gettime(CLOCK_MONOTONIC, {574346, 664382285}) = 0
times({tms_utime=83, tms_stime=32, tms_cutime=0, tms_cstime=0}) = 1775391585
clock_gettime(CLOCK_MONOTONIC, {574346, 664398105}) = 0
clock_gettime(CLOCK_MONOTONIC, {574346, 664406825}) = 0
clock_gettime(CLOCK_MONOTONIC, {574346, 664414900}) = 0
clock_gettime(CLOCK_MONOTONIC, {574346, 664424158}) = 0
brk(0x5056000)                          = 0x5056000
brk(0x5077000)                          = 0x5077000
clock_gettime(CLOCK_MONOTONIC, {574346, 674643892}) = 0
brk(0x5099000)                          = 0x5099000
brk(0x50ba000)                          = 0x50ba000
brk(0x50db000)                          = 0x50db000
brk(0x50fc000)                          = 0x50fc000
brk(0x511d000)                          = 0x511d000
brk(0x513e000)                          = 0x513e000
brk(0x515f000)                          = 0x515f000
brk(0x5180000)                          = 0x5180000
brk(0x51a1000)                          = 0x51a1000
brk(0x51c2000)                          = 0x51c2000
brk(0x51e3000)                          = 0x51e3000
brk(0x5204000)                          = 0x5204000
brk(0x5225000)                          = 0x5225000
brk(0x5246000)                          = 0x5246000
brk(0x5267000)                          = 0x5267000
brk(0x5288000)                          = 0x5288000
brk(0x52a9000)                          = 0x52a9000
brk(0x52ca000)                          = 0x52ca000
brk(0x52eb000)                          = 0x52eb000
brk(0x530c000)                          = 0x530c000
brk(0x532d000)                          = 0x532d000
brk(0x534e000)                          = 0x534e000
brk(0x536f000)                          = 0x536f000
--- SIGINT {si_signo=SIGINT, si_code=SI_USER, si_pid=4567, si_uid=1000} ---
write(2, "CVC4 interrupted by user.\n", 26) = 26
rt_sigprocmask(SIG_UNBLOCK, [ABRT], NULL, 8) = 0
tgkill(14765, 14765, SIGABRT)           = 0
--- SIGABRT {si_signo=SIGABRT, si_code=SI_TKILL, si_pid=14765, si_uid=1000} ---
+++ killed by SIGABRT (core dumped) +++


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