./locksmith /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c


--------------------------------------------------------------------------------


gcc -D_GNUCC -E -DCIL=1 /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c -o /tmp/cil-ksNEiOzv.i
./cil/obj/x86_LINUX/cilly.asm.exe --out /tmp/cil-QNj9c1e0.cil.c /tmp/cil-ksNEiOzv.i

************************* STARTING *************************

/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:724: Warning: assigning pointer to non-pointer: (void)*^{arg:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:718}
 ->
 int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:741: Warning: assigning number to pointer
functions declared and used but not defined:
  difftime
  fprintf
  prctl
  printf
  pthread_cond_broadcast
  pthread_cond_init
  pthread_cond_signal
  pthread_cond_wait
  pthread_detach
  pthread_kill
  pthread_self
  puts
  sigaction
  sigemptyset
  sleep
  snprintf
  time
Warning: Possible data race: &threads_keepalive:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:279 is not protected!
 references:
  dereference of &threads_keepalive:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:279 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:305
    &threads_keepalive:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:279
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736

  dereference of &threads_keepalive:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:279 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:396
    &threads_keepalive:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:279
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746

  dereference of &threads_keepalive:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:279 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:521
    &threads_keepalive:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:279
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of &threads_keepalive:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:279 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:523
    &threads_keepalive:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:279
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470


