Even though we have locks in context disposal, in some cases, the statistics thread seems to query the disposed Z3 context:
State 1: Checking 1 state invariants I@13:54:10.173
State 1: state invariant 7 holds. I@13:54:28.751
Z3 statistics for context 0... I@13:54:28.969
conflicts=52,decisions=147,propagations=515241,added eqs=1265660,mk clause=2838243,del clause=2043,minimized lits=41,num checks=1,mk bool var=2136404,arith eq adapter=20746,arith-lower=17273,arith-upper=20375,arith-fixed-eqs=8122,arith-conflicts=26,arith-bound-propagations-lp=4913,arith-diseq=8670,arith-make-feasible=93,arith-max-columns=44159,arith-max-rows=23640,arith-offset-eqs=673,arith-fixed-eqs=15342,rlimit count=91473338,max memory=4170.54,memory=4104.51,num allocs=3.3337290742732E13,time=0.181
I@13:54:28.969
#
# A fatal error has been detected by the Java Runtime Environment:
#
# SIGSEGV (0xb) at pc=0x00007ba55917c7fb, pid=349967, tid=350074
#
# JRE version: OpenJDK Runtime Environment (21.0.4+7) (build 21.0.4+7-Ubuntu-1ubuntu224.04)
# Java VM: OpenJDK 64-Bit Server VM (21.0.4+7-Ubuntu-1ubuntu224.04, mixed mode, sharing, tiered, compressed class ptrs, g1 gc, linux-amd64)
# Problematic frame:
# C [libz3.so+0x97c7fb] smt::context::undo_mk_bool_var()+0x6b
#
# Core dump will be written. Default location: Core dumps may be processed with "/usr/share/apport/apport -p%p -s%s -c%c -d%d -P%P -u%u -g%g -- %E" (or dumping to /home/igor/devl/era-consensus/spec/protocol-spec/simplified/core.349967)
#
# An error report file with more information is saved as:
# /home/igor/devl/era-consensus/spec/protocol-spec/simplified/hs_err_pid349967.log
[579.355s][warning][os] Loading hsdis library failed
#
# If you would like to submit a bug report, please visit:
# https://bugs.launchpad.net/ubuntu/+source/openjdk-21
# The crash happened outside the Java Virtual Machine in native code.
# See problematic frame for where to report the bug.
#
Even though we have locks in context disposal, in some cases, the statistics thread seems to query the disposed Z3 context: