./goblint --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-data-race.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:723:5-725:5 with factor 25
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:739:5-742:5 with factor 8
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:745:5-748:5 with factor 8
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:756:5-760:5 with factor 6
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:763:5-765:5 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:772:5-776:5 with factor 6
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:780:5-781:73 with factor 25
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:783:5-784:49 with factor 25
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:786:5-789:5 with factor 8
unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
Collected factors:
functions: 41
functionCalls: 174
loops: 15
loopBreaks: 0
controlFlowStatements: 454
expressions: 2676
instructions: 439
integralVars: (4,57)
arrayVars: (7,2)
pointerVars: (0,17)

Complexity estimates:
File: 57963
Total: 57963
SV-COMP specification: CHECK( init(main()), LTL(G ! data-race) )
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(pthread_cond_t, TComp(union __anonunion_pthread_cond_t_951761805, __data : TComp(struct __pthread_cond_s, __annonCompField2 : TComp(union __anonunion____missing_field_name_700818794, __wseq : TInt(unsigned long long, ), __wseq32 : TComp(struct __anonstruct___wseq32_817613185, __low : TInt(unsigned int, ), __high : TInt(unsigned int, ), , ), , ), __annonCompField3 : TComp(union __anonunion____missing_field_name_342771831, __g1_start : TInt(unsigned long long, ), __g1_start32 : TComp(struct __anonstruct___g1_start32_817613186, __low : TInt(unsigned int, ), __high : TInt(unsigned int, ), , ), , ), __g_refs : TArray(TInt(unsigned int, ), Some(Const(Int(2,int,2))), ), __g_size : TArray(TInt(unsigned int, ), Some(Const(Int(2,int,2))), ), __g1_orig_size : TInt(unsigned int, ), __wrefs : TInt(unsigned int, ), __g_signals : TArray(TInt(unsigned int, ), Some(Const(Int(2,int,2))), ), , ), __size : TArray(TInt(char, ), Some(Const(Int(48,int,48))), ), __align : TInt(long long, ), , ), ),  __restrict  ), AddrOf(Mem(Lval(Var(b, NoOffset)), Field(sig:TNamed(pthread_cond_t, TComp(union __anonunion_pthread_cond_t_951761805, __data : TComp(struct __pthread_cond_s, __annonCompField2 : TComp(union __anonunion____missing_field_name_700818794, __wseq : TInt(unsigned long long, ), __wseq32 : TComp(struct __anonstruct___wseq32_817613185, __low : TInt(unsigned int, ), __high : TInt(unsigned int, ), , ), , ), __annonCompField3 : TComp(union __anonunion____missing_field_name_342771831, __g1_start : TInt(unsigned long long, ), __g1_start32 : TComp(struct __anonstruct___g1_start32_817613186, __low : TInt(unsigned int, ), __high : TInt(unsigned int, ), , ), , ), __g_refs : TArray(TInt(unsigned int, ), Some(Const(Int(2,int,2))), ), __g_size : TArray(TInt(unsigned int, ), Some(Const(Int(2,int,2))), ), __g1_orig_size : TInt(unsigned int, ), __wrefs : TInt(unsigned int, ), __g_signals : TArray(TInt(unsigned int, ), Some(Const(Int(2,int,2))), ), , ), __size : TArray(TInt(char, ), Some(Const(Int(48,int,48))), ), __align : TInt(long long, ), , ), ), NoOffset)))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:708:5-708:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:717:5-717:14)
[Warning][Deadcode] Function '__bswap_16' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:63:1-67:1)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:68:1-72:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:73:15-77:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:78:1-82:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:83:1-87:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:88:1-92:1)
[Warning][Deadcode] Function 'barrier_destroy' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:710:1-713:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 67
  dead: 9 (9 in uncalled functions)
  total lines: 76