Warning: Possible data race: alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 is not protected!
 references:
  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:315
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:316
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:320
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:324
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:325
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:328
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:331
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:332
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:339
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:345 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:295
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 at thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
                                                                                   => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:731
                                                                                   => thpool:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
                                                                                   => thpool_add_work.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:741
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:345 at thpool_add_work /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:741
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:741

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:363 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:368
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:295
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 at thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
                                                                                   => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:731
                                                                                   => thpool:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
                                                                                   => thpool_wait.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:744
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:363 at thpool_wait /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:744
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:744

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:363 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:370
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:295
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 at thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
                                                                                   => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:731
                                                                                   => thpool:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
                                                                                   => thpool_wait.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:744
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:363 at thpool_wait /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:744
  locks acquired:
    concrete thpool_p->thcount_lock::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
    thpool->thcount_lock:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:744

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:363 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:371
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:295
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 at thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
                                                                                   => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:731
                                                                                   => thpool:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
                                                                                   => thpool_wait.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:744
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:363 at thpool_wait /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:744
  locks acquired:
    concrete thpool_p->thcount_lock::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
    thpool->thcount_lock:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:744

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:363 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:375
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:295
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 at thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
                                                                                   => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:731
                                                                                   => thpool:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
                                                                                   => thpool_wait.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:744
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:363 at thpool_wait /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:744
  locks acquired:
    concrete thpool_p->thcount_lock::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
    thpool->thcount_lock:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:744

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:363 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:378
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:295
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 at thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
                                                                                   => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:731
                                                                                   => thpool:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
                                                                                   => thpool_wait.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:744
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:363 at thpool_wait /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:744
  locks acquired:
    concrete thpool_p->thcount_lock::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
    thpool->thcount_lock:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:744

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:382 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:395
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:295
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 at thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
                                                                                   => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:731
                                                                                   => thpool:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
                                                                                   => thpool_destroy.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:382 at thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:382 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:402
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:295
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 at thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
                                                                                   => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:731
                                                                                   => thpool:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
                                                                                   => thpool_destroy.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:382 at thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:382 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:408
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:295
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 at thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
                                                                                   => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:731
                                                                                   => thpool:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
                                                                                   => thpool_destroy.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:382 at thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:382 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:412
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:295
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 at thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
                                                                                   => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:731
                                                                                   => thpool:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
                                                                                   => thpool_destroy.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:382 at thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:382 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:413
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:295
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 at thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
                                                                                   => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:731
                                                                                   => thpool:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
                                                                                   => thpool_destroy.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:382 at thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:382 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:295
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 at thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
                                                                                   => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:731
                                                                                   => thpool:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
                                                                                   => thpool_destroy.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:382 at thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:382 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:419
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:295
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 at thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
                                                                                   => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:731
                                                                                   => thpool:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
                                                                                   => thpool_destroy.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:382 at thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:382 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:422
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:295
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 at thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
                                                                                   => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:731
                                                                                   => thpool:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
                                                                                   => thpool_destroy.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:382 at thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:382 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:423
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:295
                                                                                   => thpool_init.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 at thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
                                                                                   => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:731
                                                                                   => thpool:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
                                                                                   => thpool_destroy.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:382 at thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:518
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
                                                                                   => *(*thread_p).thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281
                                                                                   => *thread_p.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:282 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:519
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
                                                                                   => *(*thread_p).thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281
                                                                                   => *thread_p.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:282 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492
  locks acquired:
    concrete thpool_p->thcount_lock::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
    thpool->thcount_lock:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:520
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
                                                                                   => *(*thread_p).thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281
                                                                                   => *thread_p.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:282 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492
  locks acquired:
    concrete thpool_p->thcount_lock::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
    thpool->thcount_lock:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:522
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
                                                                                   => *(*thread_p).thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281
                                                                                   => *thread_p.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:282 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:524
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
                                                                                   => *(*thread_p).thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281
                                                                                   => *thread_p.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:282 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:525
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
                                                                                   => *(*thread_p).thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281
                                                                                   => *thread_p.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:282 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492
  locks acquired:
    concrete thpool_p->thcount_lock::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
    thpool->thcount_lock:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:526
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
                                                                                   => *(*thread_p).thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281
                                                                                   => *thread_p.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:282 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492
  locks acquired:
    concrete thpool_p->thcount_lock::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
    thpool->thcount_lock:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:527
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
                                                                                   => *(*thread_p).thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281
                                                                                   => *thread_p.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:282 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:535
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
                                                                                   => *(*thread_p).thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281
                                                                                   => *thread_p.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:282 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:536
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
                                                                                   => *(*thread_p).thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281
                                                                                   => *thread_p.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:282 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492
  locks acquired:
    concrete thpool_p->thcount_lock::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
    thpool->thcount_lock:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:537
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
                                                                                   => *(*thread_p).thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281
                                                                                   => *thread_p.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:282 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492
  locks acquired:
    concrete thpool_p->thcount_lock::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
    thpool->thcount_lock:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:538
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
                                                                                   => *(*thread_p).thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281
                                                                                   => *thread_p.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:282 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492
  locks acquired:
    concrete thpool_p->thcount_lock::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
    thpool->thcount_lock:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:540
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
                                                                                   => *(*thread_p).thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281
                                                                                   => *thread_p.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:282 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492
  locks acquired:
    concrete thpool_p->thcount_lock::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
    thpool->thcount_lock:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:543
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
                                                                                   => *(*thread_p).thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281
                                                                                   => *thread_p.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:282 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:544
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
                                                                                   => *(*thread_p).thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281
                                                                                   => *thread_p.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:282 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492
  locks acquired:
    concrete thpool_p->thcount_lock::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
    thpool->thcount_lock:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:545
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:309 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:298
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:310
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thread_init.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
                                                                                   => *(*thread_p).thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281
                                                                                   => *thread_p.thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:282 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thpool_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492
  locks acquired:
    concrete thpool_p->thcount_lock::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
    thpool->thcount_lock:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470


