[ 0:00] --symbolic --sequential -o nofail:malloc
[ 0:00] + divine cc -o testcase.bc -DSIZE=1000 /var/obj/divine-nightly/semidbg/test/_expand/svcomp/array/standard_copy3_false.pkg.c/v.1000.c
[ 0:00] compiling /var/obj/divine-nightly/semidbg/test/_expand/svcomp/array/standard_copy3_false.pkg.c/v.1000.c
[ 0:00] + divine verify --max-memory 4GiB --threads 1 --report-filename verify.out --solver z3 --symbolic --sequential -o nofail:malloc testcase.bc
[ 0:00] /home/xrockai/src/divine/nightly/test/lib/verify: line 15:  2369 Segmentation fault      (core dumped) divine "$@"
[ 0:17] (lldb) target create "/var/obj/divine-nightly/semidbg/tools/divine" --core "core"
[ 0:17] Core file '/var/obj/divine-nightly/semidbg/test/__test_work_dir.0/core' (x86_64) was loaded.
[ 0:39] (lldb) bt all
[ 0:39] * thread #1, name = 'divine', stop reason = signal SIGSEGV
[ 0:40]   * frame #0: 0x00007f189dc42512 libdivine-ui.so`void divine::mem::Metadata<divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > > >::hash<brick::hash::State, divine::mem::Data<divine::mem::UserMeta<divine::mem::Metadata<divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > > > > >::hash_data(brick::mem::PoolPointer<divine::mem::PoolRep<20> >) const::'lambda'(unsigned int)>(brick::mem::PoolPointer<divine::mem::PoolRep<20> >, int, brick::hash::State&, divine::mem::Data<divine::mem::UserMeta<divine::mem::Metadata<divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > > > > >::hash_data(brick::mem::PoolPointer<divine::mem::PoolRep<20> >) const::'lambda'(unsigned int)) const [inlined] brick::hash::tail(unsigned long, unsigned int) at brick-hash:61
[ 0:40]     frame #1: 0x00007f189dc424fe libdivine-ui.so`void divine::mem::Metadata<divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > > >::hash<brick::hash::State, divine::mem::Data<divine::mem::UserMeta<divine::mem::Metadata<divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > > > > >::hash_data(brick::mem::PoolPointer<divine::mem::PoolRep<20> >) const::'lambda'(unsigned int)>(brick::mem::PoolPointer<divine::mem::PoolRep<20> >, int, brick::hash::State&, divine::mem::Data<divine::mem::UserMeta<divine::mem::Metadata<divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > > > > >::hash_data(brick::mem::PoolPointer<divine::mem::PoolRep<20> >) const::'lambda'(unsigned int)) const [inlined] brick::hash::State::update_aligned(this=<unavailable>, data=<unavailable>, count=<unavailable>) at brick-hash:174
[ 0:40]     frame #2: 0x00007f189dc42332 libdivine-ui.so`void divine::mem::Metadata<divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > > >::hash<brick::hash::State, divine::mem::Data<divine::mem::UserMeta<divine::mem::Metadata<divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > > > > >::hash_data(this=<unavailable>, i=<unavailable>, size=<unavailable>, state=<unavailable>, ptr_cb=<unavailable>) const::'lambda'(unsigned int)>(brick::mem::PoolPointer<divine::mem::PoolRep<20> >, int, brick::hash::State&, divine::mem::Data<divine::mem::UserMeta<divine::mem::Metadata<divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > > > > >::hash_data(brick::mem::PoolPointer<divine::mem::PoolRep<20> >) const::'lambda'(unsigned int)) const at metadata.hpp:278
[ 0:40]     frame #3: 0x00007f189dc4137d libdivine-ui.so`divine::mem::Data<divine::mem::UserMeta<divine::mem::Metadata<divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > > > > >::hash_data(this=0x0000000009a626d8, i=divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > >::Internal @ r14) const at data.hpp:67
[ 0:40]     frame #4: 0x00007f189dc8763d libdivine-ui.so`divine::mem::Cow<divine::mem::Data<divine::mem::UserMeta<divine::mem::Metadata<divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > > > > > >::snap_dedup(divine::mem::Data<divine::mem::UserMeta<divine::mem::Metadata<divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > > > > >::SnapItem) const [inlined] divine::mem::Cow<divine::mem::Data<divine::mem::UserMeta<divine::mem::Metadata<divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > > > > > >::ObjHasher::hash(this=0x0000000009a62870, i=<unavailable>) const at cow.hpp:52
[ 0:40]     frame #5: 0x00007f189dc87631 libdivine-ui.so`divine::mem::Cow<divine::mem::Data<divine::mem::UserMeta<divine::mem::Metadata<divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > > > > > >::snap_dedup(divine::mem::Data<divine::mem::UserMeta<divine::mem::Metadata<divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > > > > >::SnapItem) const [inlined] brick::hashset::HashSetBase<brick::hashset::AtomicCell<brick::mem::PoolPointer<divine::mem::PoolRep<20> > > >::iterator brick::hashset::HashSet<brick::hashset::AtomicCell<brick::mem::PoolPointer<divine::mem::PoolRep<20> > >, true, brick::hashset::Grow<256ul, 4096ul, 65536ul, 524288ul, 1048576ul, 4194304ul>, 24>::insert<brick::mem::PoolPointer<divine::mem::PoolRep<20> >, divine::mem::Cow<divine::mem::Data<divine::mem::UserMeta<divine::mem::Metadata<divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > > > > > >::ObjHasher>(this=0x0000000009a62878, x=0x00007f188d005444, adaptor=0x0000000009a62870) at brick-hashset:570
[ 0:40]     frame #6: 0x00007f189dc8762c libdivine-ui.so`divine::mem::Cow<divine::mem::Data<divine::mem::UserMeta<divine::mem::Metadata<divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > > > > > >::snap_dedup(this=0x0000000009a626d8, si=SnapItem @ 0x00007f188d005440) const at cow.tpp:63
[ 0:40]     frame #7: 0x00007f189dc871fa libdivine-ui.so`divine::mem::Cow<divine::mem::Data<divine::mem::UserMeta<divine::mem::Metadata<divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > > > > > >::snapshot(this=0x0000000009a626d8, p=<unavailable>) const at cow.tpp:115
[ 0:40]     frame #8: 0x00007f189dd1d722 libdivine-ui.so`std::__2::__function::__func<divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::pseudoBFS()::'lambda0'(), std::__2::allocator<divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::pseudoBFS()::'lambda0'()>, void ()>::operator()() [inlined] divine::mem::Frontend<divine::mem::Cow<divine::mem::Data<divine::mem::UserMeta<divine::mem::Metadata<divine::mem::TaintLayer<divine::mem::DefinednessLayer<divine::mem::PointerLayer<divine::mem::ShadowBase<divine::mem::CompressPDT<divine::mem::Base<divine::vm::HeapPointer, divine::vm::value::Pointer, divine::vm::value::FixInt, brick::mem::Pool<divine::mem::PoolRep<20> > > > > > > > > > > > >::snapshot(this=<unavailable>, p=<unavailable>) at frontend.hpp:118
[ 0:40]     frame #9: 0x00007f189dd1d710 libdivine-ui.so`std::__2::__function::__func<divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::pseudoBFS()::'lambda0'(), std::__2::allocator<divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::pseudoBFS()::'lambda0'()>, void ()>::operator()() at builder.hpp:268
[ 0:40]     frame #10: 0x00007f189dd1ce5f libdivine-ui.so`std::__2::__function::__func<divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::pseudoBFS()::'lambda0'(), std::__2::allocator<divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::pseudoBFS()::'lambda0'()>, void ()>::operator()() [inlined] void divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::_succs<divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(this=<unavailable>, l=<unavailable>, b=<unavailable>)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::pseudoBFS()::'lambda0'()::operator()()::'lambda'(auto, auto, bool)>(divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1>&, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >&, divine::mc::builder::State, auto) at search.hpp:107
[ 0:40]     frame #11: 0x00007f189dd1ce5f libdivine-ui.so`std::__2::__function::__func<divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::pseudoBFS()::'lambda0'(), std::__2::allocator<divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::pseudoBFS()::'lambda0'()>, void ()>::operator()() at search.hpp:149
[ 0:40]     frame #12: 0x00007f189dd1cb49 libdivine-ui.so`std::__2::__function::__func<divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::pseudoBFS()::'lambda0'(), std::__2::allocator<divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::pseudoBFS()::'lambda0'()>, void ()>::operator()() [inlined] decltype(__f=<unavailable>)()) std::__2::__invoke<divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::pseudoBFS()::'lambda0'()&>(auto&&) at type_traits:4301
[ 0:40]     frame #13: 0x00007f189dd1cb49 libdivine-ui.so`std::__2::__function::__func<divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::pseudoBFS()::'lambda0'(), std::__2::allocator<divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::pseudoBFS()::'lambda0'()>, void ()>::operator()() [inlined] void std::__2::__invoke_void_return_wrapper<void>::__call<divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(__args=<unavailable>)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::pseudoBFS()::'lambda0'()&>(divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::pseudoBFS()::'lambda0'()&) at __functional_base:359
[ 0:40]     frame #14: 0x00007f189dd1cb49 libdivine-ui.so`std::__2::__function::__func<divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::pseudoBFS()::'lambda0'(), std::__2::allocator<divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::pseudoBFS()::'lambda0'()>, void ()>::operator(this=0x0000000009a625b0)() at functional:1552
[ 0:40]     frame #15: 0x00007f189dcedd19 libdivine-ui.so`std::__2::__async_assoc_state<void, std::__2::__async_func<std::__2::function<void ()> > >::__execute() [inlined] std::__2::function<void ()>::operator(this=<unavailable>)() const at functional:1914
[ 0:40]     frame #16: 0x00007f189dcedd07 libdivine-ui.so`std::__2::__async_assoc_state<void, std::__2::__async_func<std::__2::function<void ()> > >::__execute() [inlined] decltype(__f=<unavailable>)> >(fp)()) std::__2::__invoke<std::__2::function<void ()> >(std::__2::function<void ()>&&) at type_traits:4301
[ 0:40]     frame #17: 0x00007f189dcedd07 libdivine-ui.so`std::__2::__async_assoc_state<void, std::__2::__async_func<std::__2::function<void ()> > >::__execute() [inlined] void std::__2::__async_func<std::__2::function<void ()> >::__execute<>(this=<unavailable>) at future:2324
[ 0:40]     frame #18: 0x00007f189dcedd07 libdivine-ui.so`std::__2::__async_assoc_state<void, std::__2::__async_func<std::__2::function<void ()> > >::__execute() [inlined] std::__2::__async_func<std::__2::function<void ()> >::operator(this=<unavailable>)() at future:2317
[ 0:40]     frame #19: 0x00007f189dcedd07 libdivine-ui.so`std::__2::__async_assoc_state<void, std::__2::__async_func<std::__2::function<void ()> > >::__execute(this=0x000000000a247920) at future:1035
[ 0:40]     frame #20: 0x00007f189dcedde8 libdivine-ui.so`void* std::__2::__thread_proxy<std::__2::tuple<std::__2::unique_ptr<std::__2::__thread_struct, std::__2::default_delete<std::__2::__thread_struct> >, void (std::__2::__async_assoc_state<void, std::__2::__async_func<std::__2::function<void ()> > >::*)(), std::__2::__async_assoc_state<void, std::__2::__async_func<std::__2::function<void ()> > >*> >(void*) [inlined] decltype(__f=<unavailable>, __a0=<unavailable>)> > >*>(fp0)).*fp()) std::__2::__invoke<void (std::__2::__async_assoc_state<void, std::__2::__async_func<std::__2::function<void ()> > >::*)(), std::__2::__async_assoc_state<void, std::__2::__async_func<std::__2::function<void ()> > >*, void>(void (std::__2::__async_assoc_state<void, std::__2::__async_func<std::__2::function<void ()> > >::*&&)(), std::__2::__async_assoc_state<void, std::__2::__async_func<std::__2::function<void ()> > >*&&) at type_traits:4242
[ 0:40]     frame #21: 0x00007f189dceddce libdivine-ui.so`void* std::__2::__thread_proxy<std::__2::tuple<std::__2::unique_ptr<std::__2::__thread_struct, std::__2::default_delete<std::__2::__thread_struct> >, void (std::__2::__async_assoc_state<void, std::__2::__async_func<std::__2::function<void ()> > >::*)(), std::__2::__async_assoc_state<void, std::__2::__async_func<std::__2::function<void ()> > >*> >(void*) [inlined] void std::__2::__thread_execute<std::__2::unique_ptr<std::__2::__thread_struct, std::__2::default_delete<std::__2::__thread_struct> >, void (std::__2::__async_assoc_state<void, std::__2::__async_func<std::__2::function<void ()> > >::*)(), std::__2::__async_assoc_state<void, std::__2::__async_func<std::__2::function<void ()> > >*, 2ul>(std::__2::tuple<std::__2::unique_ptr<std::__2::__thread_struct, std::__2::default_delete<std::__2::__thread_struct> >, void (std::__2::__async_assoc_state<void, std::__2::__async_func<std::__2::function<void ()> > >::*)(), std::__2::__async_assoc_state<void, std::__2::__async_func<std::__2::function<void ()> > >*>&, std::__2::__tuple_indices<2ul>) at thread:336
[ 0:40]     frame #22: 0x00007f189dceddce libdivine-ui.so`void* std::__2::__thread_proxy<std::__2::tuple<std::__2::unique_ptr<std::__2::__thread_struct, std::__2::default_delete<std::__2::__thread_struct> >, void (std::__2::__async_assoc_state<void, std::__2::__async_func<std::__2::function<void ()> > >::*)(), std::__2::__async_assoc_state<void, std::__2::__async_func<std::__2::function<void ()> > >*> >(__vp=0x000000000c4bc810) at thread:346
[ 0:40]     frame #23: 0x00007f189d8eca9d libpthread.so.0`start_thread + 253
[ 0:40]     frame #24: 0x00007f189505ab23 libc.so.6`__GI___clone + 67
[ 0:40]   thread #2, stop reason = signal 0
[ 0:40]     frame #0: 0x00007f189d8f2e5b libpthread.so.0`__pthread_cond_timedwait + 603
[ 0:40]     frame #1: 0x00007f1895339967 libc++.so.2`std::__2::condition_variable::__do_timed_wait(std::__2::unique_lock<std::__2::mutex>&, std::__2::chrono::time_point<std::__2::chrono::system_clock, std::__2::chrono::duration<long long, std::__2::ratio<1l, 1000000000l> > >) [inlined] std::__2::__libcpp_condvar_timedwait(__ts=<unavailable>, __m=<unavailable>, __cv=<unavailable>) at __threading_support:284
[ 0:40]     frame #2: 0x00007f1895339962 libc++.so.2`std::__2::condition_variable::__do_timed_wait(this=<unavailable>, lk=<unavailable>, tp=<unavailable>) at condition_variable.cpp:74
[ 0:40]     frame #3: 0x00007f189dcee135 libdivine-ui.so`std::__2::cv_status std::__2::condition_variable::wait_until<std::__2::chrono::steady_clock, std::__2::chrono::duration<long long, std::__2::ratio<1l, 1000000000l> > >(std::__2::unique_lock<std::__2::mutex>&, std::__2::chrono::time_point<std::__2::chrono::steady_clock, std::__2::chrono::duration<long long, std::__2::ratio<1l, 1000000000l> > > const&) [inlined] std::__2::cv_status std::__2::condition_variable::wait_for<long long, std::__2::ratio<1l, 1000000000l> >(this=0x0000000009e87250, __lk=0x00007ffdb6500c00) at __mutex_base:0
[ 0:40]     frame #4: 0x00007f189dcee0dd libdivine-ui.so`std::__2::cv_status std::__2::condition_variable::wait_until<std::__2::chrono::steady_clock, std::__2::chrono::duration<long long, std::__2::ratio<1l, 1000000000l> > >(this=0x0000000009e87250, __lk=0x00007ffdb6500c00, __t=0x00007ffdb6500c48) at __mutex_base:384
[ 0:40]     frame #5: 0x00007f189dcee058 libdivine-ui.so`std::__2::future_status std::__2::__assoc_sub_state::wait_until<std::__2::chrono::steady_clock, std::__2::chrono::duration<long long, std::__2::ratio<1l, 1000000000l> > >(this=0x0000000009e87210, __abs_time=0x00007ffdb6500c48) const at future:599
[ 0:40]     frame #6: 0x00007f189dd869c8 libdivine-ui.so`divine::mc::Job::wait() [inlined] std::__2::future_status std::__2::future<void>::wait_until<std::__2::chrono::steady_clock, std::__2::chrono::duration<long long, std::__2::ratio<1l, 1000000000l> > >(__abs_time=<unavailable>) const at future:1346
[ 0:40]     frame #7: 0x00007f189dd869ae libdivine-ui.so`divine::mc::Job::wait() at brick-shmem:658
[ 0:40]     frame #8: 0x00007f189dd869a4 libdivine-ui.so`divine::mc::Job::wait(this=0x000000000ba4e570) at job.hpp:54
[ 0:40]     frame #9: 0x00007f189dd164f2 libdivine-ui.so`divine::ui::Verify::safety(this=0x00007ffdb6501598) at verify.cpp:169
[ 0:40]     frame #10: 0x00007f189dbd4817 libdivine-ui.so`brick::types::Maybe<brick::types::_impl::_ApplyResult<divine::ui::CLI::main()::'lambda'(divine::ui::Command&), divine::ui::Ltlc, brick::types::Unit, bool>::Result> brick::types::_impl::Union<true, divine::ui::Ltlc, divine::ui::Help, divine::ui::Version, divine::ui::Cc, divine::ui::Info, divine::ui::Draw, divine::ui::Sim, divine::ui::Exec, divine::ui::Check, divine::ui::Verify>::_apply<divine::ui::CLI::main()::'lambda'(divine::ui::Command&), divine::ui::Ltlc, divine::ui::Help, divine::ui::Version, divine::ui::Cc, divine::ui::Info, divine::ui::Draw, divine::ui::Sim, divine::ui::Exec, divine::ui::Check, divine::ui::Verify>(brick::types::Preferred, divine::ui::CLI::main()::'lambda'(divine::ui::Command&)) [inlined] divine::ui::CLI::main(c=0x00007ffdb6501598)::'lambda'(divine::ui::Command&)::operator()(divine::ui::Command&) const at parser.hpp:338
[ 0:40]     frame #11: 0x00007f189dbd4806 libdivine-ui.so`brick::types::Maybe<brick::types::_impl::_ApplyResult<divine::ui::CLI::main()::'lambda'(divine::ui::Command&), divine::ui::Ltlc, brick::types::Unit, bool>::Result> brick::types::_impl::Union<true, divine::ui::Ltlc, divine::ui::Help, divine::ui::Version, divine::ui::Cc, divine::ui::Info, divine::ui::Draw, divine::ui::Sim, divine::ui::Exec, divine::ui::Check, divine::ui::Verify>::_apply<divine::ui::CLI::main()::'lambda'(divine::ui::Command&), divine::ui::Ltlc, divine::ui::Help, divine::ui::Version, divine::ui::Cc, divine::ui::Info, divine::ui::Draw, divine::ui::Sim, divine::ui::Exec, divine::ui::Check, divine::ui::Verify>(brick::types::Preferred, divine::ui::CLI::main()::'lambda'(divine::ui::Command&)) [inlined] std::__2::enable_if<std::is_void<brick::types::Maybe<brick::types::_impl::ApplyResult<divine::ui::CLI::main()::'lambda'(divine::ui::Command&), divine::ui::Ltlc, divine::ui::Help, divine::ui::Version, divine::ui::Cc, divine::ui::Info, divine::ui::Draw, divine::ui::Sim, divine::ui::Exec, divine::ui::Check, divine::ui::Verify>::Result>::T>::value, brick::types::Maybe<brick::types::_impl::ApplyResult<divine::ui::CLI::main()::'lambda'(divine::ui::Command&), divine::ui::Ltlc, divine::ui::Help, divine::ui::Version, divine::ui::Cc, divine::ui::Info, divine::ui::Draw, divine::ui::Sim, divine::ui::Exec, divine::ui::Check, divine::ui::Verify>::Result> >::type brick::types::_impl::Union<true, divine::ui::Ltlc, divine::ui::Help, divine::ui::Version, divine::ui::Cc, divine::ui::Info, divine::ui::Draw, divine::ui::Sim, divine::ui::Exec, divine::ui::Check, divine::ui::Verify>::fixvoid<divine::ui::CLI::main()::'lambda'(divine::ui::Command&), divine::ui::Ltlc>(divine::ui::CLI::main()::'lambda'(divine::ui::Command&)) at brick-types:780
[ 0:40]     frame #12: 0x00007f189dbd47f5 libdivine-ui.so`brick::types::Maybe<brick::types::_impl::_ApplyResult<divine::ui::CLI::main()::'lambda'(divine::ui::Command&), divine::ui::Ltlc, brick::types::Unit, bool>::Result> brick::types::_impl::Union<true, divine::ui::Ltlc, divine::ui::Help, divine::ui::Version, divine::ui::Cc, divine::ui::Info, divine::ui::Draw, divine::ui::Sim, divine::ui::Exec, divine::ui::Check, divine::ui::Verify>::_apply<divine::ui::CLI::main(this=0x00007ffdb6501598, (null)=<unavailable>, f=<unavailable>)::'lambda'(divine::ui::Command&), divine::ui::Ltlc, divine::ui::Help, divine::ui::Version, divine::ui::Cc, divine::ui::Info, divine::ui::Draw, divine::ui::Sim, divine::ui::Exec, divine::ui::Check, divine::ui::Verify>(brick::types::Preferred, divine::ui::CLI::main()::'lambda'(divine::ui::Command&)) at brick-types:797
[ 0:40]     frame #13: 0x00007f189db8249f libdivine-ui.so`divine::ui::CLI::main() [inlined] brick::types::Maybe<brick::types::_impl::ApplyResult<divine::ui::CLI::main()::'lambda'(divine::ui::Command&), divine::ui::Ltlc, divine::ui::Help, divine::ui::Version, divine::ui::Cc, divine::ui::Info, divine::ui::Draw, divine::ui::Sim, divine::ui::Exec, divine::ui::Check, divine::ui::Verify>::Result> brick::types::_impl::Union<true, divine::ui::Ltlc, divine::ui::Help, divine::ui::Version, divine::ui::Cc, divine::ui::Info, divine::ui::Draw, divine::ui::Sim, divine::ui::Exec, divine::ui::Check, divine::ui::Verify>::apply<divine::ui::CLI::main(this=<unavailable>)::'lambda'(divine::ui::Command&)>(divine::ui::CLI::main()::'lambda'(divine::ui::Command&)) at brick-types:621
[ 0:40]     frame #14: 0x00007f189db8249a libdivine-ui.so`divine::ui::CLI::main() [inlined] brick::types::Maybe<void> brick::types::_impl::Union<true, divine::ui::Ltlc, divine::ui::Help, divine::ui::Version, divine::ui::Cc, divine::ui::Info, divine::ui::Draw, divine::ui::Sim, divine::ui::Exec, divine::ui::Check, divine::ui::Verify>::_match<brick::types::Maybe<void>, divine::ui::CLI::main(this=<unavailable>)::'lambda'(divine::ui::Command&)>(divine::ui::CLI::main()::'lambda'(divine::ui::Command&)) at brick-types:631
[ 0:40]     frame #15: 0x00007f189db8249a libdivine-ui.so`divine::ui::CLI::main() [inlined] brick::types::Maybe<void> brick::types::_impl::Union<true, divine::ui::Ltlc, divine::ui::Help, divine::ui::Version, divine::ui::Cc, divine::ui::Info, divine::ui::Draw, divine::ui::Sim, divine::ui::Exec, divine::ui::Check, divine::ui::Verify>::_match<brick::types::Maybe<void>, divine::ui::CLI::main()::'lambda'(divine::ui::Help&), divine::ui::CLI::main()::'lambda'(divine::ui::Command&)&>(divine::ui::CLI::main()::'lambda'(divine::ui::Help&), divine::ui::CLI::main()::'lambda'(divine::ui::Command&)&) at brick-types:633
[ 0:40]     frame #16: 0x00007f189db82489 libdivine-ui.so`divine::ui::CLI::main() [inlined] brick::types::Maybe<brick::types::_impl::ApplyResult<divine::ui::CLI::main()::'lambda'(divine::ui::Help&), divine::ui::Ltlc, divine::ui::Help, divine::ui::Version, divine::ui::Cc, divine::ui::Info, divine::ui::Draw, divine::ui::Sim, divine::ui::Exec, divine::ui::Check, divine::ui::Verify>::Result> brick::types::_impl::Union<true, divine::ui::Ltlc, divine::ui::Help, divine::ui::Version, divine::ui::Cc, divine::ui::Info, divine::ui::Draw, divine::ui::Sim, divine::ui::Exec, divine::ui::Check, divine::ui::Verify>::match<divine::ui::CLI::main()::'lambda'(divine::ui::Help&), divine::ui::CLI::main()::'lambda'(divine::ui::Command&)>(divine::ui::CLI::main()::'lambda'(divine::ui::Help&), divine::ui::CLI::main()::'lambda'(divine::ui::Command&)&&) at brick-types:644
[ 0:40]     frame #17: 0x00007f189db82489 libdivine-ui.so`divine::ui::CLI::main(this=<unavailable>) at parser.hpp:331
[ 0:40]     frame #18: 0x000000000041e0a4 divine`main(argc=<unavailable>, argv=0x00007ffdb6502338) at divine.cpp:76
[ 0:40]     frame #19: 0x00007f1894f83223 libc.so.6`__libc_start_main + 243
[ 0:40]     frame #20: 0x000000000041d8ae divine`_start + 46
[ 0:40]   thread #3, stop reason = signal 0
[ 0:40]     frame #0: 0x00007f189d8f2e5b libpthread.so.0`__pthread_cond_timedwait + 603
[ 0:40]     frame #1: 0x00007f1895339967 libc++.so.2`std::__2::condition_variable::__do_timed_wait(std::__2::unique_lock<std::__2::mutex>&, std::__2::chrono::time_point<std::__2::chrono::system_clock, std::__2::chrono::duration<long long, std::__2::ratio<1l, 1000000000l> > >) [inlined] std::__2::__libcpp_condvar_timedwait(__ts=<unavailable>, __m=<unavailable>, __cv=<unavailable>) at __threading_support:284
[ 0:40]     frame #2: 0x00007f1895339962 libc++.so.2`std::__2::condition_variable::__do_timed_wait(this=<unavailable>, lk=<unavailable>, tp=<unavailable>) at condition_variable.cpp:74
[ 0:40]     frame #3: 0x00007f189dcee135 libdivine-ui.so`std::__2::cv_status std::__2::condition_variable::wait_until<std::__2::chrono::steady_clock, std::__2::chrono::duration<long long, std::__2::ratio<1l, 1000000000l> > >(std::__2::unique_lock<std::__2::mutex>&, std::__2::chrono::time_point<std::__2::chrono::steady_clock, std::__2::chrono::duration<long long, std::__2::ratio<1l, 1000000000l> > > const&) [inlined] std::__2::cv_status std::__2::condition_variable::wait_for<long long, std::__2::ratio<1l, 1000000000l> >(this=0x000000000a247960, __lk=0x00007f1887ffe9b0) at __mutex_base:0
[ 0:40]     frame #4: 0x00007f189dcee0dd libdivine-ui.so`std::__2::cv_status std::__2::condition_variable::wait_until<std::__2::chrono::steady_clock, std::__2::chrono::duration<long long, std::__2::ratio<1l, 1000000000l> > >(this=0x000000000a247960, __lk=0x00007f1887ffe9b0, __t=0x00007f1887ffea00) at __mutex_base:384
[ 0:40]     frame #5: 0x00007f189dcee058 libdivine-ui.so`std::__2::future_status std::__2::__assoc_sub_state::wait_until<std::__2::chrono::steady_clock, std::__2::chrono::duration<long long, std::__2::ratio<1l, 1000000000l> > >(this=0x000000000a247920, __abs_time=0x00007f1887ffea00) const at future:599
[ 0:40]     frame #6: 0x00007f189dd1c380 libdivine-ui.so`divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::wait() [inlined] std::__2::future_status std::__2::future<void>::wait_until<std::__2::chrono::steady_clock, std::__2::chrono::duration<long long, std::__2::ratio<1l, 1000000000l> > >(__abs_time=<unavailable>) const at future:1346
[ 0:40]     frame #7: 0x00007f189dd1c378 libdivine-ui.so`divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::wait() at brick-shmem:658
[ 0:40]     frame #8: 0x00007f189dd1c354 libdivine-ui.so`divine::ss::Search<divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> >, divine::ss::GenericListen<divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto, auto, auto, bool), divine::mc::Safety<divine::ss::PassiveListen<divine::ss::(anonymous namespace)::$_5, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0, divine::ss::(anonymous namespace)::$_0>, divine::mc::Builder<divine::smt::solver::Simple<divine::smt::solver::Z3> > >::make_search()::'lambda'(auto), divine::ss::(anonymous namespace)::$_1, divine::ss::(anonymous namespace)::$_1> >::wait(this=0x0000000009e81790) at search.hpp:234
[ 0:40]     frame #9: 0x00007f189dd8a6c8 libdivine-ui.so`std::__2::__async_assoc_state<void, std::__2::__async_func<divine::mc::Job::wait()::'lambda'()> >::__execute() [inlined] divine::mc::Job::wait(this=<unavailable>)::'lambda'()::operator()() const at job.hpp:50
[ 0:40]     frame #10: 0x00007f189dd8a6bb libdivine-ui.so`std::__2::__async_assoc_state<void, std::__2::__async_func<divine::mc::Job::wait()::'lambda'()> >::__execute() [inlined] decltype(__f=<unavailable>)::'lambda'()>(fp)()) std::__2::__invoke<divine::mc::Job::wait()::'lambda'()>(divine::mc::Job::wait()::'lambda'()&&) at type_traits:4301
[ 0:40]     frame #11: 0x00007f189dd8a6bb libdivine-ui.so`std::__2::__async_assoc_state<void, std::__2::__async_func<divine::mc::Job::wait()::'lambda'()> >::__execute() [inlined] void std::__2::__async_func<divine::mc::Job::wait()::'lambda'()>::__execute<>(this=<unavailable>) at future:2324
[ 0:40]     frame #12: 0x00007f189dd8a6bb libdivine-ui.so`std::__2::__async_assoc_state<void, std::__2::__async_func<divine::mc::Job::wait()::'lambda'()> >::__execute() [inlined] std::__2::__async_func<divine::mc::Job::wait()::'lambda'()>::operator(this=<unavailable>)() at future:2317
[ 0:40]     frame #13: 0x00007f189dd8a6bb libdivine-ui.so`std::__2::__async_assoc_state<void, std::__2::__async_func<divine::mc::Job::wait()::'lambda'()> >::__execute(this=0x0000000009e87210) at future:1035
[ 0:40]     frame #14: 0x00007f189dd8a768 libdivine-ui.so`void* std::__2::__thread_proxy<std::__2::tuple<std::__2::unique_ptr<std::__2::__thread_struct, std::__2::default_delete<std::__2::__thread_struct> >, void (std::__2::__async_assoc_state<void, std::__2::__async_func<divine::mc::Job::wait()::'lambda'()> >::*)(), std::__2::__async_assoc_state<void, std::__2::__async_func<divine::mc::Job::wait()::'lambda'()> >*> >(void*) [inlined] decltype(__f=<unavailable>, __a0=<unavailable>)::'lambda'()> >*>(fp0)).*fp()) std::__2::__invoke<void (std::__2::__async_assoc_state<void, std::__2::__async_func<divine::mc::Job::wait()::'lambda'()> >::*)(), std::__2::__async_assoc_state<void, std::__2::__async_func<divine::mc::Job::wait()::'lambda'()> >*, void>(void (std::__2::__async_assoc_state<void, std::__2::__async_func<divine::mc::Job::wait()::'lambda'()> >::*&&)(), std::__2::__async_assoc_state<void, std::__2::__async_func<divine::mc::Job::wait()::'lambda'()> >*&&) at type_traits:4242
[ 0:40]     frame #15: 0x00007f189dd8a74e libdivine-ui.so`void* std::__2::__thread_proxy<std::__2::tuple<std::__2::unique_ptr<std::__2::__thread_struct, std::__2::default_delete<std::__2::__thread_struct> >, void (std::__2::__async_assoc_state<void, std::__2::__async_func<divine::mc::Job::wait()::'lambda'()> >::*)(), std::__2::__async_assoc_state<void, std::__2::__async_func<divine::mc::Job::wait()::'lambda'()> >*> >(void*) [inlined] void std::__2::__thread_execute<std::__2::unique_ptr<std::__2::__thread_struct, std::__2::default_delete<std::__2::__thread_struct> >, void (std::__2::__async_assoc_state<void, std::__2::__async_func<divine::mc::Job::wait()::'lambda'()> >::*)(), std::__2::__async_assoc_state<void, std::__2::__async_func<divine::mc::Job::wait()::'lambda'()> >*, 2ul>(std::__2::tuple<std::__2::unique_ptr<std::__2::__thread_struct, std::__2::default_delete<std::__2::__thread_struct> >, void (std::__2::__async_assoc_state<void, std::__2::__async_func<divine::mc::Job::wait()::'lambda'()> >::*)(), std::__2::__async_assoc_state<void, std::__2::__async_func<divine::mc::Job::wait()::'lambda'()> >*>&, std::__2::__tuple_indices<2ul>) at thread:336
[ 0:40]     frame #16: 0x00007f189dd8a74e libdivine-ui.so`void* std::__2::__thread_proxy<std::__2::tuple<std::__2::unique_ptr<std::__2::__thread_struct, std::__2::default_delete<std::__2::__thread_struct> >, void (std::__2::__async_assoc_state<void, std::__2::__async_func<divine::mc::Job::wait()::'lambda'()> >::*)(), std::__2::__async_assoc_state<void, std::__2::__async_func<divine::mc::Job::wait()::'lambda'()> >*> >(__vp=0x000000000c49c740) at thread:346
[ 0:40]     frame #17: 0x00007f189d8eca9d libpthread.so.0`start_thread + 253
[ 0:40]     frame #18: 0x00007f189505ab23 libc.so.6`__GI___clone + 67