[Warning][Deadcode][CWE-570] condition 'i___2 < 2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:786:9-786:33)
[Warning][Deadcode][CWE-571] condition 'i___2 < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:763:9-763:33)
[Warning][Deadcode][CWE-570] condition 'i < 2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:772:9-772:33)
[Warning][Deadcode][CWE-571] condition 'i___2 < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:763:9-763:33)
[Warning][Deadcode][CWE-570] condition 'i___2 < 2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:763:9-763:33)
[Warning][Deadcode][CWE-571] condition 'i___1 < 1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:783:9-783:37)
[Warning][Deadcode][CWE-571] condition 'i___1 < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:756:9-756:33)
[Warning][Deadcode][CWE-570] condition 'i___1 < 1' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:783:9-783:37)
[Warning][Deadcode][CWE-571] condition 'i___0 < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:745:9-745:33)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:739:9-739:33)
[Warning][Deadcode][CWE-571] condition 'i___1 < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:756:9-756:33)
[Warning][Race] Memory location pre[?] (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:733:16-733:24)
  write with [region:{pre[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & pre[tid]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:738:5-738:19)
  write with [region:{pre[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & pre[tid]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:738:5-738:19)
  read with [region:{pre[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & pre[i___0]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:746:10-746:48)
  read with [region:{pre[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & pre[i___0]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:746:10-746:48)
  read with [region:{pre[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & pre[i___0]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:746:10-746:48)
  read with [region:{pre[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & pre[i___0]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:746:10-746:48)
  read with [region:{pre[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & pre[i___1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:757:10-757:48)
  read with [region:{pre[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & pre[i___1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:757:10-757:48)
  read with [region:{pre[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & pre[i___1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:757:10-757:48)
  read with [region:{pre[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & pre[i___1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:757:10-757:48)
[Warning][Race] Memory location in[?] (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:733:26-733:33)
  write with [region:{in[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & in[tid]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:751:5-751:18)
  write with [region:{in[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & in[tid]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:751:5-751:18)
  read with [region:{in[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & in[i]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:740:10-740:48)
  read with [region:{in[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & in[i]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:740:10-740:48)
  read with [region:{in[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & in[i]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:740:10-740:48)
  read with [region:{in[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & in[i]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:740:10-740:48)
  read with [region:{in[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & in[tid]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:750:6-750:46)
  read with [region:{in[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & in[tid]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:750:6-750:46)
  read with [region:{in[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & in[i___1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:758:10-758:47)
  read with [region:{in[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & in[i___1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:758:10-758:47)
  read with [region:{in[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & in[i___1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:758:10-758:47)
  read with [region:{in[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & in[i___1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:758:10-758:47)
[Warning][Deadcode][CWE-571] condition 'i___0 < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:745:9-745:33)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:739:9-739:33)
[Warning][Deadcode][CWE-570] condition 'i___1 < 2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:756:9-756:33)
[Warning][Deadcode][CWE-570] condition 'i___0 < 2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:745:9-745:33)
[Warning][Race] Memory location post[?] (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:733:35-733:44)
  write with [region:{post[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & post[tid]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:754:5-754:20)
  write with [region:{post[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & post[tid]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:754:5-754:20)
  read with [region:{post[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & post[i]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:741:10-741:50)
  read with [region:{post[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & post[i]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:741:10-741:50)
  read with [region:{post[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & post[i]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:741:10-741:50)
  read with [region:{post[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & post[i]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:741:10-741:50)
  read with [region:{post[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & post[tid]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:753:6-753:48)
  read with [region:{post[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & post[tid]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:753:6-753:48)
[Warning][Deadcode][CWE-570] condition 'i < 2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:739:9-739:33)
[Warning][Deadcode][CWE-571] condition 'i___0 < 1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:780:9-780:37)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:696:73-696:74)
[Warning][Deadcode][CWE-570] condition '! (thread_count > 1)' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:704:6-704:52)
[Warning][Race] Memory location sig2[?] (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:734:26-734:35)
  write with [region:{sig2[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & sig2[tid]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:752:5-752:40)
  write with [region:{sig2[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & sig2[tid]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:752:5-752:40)
  read with [region:{sig2[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & sig2[i___2]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:764:9-764:25)
  read with [region:{sig2[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & sig2[i___2]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:764:9-764:25)
  read with [region:{sig2[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & sig2[i___2]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:764:9-764:25)
  read with [region:{sig2[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & sig2[i___2]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:764:9-764:25)
[Warning][Deadcode][CWE-570] condition 'i___0 < 1' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:780:9-780:37)
[Warning][Race] Memory location sig1[?] (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:734:15-734:24)
  write with [region:{sig1[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & sig1[tid]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:743:5-743:40)
  write with [region:{sig1[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & sig1[tid]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:743:5-743:40)
  read with [region:{sig1[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & sig1[i___0]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:747:9-747:25)
  read with [region:{sig1[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & sig1[i___0]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:747:9-747:25)
  read with [region:{sig1[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & sig1[i___0]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:747:9-747:25)
  read with [region:{sig1[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & sig1[i___0]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:747:9-747:25)
  read with [region:{sig1[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & sig1[i___1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:759:9-759:25)
  read with [region:{sig1[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & sig1[i___1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:759:9-759:25)
  read with [region:{sig1[?]}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & sig1[i___1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:759:9-759:25)
  read with [region:{sig1[?]}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & sig1[i___1]) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:759:9-759:25)
[Warning][Deadcode][CWE-571] condition 'i___2 < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:786:9-786:33)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:772:9-772:33)
[Warning][Deadcode][CWE-571] condition 'i___2 < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:786:9-786:33)
[Warning][Race] Memory location b2.seen (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:770:17-770:19)
  write with [symblock:{p-lock:*.lock}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, lock:{b2.lock}, thread:[main]] (conf. 110)  (exp: & b->seen) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:717:5-717:14)
  read with [mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & b->seen) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:715:6-715:61)
[Warning][Race] Memory location b2.seen (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:770:17-770:19)
  write with [symblock:{p-lock:*.lock}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, lock:{b2.lock}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & b->seen) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:717:5-717:14)
  read with [mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & b->seen) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:715:6-715:61)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:772:9-772:33)
[Warning][Race] Memory location b1.seen (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:770:13-770:15)
  write with [symblock:{p-lock:*.lock}, mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, lock:{b1.lock}, thread:[main]] (conf. 110)  (exp: & b->seen) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:717:5-717:14)
  read with [mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & b->seen) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:715:6-715:61)
[Warning][Race] Memory location b1.seen (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:770:13-770:15)
  write with [symblock:{p-lock:*.lock}, mhp:{tid=[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}, lock:{b1.lock}, thread:[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]] (conf. 110)  (exp: & b->seen) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:717:5-717:14)
  read with [mhp:{tid=[main]; created={[main, worker_fn@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:781:9-781:73#top]}}, thread:[main]] (conf. 110)  (exp: & b->seen) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-divine/one_time_barrier_twice_2t.i:715:6-715:61)
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 5
  vulnerable: 0
  unsafe: 7
  total memory locations: 12
