Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] cvc4 crashing (was: Isabelle2016-RC0: cvc4 cra...


view this post on Zulip Email Gateway (Aug 22 2022 at 14:13):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I can report that cvc4 has crashed in the same way under Isabelle2016-RC1
running on Ubuntu 16.04 LTS on the amd64 architecture. I have appended the
Ubuntu crash report (minus the core dump).

It looks to me like the cvc4 process is sleeping at the time it receives
a SIGABRT, which causes abnormal termination. I'm not quite sure why a
process would receive a SIGABRT while it is sleeping, unless for some
reason that is a mechanism being used to forcibly terminate the process.
If that is the case, perhaps there is some situation (due to the interaction
of some library code with the signal mechanism) under which the cvc4 process
can enter the kernel with the SIGABRT handler disabled, so that if the signal
happens to be delivered during that time the default action (core dump)
will occur.

- Gene Stark

ProblemType: Crash
Architecture: amd64
CurrentDesktop: Unity
Date: Sat Oct 29 05:37:47 2016
DistroRelease: Ubuntu 16.04
ExecutablePath: /opt/Isabelle2016-1-RC1/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4
ExecutableTimestamp: 1477554478
ProcCmdline: /opt/Isabelle2016-1-RC1/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4 --full-saturate-quant
--inst-when=full-last-call --inst-no-entail --term-db-mode=relevant --random-seed=1 --lang=smt2 --continued-execution
--tlimit 230 /tmp/isabelle-gene/process3970109973954785755/cache-io-3213828
ProcCwd: /home/gene
ProcEnviron:
SHELL=/bin/tcsh
TERM=xterm-256color
LD_LIBRARY_PATH=<set>
PATH=(custom, no user)
LANG=en_US.UTF-8
LANGUAGE=en_US
XDG_RUNTIME_DIR=<set>
ProcMaps:
00400000-01339000 r-xp 00000000 fc:00 540449
/opt/Isabelle2016-1-RC1/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4
01539000-01562000 rw-p 00f39000 fc:00 540449
/opt/Isabelle2016-1-RC1/contrib/cvc4-1.5pre-4/x86_64-linux/cvc4
01562000-01581000 rw-p 00000000 00:00 0
01dae000-02109000 rw-p 00000000 00:00 0 [heap]
7ff87477b000-7ff8754ff000 rw-p 00000000 00:00 0
7ffe6d241000-7ffe6d265000 rw-p 00000000 00:00 0 [stack]
7ffe6d2ac000-7ffe6d2ae000 r--p 00000000 00:00 0 [vvar]
7ffe6d2ae000-7ffe6d2b0000 r-xp 00000000 00:00 0 [vdso]
ffffffffff600000-ffffffffff601000 r-xp 00000000 00:00 0 [vsyscall]
ProcStatus:
Name: cvc4
State: S (sleeping)
Tgid: 10286
Ngid: 0
Pid: 10286
PPid: 2456
TracerPid: 0
Uid: 1000 1000 1000 1000
Gid: 1000 1000 1000 1000
FDSize: 64
Groups: 4 20 24 27 30 46 112 124 135 1000
NStgid: 10286
NSpid: 10286
NSpgid: 10284
NSsid: 10284
VmPeak: 33316 kB
VmSize: 33316 kB
VmLck: 0 kB
VmPin: 0 kB
VmHWM: 12460 kB
VmRSS: 12460 kB
VmData: 17416 kB
VmStk: 148 kB
VmExe: 15588 kB
VmLib: 0 kB
VmPTE: 64 kB
VmPMD: 12 kB
VmSwap: 0 kB
HugetlbPages: 0 kB
Threads: 1
SigQ: 1/95164
SigPnd: 0000000000000000
ShdPnd: 0000000000000000
SigBlk: 0000000000000002
SigIgn: 0000000000001000
SigCgt: 000000000080040a
CapInh: 0000000000000000
CapPrm: 0000000000000000
CapEff: 0000000000000000
CapBnd: 0000003fffffffff
CapAmb: 0000000000000000
Seccomp: 0
Cpus_allowed: f
Cpus_allowed_list: 0-3
Mems_allowed: 00000000,00000001
Mems_allowed_list: 0
voluntary_ctxt_switches: 2
nonvoluntary_ctxt_switches: 20
Signal: 6
Uname: Linux 4.4.0-45-generic x86_64
UserGroups: adm cdrom dialout dip lpadmin plugdev sambashare sudo vboxusers
_LogindSession: c2


Last updated: Apr 20 2024 at 08:16 UTC