[isabelle] cvc4 crashing (was: Re: Isabelle2016-RC0: cvc4 crashing)

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
 PATH=(custom, no user)
 00400000-01339000 r-xp 00000000 fc:00 540449
 01539000-01562000 rw-p 00f39000 fc:00 540449
 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]
 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

On 10/27/2016 08:51 AM, Jasmin Blanchette wrote:
> Dear Eugene,
>> But now before I can get back to what I was doing and report on whether CVC4 is still crashing,
> Please let us know how this goes. Regardless, the next release candidate will likely feature a new version of CVC4.
>> I need to know what the new warning "Not a proper equation" means in a
>> datatype definition as follows (also attached):
> Thank you for your report. In short, the code generator is now more verbose, and the "datatype" package interacts with it. I have a solution locally to get rid of the warning that is likely to be part of the next release candidate.
>> Another issue I noticed: JEdit now forcibly resets the indentations of lines
>> with keywords such as "locale" when I type the keyword, or, what is even
>> more irritating, when I type ENTER at the end of the line.  I think this
>> new behavior is fairly disruptive of the typing habits I have established
>> to this point.
> I guess this is for Makarius to answer.
> Cheers,
> Jasmin

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