./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-deagle/arithmetic_prog_ok.i


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i:880:5-881:36 with factor 25
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i:878:3-886:3 with factor 1
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i:894:5-895:35 with factor 25
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i:892:3-901:3 with factor 1
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: 33
functionCalls: 147
loops: 12
loopBreaks: 0
controlFlowStatements: 337
expressions: 1646
instructions: 236
integralVars: (7,38)
arrayVars: (2,0)
pointerVars: (3,14)

Complexity estimates:
File: 19727
Total: 30669
Congruence: 1590
Enabled congruence domain.
Octagon: 3000
Enabled octagon domain for:
num, pthread_cond_wait, i, key, count, a, tmp, j, count, k, size, a, b, c, i, t1, t2, j, i
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, __annonCompField1 : TComp(union __anonunion____missing_field_name_263038923, __wseq : TInt(unsigned long long, ), __wseq32 : TComp(struct __anonstruct___wseq32_817613185, __low : TInt(unsigned int, ), __high : TInt(unsigned int, ), , ), , ), __annonCompField2 : TComp(union __anonunion____missing_field_name_1026474520, __g1_start : TInt(unsigned long long, ), __g1_start32 : TComp(struct __anonstruct___g1_start32_1026474521, __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(Var(empty, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i:911:3-911:31)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(pthread_cond_t, TComp(union __anonunion_pthread_cond_t_951761805, __data : TComp(struct __pthread_cond_s, __annonCompField1 : TComp(union __anonunion____missing_field_name_263038923, __wseq : TInt(unsigned long long, ), __wseq32 : TComp(struct __anonstruct___wseq32_817613185, __low : TInt(unsigned int, ), __high : TInt(unsigned int, ), , ), , ), __annonCompField2 : TComp(union __anonunion____missing_field_name_1026474520, __g1_start : TInt(unsigned long long, ), __g1_start32 : TComp(struct __anonstruct___g1_start32_1026474521, __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(Var(full, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i:912:3-912:30)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i:896:5-896:22)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i:902:3-902:20)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 40
  dead: 0
  total lines: 40
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i:18:73-18:74)
[Warning][Deadcode][CWE-571] condition 'i < 4' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i:878:10-878:15)
[Warning][Deadcode][CWE-571] condition 'j < 4' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i:892:10-892:15)
SV-COMP result: true
[Info][Race] Memory locations race summary:
  safe: 3
  vulnerable: 0
  unsafe: 0
  total memory locations: 3
