Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] z3 crashing, too (was cvc4 crashing)


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

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
(In Isabelle2016-1-RC1)
This is maybe unrelated to the cvc4 issue, since this crash is with SIGSEGV.

- Gene Stark

ProblemType: Crash
Architecture: amd64
CrashCounter: 1
CurrentDesktop: Unity
Date: Thu Nov 3 04:46:21 2016
DistroRelease: Ubuntu 16.04
ExecutablePath: /opt/Isabelle2016-1-RC1/contrib/z3-4.4.0pre/x86_64-linux/z3
ExecutableTimestamp: 1428507126
ProcCmdline: /opt/Isabelle2016-1-RC1/contrib/z3-4.4.0pre/x86_64-linux/z3 smt.random_seed 1 smt.refine_inj_axioms false
-T 1 -smt2 /tmp/isabelle-gene/process3970109973954785755/cache-io-27359710
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-0114e000 r-xp 00000000 fc:00 677391
/opt/Isabelle2016-1-RC1/contrib/z3-4.4.0pre/x86_64-linux/z3
0134d000-01371000 r--p 00d4d000 fc:00 677391
/opt/Isabelle2016-1-RC1/contrib/z3-4.4.0pre/x86_64-linux/z3
01371000-01373000 rw-p 00d71000 fc:00 677391
/opt/Isabelle2016-1-RC1/contrib/z3-4.4.0pre/x86_64-linux/z3
01373000-01375000 rw-p 00000000 00:00 0
02c22000-02e85000 rw-p 00000000 00:00 0 [heap]
7f647c220000-7f647c223000 r-xp 00000000 fc:00 1180234 /lib/x86_64-linux-gnu/libdl-2.23.so
7f647c223000-7f647c422000 ---p 00003000 fc:00 1180234 /lib/x86_64-linux-gnu/libdl-2.23.so
7f647c422000-7f647c423000 r--p 00002000 fc:00 1180234 /lib/x86_64-linux-gnu/libdl-2.23.so
7f647c423000-7f647c424000 rw-p 00003000 fc:00 1180234 /lib/x86_64-linux-gnu/libdl-2.23.so
7f647c424000-7f647c5e4000 r-xp 00000000 fc:00 1180232 /lib/x86_64-linux-gnu/libc-2.23.so
7f647c5e4000-7f647c7e3000 ---p 001c0000 fc:00 1180232 /lib/x86_64-linux-gnu/libc-2.23.so
7f647c7e3000-7f647c7e7000 r--p 001bf000 fc:00 1180232 /lib/x86_64-linux-gnu/libc-2.23.so
7f647c7e7000-7f647c7e9000 rw-p 001c3000 fc:00 1180232 /lib/x86_64-linux-gnu/libc-2.23.so
7f647c7e9000-7f647c7ed000 rw-p 00000000 00:00 0
7f647c7ed000-7f647c803000 r-xp 00000000 fc:00 1179781 /lib/x86_64-linux-gnu/libgcc_s.so.1
7f647c803000-7f647ca02000 ---p 00016000 fc:00 1179781 /lib/x86_64-linux-gnu/libgcc_s.so.1
7f647ca02000-7f647ca03000 rw-p 00015000 fc:00 1179781 /lib/x86_64-linux-gnu/libgcc_s.so.1
7f647ca03000-7f647ca24000 r-xp 00000000 fc:00 789048 /usr/lib/x86_64-linux-gnu/libgomp.so.1.0.0
7f647ca24000-7f647cc23000 ---p 00021000 fc:00 789048 /usr/lib/x86_64-linux-gnu/libgomp.so.1.0.0
7f647cc23000-7f647cc24000 r--p 00020000 fc:00 789048 /usr/lib/x86_64-linux-gnu/libgomp.so.1.0.0
7f647cc24000-7f647cc25000 rw-p 00021000 fc:00 789048 /usr/lib/x86_64-linux-gnu/libgomp.so.1.0.0
7f647cc25000-7f647cd2d000 r-xp 00000000 fc:00 1180210 /lib/x86_64-linux-gnu/libm-2.23.so
7f647cd2d000-7f647cf2c000 ---p 00108000 fc:00 1180210 /lib/x86_64-linux-gnu/libm-2.23.so
7f647cf2c000-7f647cf2d000 r--p 00107000 fc:00 1180210 /lib/x86_64-linux-gnu/libm-2.23.so
7f647cf2d000-7f647cf2e000 rw-p 00108000 fc:00 1180210 /lib/x86_64-linux-gnu/libm-2.23.so
7f647cf2e000-7f647d0a0000 r-xp 00000000 fc:00 788013 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.21
7f647d0a0000-7f647d2a0000 ---p 00172000 fc:00 788013 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.21
7f647d2a0000-7f647d2aa000 r--p 00172000 fc:00 788013 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.21
7f647d2aa000-7f647d2ac000 rw-p 0017c000 fc:00 788013 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.21
7f647d2ac000-7f647d2b0000 rw-p 00000000 00:00 0
7f647d2b0000-7f647d2b7000 r-xp 00000000 fc:00 1180220 /lib/x86_64-linux-gnu/librt-2.23.so
7f647d2b7000-7f647d4b6000 ---p 00007000 fc:00 1180220 /lib/x86_64-linux-gnu/librt-2.23.so
7f647d4b6000-7f647d4b7000 r--p 00006000 fc:00 1180220 /lib/x86_64-linux-gnu/librt-2.23.so
7f647d4b7000-7f647d4b8000 rw-p 00007000 fc:00 1180220 /lib/x86_64-linux-gnu/librt-2.23.so
7f647d4b8000-7f647d4d0000 r-xp 00000000 fc:00 1180230 /lib/x86_64-linux-gnu/libpthread-2.23.so
7f647d4d0000-7f647d6cf000 ---p 00018000 fc:00 1180230 /lib/x86_64-linux-gnu/libpthread-2.23.so
7f647d6cf000-7f647d6d0000 r--p 00017000 fc:00 1180230 /lib/x86_64-linux-gnu/libpthread-2.23.so
7f647d6d0000-7f647d6d1000 rw-p 00018000 fc:00 1180230 /lib/x86_64-linux-gnu/libpthread-2.23.so
7f647d6d1000-7f647d6d5000 rw-p 00000000 00:00 0
7f647d6d5000-7f647d6fb000 r-xp 00000000 fc:00 1180224 /lib/x86_64-linux-gnu/ld-2.23.so
7f647d8a3000-7f647d8d3000 rw-p 00000000 00:00 0
7f647d8f0000-7f647d8f1000 ---p 00000000 00:00 0
7f647d8f1000-7f647d8fa000 rw-p 00000000 00:00 0
7f647d8fa000-7f647d8fb000 r--p 00025000 fc:00 1180224 /lib/x86_64-linux-gnu/ld-2.23.so
7f647d8fb000-7f647d8fc000 rw-p 00026000 fc:00 1180224 /lib/x86_64-linux-gnu/ld-2.23.so
7f647d8fc000-7f647d8fd000 rw-p 00000000 00:00 0
7fff06fb5000-7fff06fd9000 rw-p 00000000 00:00 0 [stack]
7fff06fec000-7fff06fee000 r--p 00000000 00:00 0 [vvar]
7fff06fee000-7fff06ff0000 r-xp 00000000 00:00 0 [vdso]
ffffffffff600000-ffffffffff601000 r-xp 00000000 00:00 0 [vsyscall]
ProcStatus:
Name: z3
State: S (sleeping)
Tgid: 15560
Ngid: 0
Pid: 15560
PPid: 15559
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: 15560
NSpid: 15560
NSpgid: 15558
NSsid: 15558
VmPeak: 37992 kB
VmSize: 37992 kB
VmLck: 0 kB
VmPin: 0 kB
VmHWM: 16324 kB
VmRSS: 16324 kB
VmData: 2752 kB
VmStk: 148 kB
VmExe: 13624 kB
VmLib: 4836 kB
VmPTE: 84 kB
VmPMD: 12 kB
VmSwap: 0 kB
HugetlbPages: 0 kB
Threads: 2
SigQ: 1/95164
SigPnd: 0000000000000000
ShdPnd: 0000000000000000
SigBlk: 0000000000000000
SigIgn: 0000000000001000
SigCgt: 0000000180000002
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: 3
nonvoluntary_ctxt_switches: 11
Signal: 11
Uname: Linux 4.4.0-45-generic x86_64
UserGroups: adm cdrom dialout dip lpadmin plugdev sambashare sudo vboxusers
_LogindSession: c2

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

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Eugene,

This is maybe unrelated to the cvc4 issue, since this crash is with SIGSEGV.

I believe this is completely unrelated. If you can reproduce this or future crashes reliably, please let us know and we'll inform the Z3 developers.

Cheers,

Jasmin


Last updated: Apr 18 2024 at 20:16 UTC