You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
#
The text was updated successfully, but these errors were encountered:
Even though we have locks in context disposal, in some cases, the statistics thread seems to query the disposed Z3 context:
The text was updated successfully, but these errors were encountered: