Symbolic exploration using lps2lts-sym of the latest version of ltsmin is broken

[mlaveaux]

Here is the stack trace, something something global variables

#0  __pthread_kill_implementation (threadid=<optimized out>, signo=signo@entry=6, no_tid=no_tid@entry=0) at pthread_kill.c:44
#1  0x00007ffff38d08a3 in __pthread_kill_internal (signo=6, threadid=<optimized out>) at pthread_kill.c:78
#2  0x00007ffff387e8ee in __GI_raise (sig=sig@entry=6) at ../sysdeps/posix/raise.c:26
#3  0x00007ffff38668ff in __GI_abort () at abort.c:79
#4  0x00007ffff386681b in __assert_fail_base (fmt=0x7ffff39e5af8 "%s%s%s:%u: %s%sAssertion `%s' failed.\n%n", assertion=assertion@entry=0x7ffff7a84160 "!m_busy_flag", 
    file=file@entry=0x7ffff7a84080 "/root/mcrl2/libraries/utilities/include/mcrl2/utilities/shared_mutex.h", line=line@entry=249, function=function@entry=0x7ffff7a84128 "void mcrl2::utilities::shared_mutex::lock_shared_impl()")
    at assert.c:92
#5  0x00007ffff3876c57 in __assert_fail (assertion=0x7ffff7a84160 "!m_busy_flag", file=0x7ffff7a84080 "/root/mcrl2/libraries/utilities/include/mcrl2/utilities/shared_mutex.h", line=249, 
    function=0x7ffff7a84128 "void mcrl2::utilities::shared_mutex::lock_shared_impl()") at assert.c:101
#6  0x00007ffff75e854e in mcrl2::utilities::shared_mutex::lock_shared_impl (this=0x7ffff2a91858) at /root/mcrl2/libraries/utilities/include/mcrl2/utilities/shared_mutex.h:249
#7  0x00007ffff75e840f in mcrl2::utilities::shared_mutex::lock_shared (this=0x7ffff2a91858) at /root/mcrl2/libraries/utilities/include/mcrl2/utilities/shared_mutex.h:216
#8  0x00007ffff76152cb in atermpp::detail::thread_aterm_pool::create_appl<atermpp::aterm> (this=0x7ffff2a91848, term=..., sym=...) at /root/mcrl2/libraries/atermpp/include/mcrl2/atermpp/detail/thread_aterm_pool_implementation.h:59
#9  0x00007ffff420fc68 in atermpp::term_appl<atermpp::aterm>::term_appl<atermpp::term_appl<atermpp::aterm> > (this=0x7ffff42cf9a8 <mcrl2::core::detail::default_value_SortId()::t>, symbol=...)
    at /root/mcrl2/libraries/atermpp/include/mcrl2/atermpp/aterm_appl.h:166
#10 0x00007ffff42046c8 in mcrl2::core::detail::default_value_SortId () at /root/mcrl2/libraries/core/include/mcrl2/core/detail/default_values.h:289
#11 0x00007ffff420c5bb in mcrl2::core::detail::default_value_SortExpr () at /root/mcrl2/libraries/core/include/mcrl2/core/detail/default_values.h:1473
#12 0x00007ffff4204130 in mcrl2::core::detail::default_value_SortCons () at /root/mcrl2/libraries/core/include/mcrl2/core/detail/default_values.h:241
#13 0x00007ffff41f38c1 in __static_initialization_and_destruction_0 () at /root/mcrl2/libraries/core/source/core.cpp:187
#14 0x00007ffff41f6189 in _GLOBAL__sub_I_core.cpp(void) () at /root/mcrl2/libraries/core/source/core.cpp:362
#15 0x00007ffff7fce237 in call_init (env=0x7fffffffe050, argv=0x7fffffffe038, argc=2, l=<optimized out>) at dl-init.c:74

[mlaveaux]

Further investigation shows that this issue has been introduced between the latest release of ltsmin (v3.0.2) and the latest development version. Most notably it does not occur when ltsmin is built without Sylvan support. I suspect that the upgrade of Sylvan causes the same issues as we had with upgrading Sylvan in mCRL2. I am not sure how to fix this, Sylvan has changed something about how the worker threads interface.