Warning: Possible data race: alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:351 is not protected!
 references:
  dereference of newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:347 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:357
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:351 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:348
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:352
                                                                                   => newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:347
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:741

  dereference of newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:347 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:358
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:351 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:348
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:352
                                                                                   => newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:347
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:741

  dereference of job_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:497 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:530
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:351 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:348
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:352
                                                                                   => newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:347
                                                                                   => jobqueue_push.newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
                                                                                   => jobqueue_push.newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:287 at jobqueue_push /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
                                                                                   => newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:592
                                                                                   => *jobqueue_p.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:287
                                                                                   => jobqueue_push.jobqueue_p->front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:273 at jobqueue_push /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
                                                                                   => thpool->jobqueue.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730 at thpool_add_work /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:741
                                                                                   => jobqueue_destroy.jobqueue_p->front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:277 at thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
                                                                                   => jobqueue_p->front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:289 at jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416
                                                                                   => *jobqueue_p.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:286 at jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643
                                                                                   => *jobqueue_p.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:288 at jobqueue_pull /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:582
                                                                                   => job_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:616
                                                                                   => jobqueue_pull.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:614
                                                                                   => jobqueue_pull.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:288
                                                                                   => jobqueue_pull.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:527 at jobqueue_pull /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:527
                                                                                   => tmp___1:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:498
                                                                                   => job_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:497
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of job_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:497 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:531
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:351 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:348
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:352
                                                                                   => newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:347
                                                                                   => jobqueue_push.newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
                                                                                   => jobqueue_push.newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:287 at jobqueue_push /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
                                                                                   => newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:592
                                                                                   => *jobqueue_p.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:287
                                                                                   => jobqueue_push.jobqueue_p->front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:273 at jobqueue_push /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
                                                                                   => thpool->jobqueue.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730 at thpool_add_work /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:741
                                                                                   => jobqueue_destroy.jobqueue_p->front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:277 at thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
                                                                                   => jobqueue_p->front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:289 at jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416
                                                                                   => *jobqueue_p.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:286 at jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643
                                                                                   => *jobqueue_p.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:288 at jobqueue_pull /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:582
                                                                                   => job_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:616
                                                                                   => jobqueue_pull.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:614
                                                                                   => jobqueue_pull.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:288
                                                                                   => jobqueue_pull.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:527 at jobqueue_pull /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:527
                                                                                   => tmp___1:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:498
                                                                                   => job_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:497
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of job_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:497 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:533
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:351 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:348
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:352
                                                                                   => newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:347
                                                                                   => jobqueue_push.newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
                                                                                   => jobqueue_push.newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:287 at jobqueue_push /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
                                                                                   => newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:592
                                                                                   => *jobqueue_p.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:287
                                                                                   => jobqueue_push.jobqueue_p->front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:273 at jobqueue_push /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
                                                                                   => thpool->jobqueue.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730 at thpool_add_work /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:741
                                                                                   => jobqueue_destroy.jobqueue_p->front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:277 at thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
                                                                                   => jobqueue_p->front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:289 at jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416
                                                                                   => *jobqueue_p.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:286 at jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643
                                                                                   => *jobqueue_p.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:288 at jobqueue_pull /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:582
                                                                                   => job_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:616
                                                                                   => jobqueue_pull.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:614
                                                                                   => jobqueue_pull.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:288
                                                                                   => jobqueue_pull.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:527 at jobqueue_pull /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:527
                                                                                   => tmp___1:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:498
                                                                                   => job_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:497
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:578 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:583
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:351 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:348
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:352
                                                                                   => newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:347
                                                                                   => jobqueue_push.newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
                                                                                   => jobqueue_push.newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:287 at jobqueue_push /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
                                                                                   => newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:592
                                                                                   => *jobqueue_p.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:287
                                                                                   => jobqueue_push.jobqueue_p->front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:273 at jobqueue_push /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
                                                                                   => thpool->jobqueue.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730 at thpool_add_work /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:741
                                                                                   => jobqueue_destroy.jobqueue_p->front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:277 at thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
                                                                                   => jobqueue_p->front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:289 at jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416
                                                                                   => *jobqueue_p.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:286 at jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643
                                                                                   => *jobqueue_p.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:288 at jobqueue_pull /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:582
                                                                                   => job_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:616
                                                                                   => jobqueue_pull.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:614
                                                                                   => jobqueue_pull.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:288
                                                                                   => jobqueue_pull.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:582 at jobqueue_pull /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:582
                                                                                   => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:578
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643

  dereference of newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:592 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:598
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:351 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:348
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:352
                                                                                   => newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:347
                                                                                   => jobqueue_push.newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
                                                                                   => jobqueue_push.newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:287 at jobqueue_push /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
                                                                                   => newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:592
  locks acquired:
    concrete jobqueue_p->rwmutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
    thpool->jobqueue.rwmutex:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:741 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359

  dereference of *jobqueue_p.rear:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:287 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:605
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:351 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:348
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:352
                                                                                   => newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:347
                                                                                   => jobqueue_push.newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
                                                                                   => jobqueue_push.newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:287 at jobqueue_push /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
                                                                                   => newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:592
                                                                                   => *jobqueue_p.rear:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:287
  locks acquired:
    concrete jobqueue_p->rwmutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
    thpool->jobqueue.rwmutex:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:741 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359

  dereference of job_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:616 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:630
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:351 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:348
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:352
                                                                                   => newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:347
                                                                                   => jobqueue_push.newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
                                                                                   => jobqueue_push.newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:287 at jobqueue_push /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
                                                                                   => newjob:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:592
                                                                                   => *jobqueue_p.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:287
                                                                                   => jobqueue_push.jobqueue_p->front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:273 at jobqueue_push /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359
                                                                                   => thpool->jobqueue.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730 at thpool_add_work /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:741
                                                                                   => jobqueue_destroy.jobqueue_p->front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:277 at thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
                                                                                   => jobqueue_p->front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:289 at jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416
                                                                                   => *jobqueue_p.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:286 at jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643
                                                                                   => *jobqueue_p.front:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:288 at jobqueue_pull /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:582
                                                                                   => job_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:616
  locks acquired:
    concrete jobqueue_p->rwmutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
    thpool->jobqueue.rwmutex:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:582
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:582
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:527


Warning: Possible data race: alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:462 is not protected!
 references:
  dereference of *thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:468
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:462 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:459
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:463
                                                                                   => *thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336

  dereference of *thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:469
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:462 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:459
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:463
                                                                                   => *thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336

  dereference of *thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:462 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:459
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:463
                                                                                   => *thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336

  dereference of *thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:472
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:462 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:459
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:463
                                                                                   => *thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336

  dereference of thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:488 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:507
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:462 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:459
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:463
                                                                                   => *thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
                                                                                   => thread_do.thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thread_do.thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:282 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:488
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:488 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:510
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:462 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:459
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:463
                                                                                   => *thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
                                                                                   => thread_do.thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thread_do.thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:282 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:488
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470

  dereference of thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:549 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:554
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:462 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:459
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:463
                                                                                   => *thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:457
                                                                                   => *thread_init.thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281
                                                                                   => *thread_init.thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => **thpool_p.threads:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297
                                                                                   => *thpool->threads:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730 at thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736
                                                                                   => **thpool_p.threads:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:277 at thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746
                                                                                   => thread_destroy.thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:419
                                                                                   => thread_destroy.thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:284 at thread_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:419
                                                                                   => thread_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:549
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:419


Warning: Possible data race: alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:566 is not protected!
 references:
  dereference of *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:289 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:644
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:566 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:560
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:567
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:285
                                                                                   => jobqueue_destroy.jobqueue_p->has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:289 at jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416

  dereference of bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:648 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:661
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:566 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:560
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:567
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:285
                                                                                   => bsem_init.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:572
                                                                                   => bsem_init.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:290 at bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:572
                                                                                   => bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:648
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:572
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672

  dereference of bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:648 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:662
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:566 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:560
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:567
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:285
                                                                                   => bsem_init.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:572
                                                                                   => bsem_init.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:290 at bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:572
                                                                                   => bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:648
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:572
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672

  dereference of bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:648 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:663
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:566 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:560
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:567
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:285
                                                                                   => bsem_init.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:572
                                                                                   => bsem_init.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:290 at bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:572
                                                                                   => bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:648
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:572
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672

  dereference of bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:676 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:681
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:566 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:560
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:567
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:285
                                                                                   => jobqueue_destroy.jobqueue_p->has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
                                                                                   => thpool_p->jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => *thpool_p.jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:288 at jobqueue_pull /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:527
                                                                                   => bsem_post.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632
                                                                                   => bsem_post.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:292 at bsem_post /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632
                                                                                   => bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:676
  locks acquired:
    concrete jobqueue_p->rwmutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
    thpool->jobqueue.rwmutex:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:741 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:609
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:582 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:582 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:527 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632

  dereference of bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:676 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:682
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:566 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:560
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:567
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:285
                                                                                   => jobqueue_destroy.jobqueue_p->has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
                                                                                   => thpool_p->jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => *thpool_p.jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:288 at jobqueue_pull /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:527
                                                                                   => bsem_post.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632
                                                                                   => bsem_post.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:292 at bsem_post /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632
                                                                                   => bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:676
  locks acquired:
    concrete jobqueue_p->rwmutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
    non linear concrete bsem_p->mutex::-1 -> thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:572
    thpool->jobqueue.has_jobs->mutex:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
    thpool->jobqueue.rwmutex:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:741 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:609
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:582 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:582 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:527 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632

  dereference of bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:676 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:683
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:566 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:560
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:567
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:285
                                                                                   => jobqueue_destroy.jobqueue_p->has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
                                                                                   => thpool_p->jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => *thpool_p.jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:288 at jobqueue_pull /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:527
                                                                                   => bsem_post.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632
                                                                                   => bsem_post.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:292 at bsem_post /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632
                                                                                   => bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:676
  locks acquired:
    concrete jobqueue_p->rwmutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
    non linear concrete bsem_p->mutex::-1 -> thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:572
    thpool->jobqueue.has_jobs->mutex:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
    thpool->jobqueue.rwmutex:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:741 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:609
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:582 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:582 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:527 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632

  dereference of bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:676 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:684
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:566 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:560
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:567
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:285
                                                                                   => jobqueue_destroy.jobqueue_p->has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
                                                                                   => thpool_p->jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => *thpool_p.jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:288 at jobqueue_pull /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:527
                                                                                   => bsem_post.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632
                                                                                   => bsem_post.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:292 at bsem_post /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632
                                                                                   => bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:676
  locks acquired:
    concrete jobqueue_p->rwmutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
    non linear concrete bsem_p->mutex::-1 -> thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:572
    thpool->jobqueue.has_jobs->mutex:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
    thpool->jobqueue.rwmutex:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:741 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:359 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:609
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:582 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:582 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:527 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:632

  dereference of bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:688 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:693
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:566 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:560
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:567
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:285
                                                                                   => jobqueue_destroy.jobqueue_p->has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:289 at jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327
                                                                                   => *thpool_p.jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:277 at jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416
                                                                                   => bsem_post_all.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:413
                                                                                   => bsem_post_all.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:293 at bsem_post_all /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:413
                                                                                   => bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:688
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:408
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:413

  dereference of bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:688 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:694
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:566 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:560
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:567
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:285
                                                                                   => jobqueue_destroy.jobqueue_p->has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:289 at jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327
                                                                                   => *thpool_p.jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:277 at jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416
                                                                                   => bsem_post_all.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:413
                                                                                   => bsem_post_all.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:293 at bsem_post_all /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:413
                                                                                   => bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:688
  locks acquired:
    non linear concrete bsem_p->mutex::-1 -> thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:572
    thpool->jobqueue.has_jobs->mutex:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:408
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:413

  dereference of bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:688 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:695
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:566 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:560
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:567
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:285
                                                                                   => jobqueue_destroy.jobqueue_p->has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:289 at jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327
                                                                                   => *thpool_p.jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:277 at jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416
                                                                                   => bsem_post_all.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:413
                                                                                   => bsem_post_all.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:293 at bsem_post_all /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:413
                                                                                   => bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:688
  locks acquired:
    non linear concrete bsem_p->mutex::-1 -> thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:572
    thpool->jobqueue.has_jobs->mutex:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:408
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:413

  dereference of bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:688 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:696
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:566 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:560
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:567
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:285
                                                                                   => jobqueue_destroy.jobqueue_p->has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:289 at jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327
                                                                                   => *thpool_p.jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:277 at jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416
                                                                                   => bsem_post_all.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:413
                                                                                   => bsem_post_all.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:293 at bsem_post_all /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:413
                                                                                   => bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:688
  locks acquired:
    non linear concrete bsem_p->mutex::-1 -> thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:572
    thpool->jobqueue.has_jobs->mutex:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:408
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:413

  dereference of bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:700 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:705
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:566 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:560
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:567
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:285
                                                                                   => jobqueue_destroy.jobqueue_p->has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
                                                                                   => thpool_p->jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => *thpool_p.jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => bsem_wait.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:522
                                                                                   => bsem_wait.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:294 at bsem_wait /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:522
                                                                                   => bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:700
  locks acquired:
    <empty>
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:522

  dereference of bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:700 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:706
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:566 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:560
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:567
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:285
                                                                                   => jobqueue_destroy.jobqueue_p->has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
                                                                                   => thpool_p->jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => *thpool_p.jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => bsem_wait.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:522
                                                                                   => bsem_wait.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:294 at bsem_wait /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:522
                                                                                   => bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:700
  locks acquired:
    non linear concrete bsem_p->mutex::-1 -> thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:572
    thpool->jobqueue.has_jobs->mutex:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:522

  dereference of bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:700 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:707
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:566 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:560
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:567
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:285
                                                                                   => jobqueue_destroy.jobqueue_p->has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
                                                                                   => thpool_p->jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => *thpool_p.jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => bsem_wait.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:522
                                                                                   => bsem_wait.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:294 at bsem_wait /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:522
                                                                                   => bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:700
  locks acquired:
    non linear concrete bsem_p->mutex::-1 -> thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:572
    thpool->jobqueue.has_jobs->mutex:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:522

  dereference of bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:700 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:709
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:566 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:560
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:567
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:285
                                                                                   => jobqueue_destroy.jobqueue_p->has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
                                                                                   => thpool_p->jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => *thpool_p.jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => bsem_wait.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:522
                                                                                   => bsem_wait.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:294 at bsem_wait /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:522
                                                                                   => bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:700
  locks acquired:
    non linear concrete bsem_p->mutex::-1 -> thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:572
    thpool->jobqueue.has_jobs->mutex:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:522

  dereference of bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:700 at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:710
    alloc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:566 => tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:560
                                                                                   => cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:567
                                                                                   => *jobqueue_p.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:285
                                                                                   => jobqueue_destroy.jobqueue_p->has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:297 at jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317
                                                                                   => thpool_p->jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:281 at thread_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336
                                                                                   => *thpool_p.jobqueue.has_jobs:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:492 at thread_do /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470
                                                                                   => bsem_wait.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:522
                                                                                   => bsem_wait.bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:294 at bsem_wait /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:522
                                                                                   => bsem_p:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:700
  locks acquired:
    non linear concrete bsem_p->mutex::-1 -> thpool_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:746 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:416 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_destroy /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:327 -> jobqueue_clear /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:643 -> bsem_reset /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:587 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:672
    non linear concrete bsem_p->mutex::-1 -> thpool_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> jobqueue_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:317 -> bsem_init /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:572
    thpool->jobqueue.has_jobs->mutex:/mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:730
  in: main at /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:728 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:736 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:336 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:470 -> /mnt/goblint-svcomp/goblint-bench/bench/concrat/C-Thread-Pool/main.c:522


*************************** DONE ***************************

LockSmith run for: 0.124922 seconds

gcc -D_GNUCC -E /tmp/cil-QNj9c1e0.cil.c -o /tmp/cil-z4lqweDF.cil.i
