./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/goblint-regression/28-race_reach_72-funloop_hard_racing.i


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:941:42-941:149 with factor 16
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:941:151-941:258 with factor 16
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:941:278-941:407 with factor 16
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:946:3-946:52 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:950:3-951:58 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:27-953:113 with factor 25
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:954:3-954:52 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:956:42-956:151 with factor 16
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:956:153-956:262 with factor 16
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:956:282-956:413 with factor 16
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
has Label
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:3-958:69 with factor 25
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: 40
functionCalls: 362
loops: 21
loopBreaks: 0
controlFlowStatements: 533
expressions: 2907
instructions: 603
integralVars: (5,50)
arrayVars: (4,1)
pointerVars: (3,14)

Complexity estimates:
File: 321596
Total: 321596
SV-COMP specification: CHECK( init(main()), LTL(G ! data-race) )

runtime: 00:00:10.132
vars: 58163, evals: 197387

|rho|=58163
|stable|=58163
|infl|=58017
|wpoint|=5
|sides|=1157
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=56012
|called|=149
Found 1011 contexts for 6 functions. Top 5 functions:
247	contexts for L:entry state of __VERIFIER_assert (1560) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:929:1-929:84
246	contexts for L:entry state of cache_entry_addref (1569) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:939:1-943:1
246	contexts for L:entry state of reach_error (1558) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:928:1-928:163
246	contexts for L:entry state of __VERIFIER_nondet_int (1563) on lib/sv-comp/stub/src/sv-comp.c:22:60-22:141
25	contexts for L:entry state of t_fun (1573) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:944:1-948:1

Memory statistics: total=7745.80MB, max=95.00MB, minor=7738.13MB, major=266.42MB, promoted=258.75MB
    minor collections=3701  major collections=24 compactions=0


runtime: 00:00:20.158
vars: 64138, evals: 256456

|rho|=64138
|stable|=38905
|infl|=64061
|wpoint|=10
|sides|=1270
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=61773
|called|=171
Found 1113 contexts for 6 functions. Top 5 functions:
272	contexts for L:entry state of __VERIFIER_assert (1560) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:929:1-929:84
271	contexts for L:entry state of cache_entry_addref (1569) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:939:1-943:1
271	contexts for L:entry state of reach_error (1558) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:928:1-928:163
271	contexts for L:entry state of __VERIFIER_nondet_int (1563) on lib/sv-comp/stub/src/sv-comp.c:22:60-22:141
27	contexts for L:entry state of t_fun (1573) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:944:1-948:1

Memory statistics: total=10602.95MB, max=109.25MB, minor=10595.21MB, major=342.15MB, promoted=334.42MB
    minor collections=5065  major collections=26 compactions=0

[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:941:84-941:98)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:941:193-941:207)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:956:84-956:100)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:956:195-956:211)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:62:1-66:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:67:1-71:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:72:1-76:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:77:1-81:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:82:1-86:1)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:931:1-933:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 21
  dead: 7 (7 in uncalled functions)
  total lines: 28
[Warning][Deadcode][CWE-571] condition 'i___0 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:954:6-954:21)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:946:6-946:21)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-571] condition 'i___0 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:954:6-954:21)
[Warning][Deadcode][CWE-570] condition 'i < 10' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:946:6-946:21)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:941:269-941:271)
[Warning][Deadcode][CWE-571] condition 'i___0 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:954:6-954:21)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:956:273-956:275)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-571] condition 'i___0 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:954:6-954:21)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:941:405-941:407)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:956:411-956:413)
[Warning][Deadcode][CWE-571] condition 'i___0 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:954:6-954:21)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:950:7-950:30)
[Warning][Deadcode][CWE-571] condition 'i___0 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:954:6-954:21)

runtime: 00:00:30.176
vars: 66529, evals: 287544

|rho|=66531
|stable|=66531
|infl|=66522
|wpoint|=6
|sides|=1353
|side_dep|=1361
|side_infl|=8630
|var_messages|=4
|rho_write|=6330
|dep|=64035
|called|=0
Found 1151 contexts for 6 functions. Top 5 functions:
281	contexts for L:entry state of __VERIFIER_assert (1560) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:929:1-929:84
281	contexts for L:entry state of reach_error (1558) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:928:1-928:163
281	contexts for L:entry state of __VERIFIER_nondet_int (1563) on lib/sv-comp/stub/src/sv-comp.c:22:60-22:141
280	contexts for L:entry state of cache_entry_addref (1569) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:939:1-943:1
27	contexts for L:entry state of t_fun (1573) on /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:944:1-948:1

Memory statistics: total=15587.98MB, max=125.64MB, minor=15573.51MB, major=482.84MB, promoted=468.37MB
    minor collections=7441  major collections=30 compactions=0

[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:941:418-941:420)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:950:7-950:30)
[Warning][Deadcode][CWE-571] condition 'i___0 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:954:6-954:21)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:956:424-956:426)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:950:7-950:30)
[Warning][Deadcode][CWE-570] condition 'i___0 < 10' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:954:6-954:21)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:946:6-946:21)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:950:7-950:30)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:928:73-928:74)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:946:6-946:21)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:950:7-950:30)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:946:6-946:21)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:950:7-950:30)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:946:6-946:21)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:950:7-950:30)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:946:6-946:21)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:941:147-941:149)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:950:7-950:30)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:946:6-946:21)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:956:149-956:151)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:950:7-950:30)
[Warning][Deadcode][CWE-571] condition 'i___0 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:954:6-954:21)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:946:6-946:21)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:950:7-950:30)
[Warning][Deadcode][CWE-571] condition 'i___0 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:954:6-954:21)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:946:6-946:21)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-570] condition 'i < 10' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:950:7-950:30)
[Warning][Deadcode][CWE-571] condition 'i___0 < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:954:6-954:21)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:946:6-946:21)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:941:256-941:258)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___2 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:958:7-958:31)
[Warning][Deadcode][CWE-571] condition 'i___1 < 10000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:953:31-953:53)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i:956:260-956:262)
SV-COMP result: true
[Info][Race] Memory locations race summary:
  safe: 1
  vulnerable: 0
  unsafe: 0
  total memory locations: 1
