./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i


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


Deagle version 2.1 64-bit x86_64 linux
which contains:
CBMC version 5.67.0 (SVCOMP2023_221122-2-g2121ef1a2) 64-bit x86_64 linux
Parsing /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i
Converting
Type-checking qrcu-2
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-pthread_mutex_init> line 27: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_init"
old definition in module qrcu-2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i line 515
signed int (pthread_mutex_t *, const pthread_mutexattr_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_init> line 27
signed int (pthread_mutex_t *pthread_mutex_init$$mutex, const pthread_mutexattr_t *mutexattr)
file <builtin-library-pthread_create> line 20: warning: pointer parameter types differ between declaration and definition "pthread_create"
old definition in module qrcu-2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i line 409
signed int (pthread_t *, const pthread_attr_t *, void * (*)(void *), void *)
new definition in module <built-in-library> file <builtin-library-pthread_create> line 20
signed int (pthread_t *thread, const pthread_attr_t *attr, void * (*start_routine)(void *), void *arg)
file <builtin-library-pthread_mutex_destroy> line 17: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_destroy"
old definition in module qrcu-2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i line 518
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_destroy> line 17
signed int (pthread_mutex_t *pthread_mutex_destroy$$mutex)
file <builtin-library-pthread_mutex_lock> line 17: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_lock"
old definition in module qrcu-2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i line 522
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_lock> line 17
signed int (pthread_mutex_t *pthread_mutex_lock$$mutex)
file <builtin-library-pthread_mutex_unlock> line 17: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_unlock"
old definition in module qrcu-2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i line 527
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_unlock> line 17
signed int (pthread_mutex_t *pthread_mutex_unlock$$mutex)
Removal of function pointers and virtual functions
file <builtin-library-__spawned_thread> line 34 function __spawned_thread: replacing function pointer by 3 possible targets
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___0,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:727:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:731:7)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___0,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:746:5)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:750:7)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:763:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:763:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___1, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:766:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___2, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:767:19)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:710:3)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:717:3)
[Warning][Deadcode] Function "__bswap_32" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:72:1)
[Warning][Deadcode] Function "__bswap_64" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:77:1)
[Warning][Deadcode] Function "__uint16_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:82:1)
[Warning][Deadcode] Function "__uint32_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:87:1)
[Warning][Deadcode] Function "__uint64_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:92:1)
[Warning][Race] Memory location readerprogress1@qrcu-2.i:691:5 (race with conf. 110):
  read with {thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:706:3)
  read with {thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:711:5)
  write with {thread:([qrcu_reader1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:785:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:737:3)
  write with {thread:([qrcu_reader1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:785:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:738:3)
[Warning][Race] Memory location readerprogress2@qrcu-2.i:691:24 (race with conf. 110):
  read with {thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:707:3)
  read with {thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:718:5)
  write with {thread:([qrcu_reader2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:786:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:756:3)
  write with {thread:([qrcu_reader2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:786:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:757:3)
[Warning][Race] Memory location ctr2@qrcu-2.i:690:13 (race with conf. 110):
  read with {thread:([qrcu_reader1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:785:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:698:3)
  read with {thread:([qrcu_reader2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:786:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:698:3)
  read with {thread:([qrcu_reader1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:785:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:699:3)
  read with {thread:([qrcu_reader2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:786:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:699:3)
  read with {thread:([qrcu_reader1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:785:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:703:10)
  read with {thread:([qrcu_reader2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:786:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:703:10)
  read with {thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:766:46)
  read with {thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:766:73)
  read with {thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:767:62)
  read with {thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:767:89)
  read with {lock:mutex, thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:771:21)
  read with {lock:mutex, thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:772:29)
  read with {lock:mutex, thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:774:12)
  write with {thread:([qrcu_reader1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:785:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:699:3)
  write with {thread:([qrcu_reader2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:786:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:699:3)
  write with {thread:([qrcu_reader1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:785:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:703:10)
  write with {thread:([qrcu_reader2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:786:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:703:10)
  write with {lock:mutex, thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:771:21)
  write with {lock:mutex, thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:772:29)
[Warning][Race] Memory location ctr1@qrcu-2.i:690:5 (race with conf. 110):
  read with {thread:([qrcu_reader1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:785:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:694:3)
  read with {thread:([qrcu_reader2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:786:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:694:3)
  read with {thread:([qrcu_reader1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:785:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:695:3)
  read with {thread:([qrcu_reader2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:786:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:695:3)
  read with {thread:([qrcu_reader1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:785:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:702:21)
  read with {thread:([qrcu_reader2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:786:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:702:21)
  read with {thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:766:34)
  read with {thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:766:85)
  read with {thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:767:50)
  read with {thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:767:101)
  read with {lock:mutex, thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:771:38)
  read with {lock:mutex, thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:772:12)
  read with {lock:mutex, thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:773:21)
  write with {thread:([qrcu_reader1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:785:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:695:3)
  write with {thread:([qrcu_reader2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:786:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:695:3)
  write with {thread:([qrcu_reader1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:785:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:702:21)
  write with {thread:([qrcu_reader2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:786:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:702:21)
  write with {lock:mutex, thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:771:38)
  write with {lock:mutex, thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:772:12)
[Warning][Race] Memory location idx@qrcu-2.i:689:5 (race with conf. 110):
  read with {thread:([qrcu_reader1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:785:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:726:5)
  read with {thread:([qrcu_reader2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:786:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:745:5)
  read with {lock:mutex, thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:771:5)
  read with {lock:mutex, thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:773:5)
  write with {lock:mutex, thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:771:29)
  write with {lock:mutex, thread:([qrcu_updater@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:787:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i:772:20)

Summary for all memory locations:
	safe:            0
	vulnerable:      0
	unsafe:          5
	-------------------
	total:           5
__VERIFIER_atomic_use1::myidx's upper bound is 0
Use SV-COMP unwinding strategy: 2
Deagle's solver is set!!!!!!
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
Unwinding loop qrcu_reader1.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i line 725 function qrcu_reader1 thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
Not unwinding loop qrcu_reader1.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i line 725 function qrcu_reader1 thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
Unwinding loop qrcu_reader2.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i line 744 function qrcu_reader2 thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
Not unwinding loop qrcu_reader2.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i line 744 function qrcu_reader2 thread 2
replacing self-loop at file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i line 773 function qrcu_updater by assume(!TRUE)
replacing self-loop at file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i line 774 function qrcu_updater by assume(!TRUE)
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
Handling datarace, passing the problem to goblint first
getcwd: /mnt/goblint-svcomp/benchexec/tools-pldi/deagle
/mnt/goblint-svcomp/benchexec/tools-pldi/deagle/goblint/goblint /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/qrcu-2.i | tee goblint/goblint_output: 0
Lines where datarace may occur: 694 695 696 698 699 700 702 703 704 706 707 708 711 712 718 719 726 727 728 737 738 739 745 746 747 756 757 758 763 764 766 767 768 771 772 773 774 775 
The number of races before goblint filter: 220
The number of races after goblint filter: 144
Race categories: 28
	696(1) - 766(1) ctr1:
		ctr1#4 ctr1#22
		ctr1#4 ctr1#23
		ctr1#7 ctr1#22
		ctr1#7 ctr1#23
		ctr1#14 ctr1#22
		ctr1#14 ctr1#23
		ctr1#17 ctr1#22
		ctr1#17 ctr1#23
	696(1) - 767(1) ctr1:
		ctr1#4 ctr1#24
		ctr1#4 ctr1#25
		ctr1#7 ctr1#24
		ctr1#7 ctr1#25
		ctr1#14 ctr1#24
		ctr1#14 ctr1#25
		ctr1#17 ctr1#24
		ctr1#17 ctr1#25
	696(1) - 771(1) ctr1:
		ctr1#2 ctr1#27
		ctr1#4 ctr1#26
		ctr1#4 ctr1#27
		ctr1#5 ctr1#27
		ctr1#7 ctr1#26
		ctr1#7 ctr1#27
		ctr1#12 ctr1#27
		ctr1#14 ctr1#26
		ctr1#14 ctr1#27
		ctr1#15 ctr1#27
		ctr1#17 ctr1#26
		ctr1#17 ctr1#27
	696(1) - 772(1) ctr1:
		ctr1#2 ctr1#29
		ctr1#4 ctr1#28
		ctr1#4 ctr1#29
		ctr1#5 ctr1#29
		ctr1#7 ctr1#28
		ctr1#7 ctr1#29
		ctr1#12 ctr1#29
		ctr1#14 ctr1#28
		ctr1#14 ctr1#29
		ctr1#15 ctr1#29
		ctr1#17 ctr1#28
		ctr1#17 ctr1#29
	696(1) - 773(1) ctr1:
		ctr1#4 ctr1#30
		ctr1#7 ctr1#30
		ctr1#14 ctr1#30
		ctr1#17 ctr1#30
	704(1) - 766(1) ctr1:
		ctr1#11 ctr1#22
		ctr1#11 ctr1#23
		ctr1#21 ctr1#22
		ctr1#21 ctr1#23
	704(1) - 767(1) ctr1:
		ctr1#11 ctr1#24
		ctr1#11 ctr1#25
		ctr1#21 ctr1#24
		ctr1#21 ctr1#25
	704(1) - 771(1) ctr1:
		ctr1#8 ctr1#27
		ctr1#11 ctr1#26
		ctr1#11 ctr1#27
		ctr1#18 ctr1#27
		ctr1#21 ctr1#26
		ctr1#21 ctr1#27
	704(1) - 772(1) ctr1:
		ctr1#8 ctr1#29
		ctr1#11 ctr1#28
		ctr1#11 ctr1#29
		ctr1#18 ctr1#29
		ctr1#21 ctr1#28
		ctr1#21 ctr1#29
	704(1) - 773(1) ctr1:
		ctr1#11 ctr1#30
		ctr1#21 ctr1#30
	700(1) - 766(1) ctr2:
		ctr2#4 ctr2#22
		ctr2#4 ctr2#23
		ctr2#7 ctr2#22
		ctr2#7 ctr2#23
		ctr2#14 ctr2#22
		ctr2#14 ctr2#23
		ctr2#17 ctr2#22
		ctr2#17 ctr2#23
	700(1) - 767(1) ctr2:
		ctr2#4 ctr2#24
		ctr2#4 ctr2#25
		ctr2#7 ctr2#24
		ctr2#7 ctr2#25
		ctr2#14 ctr2#24
		ctr2#14 ctr2#25
		ctr2#17 ctr2#24
		ctr2#17 ctr2#25
	700(1) - 771(1) ctr2:
		ctr2#2 ctr2#27
		ctr2#4 ctr2#26
		ctr2#4 ctr2#27
		ctr2#5 ctr2#27
		ctr2#7 ctr2#26
		ctr2#7 ctr2#27
		ctr2#12 ctr2#27
		ctr2#14 ctr2#26
		ctr2#14 ctr2#27
		ctr2#15 ctr2#27
		ctr2#17 ctr2#26
		ctr2#17 ctr2#27
	700(1) - 772(1) ctr2:
		ctr2#2 ctr2#29
		ctr2#4 ctr2#28
		ctr2#4 ctr2#29
		ctr2#5 ctr2#29
		ctr2#7 ctr2#28
		ctr2#7 ctr2#29
		ctr2#12 ctr2#29
		ctr2#14 ctr2#28
		ctr2#14 ctr2#29
		ctr2#15 ctr2#29
		ctr2#17 ctr2#28
		ctr2#17 ctr2#29
	700(1) - 774(1) ctr2:
		ctr2#4 ctr2#30
		ctr2#7 ctr2#30
		ctr2#14 ctr2#30
		ctr2#17 ctr2#30
	704(1) - 766(1) ctr2:
		ctr2#11 ctr2#22
		ctr2#11 ctr2#23
		ctr2#21 ctr2#22
		ctr2#21 ctr2#23
	704(1) - 767(1) ctr2:
		ctr2#11 ctr2#24
		ctr2#11 ctr2#25
		ctr2#21 ctr2#24
		ctr2#21 ctr2#25
	704(1) - 771(1) ctr2:
		ctr2#8 ctr2#27
		ctr2#11 ctr2#26
		ctr2#11 ctr2#27
		ctr2#18 ctr2#27
		ctr2#21 ctr2#26
		ctr2#21 ctr2#27
	704(1) - 772(1) ctr2:
		ctr2#8 ctr2#29
		ctr2#11 ctr2#28
		ctr2#11 ctr2#29
		ctr2#18 ctr2#29
		ctr2#21 ctr2#28
		ctr2#21 ctr2#29
	704(1) - 774(1) ctr2:
		ctr2#11 ctr2#30
		ctr2#21 ctr2#30
	726(1) - 771(1) idx:
		idx#2 idx#7
		idx#3 idx#7
	726(1) - 772(1) idx:
		idx#2 idx#8
		idx#3 idx#8
	745(1) - 771(1) idx:
		idx#4 idx#7
		idx#5 idx#7
	745(1) - 772(1) idx:
		idx#4 idx#8
		idx#5 idx#8
	737(1) - 708(1) readerprogress1:
		readerprogress1#2 readerprogress1#4
	738(1) - 708(1) readerprogress1:
		readerprogress1#3 readerprogress1#4
	756(1) - 708(1) readerprogress2:
		readerprogress2#2 readerprogress2#4
	757(1) - 708(1) readerprogress2:
		readerprogress2#3 readerprogress2#4
Runtime Symex: 0.70107s
Unsupported __VERIFIER_atomic_* function!
