./goblint --conf conf/svcomp23.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
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
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:95:17-95:38 with factor 12
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:270:3-277:6 with factor 3
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:278:3-285:4 with factor 3
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:286:3-293:6 with factor 3
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:294:3-301:4 with factor 3
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:313:3-319:3 with factor 4
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:322:3-328:3 with factor 4
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:366:3-378:3 with factor 5
unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:464:3-541:3 with factor 2
Collected factors:
functions: 47
functionCalls: 125
loops: 16
loopBreaks: 0
controlFlowStatements: 571
expressions: 3377
instructions: 580
integralVars: (4,81)
arrayVars: (2,2)
pointerVars: (0,35)

Complexity estimates:
File: 55969
no thread creation -> disabeling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn"
Total: 55969
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Unsound] Unknown value in {&g_history[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:102:3-102:25)
[Info][Unsound] Unknown value in {&wrBuffer0} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:103:3-103:30)
[Info][Unsound] Unknown value in {&wrBuffer1} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:104:3-104:30)
[Info][Unsound] Unknown value in {&wrBuffer2} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:105:3-105:30)
[Info][Unsound] Unknown value in {&wrBuffer3} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:106:3-106:30)
[Info][Unsound] Unknown value in {&litmus_input} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:108:3-108:41)
[Info][Unsound] Unknown value in {&litmus_input} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:304:3-304:45)
[Info][Unsound] Unknown value in {&litmus_input} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:305:3-305:32)
[Info][Unsound] Unknown value in {&litmus_input} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:306:3-306:45)
[Info][Unsound] Unknown value in {&wrBuffer3} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:243:9-243:50)
[Info][Unsound] Unknown value in {&wrBuffer3} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:231:13-231:91)
[Info][Unsound] Unknown value in {&g_history[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:231:13-231:91)
[Info][Unsound] Unknown value in {&wrBuffer3} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:388:7-388:55)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:365:17-365:79)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:374:7-374:34)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:374:7-374:34)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:394:3-394:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:232:13-232:37)
[Info][Unsound] Unknown value in {&g_history[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:226:13-226:66)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:346:3-346:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:227:13-227:37)
[Info][Unsound] Unknown value in {&wrBuffer3} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:220:13-220:78)
[Info][Unsound] Unknown value in {&g_history[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:220:13-220:78)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:340:3-340:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:221:13-221:37)
[Info][Unsound] Unknown value in {&wrBuffer2} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:212:9-212:50)
[Info][Unsound] Unknown value in {&wrBuffer2} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:200:13-200:91)
[Info][Unsound] Unknown value in {&g_history[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:200:13-200:91)
[Info][Unsound] Unknown value in {&wrBuffer2} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:388:7-388:55)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:201:13-201:37)
[Info][Unsound] Unknown value in {&g_history[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:195:13-195:66)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:196:13-196:37)
[Info][Unsound] Unknown value in {&wrBuffer2} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:189:13-189:78)
[Info][Unsound] Unknown value in {&g_history[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:189:13-189:78)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:190:13-190:37)
[Info][Unsound] Unknown value in {&wrBuffer1} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:181:9-181:50)
[Info][Unsound] Unknown value in {&wrBuffer1} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:169:13-169:91)
[Info][Unsound] Unknown value in {&g_history[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:169:13-169:91)
[Info][Unsound] Unknown value in {&wrBuffer1} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:388:7-388:55)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:170:13-170:37)
[Info][Unsound] Unknown value in {&g_history[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:164:13-164:66)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:165:13-165:37)
[Info][Unsound] Unknown value in {&wrBuffer1} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:158:13-158:78)
[Info][Unsound] Unknown value in {&g_history[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:158:13-158:78)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:159:13-159:37)
[Info][Unsound] Unknown value in {&wrBuffer0} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:150:9-150:50)
[Info][Unsound] Unknown value in {&wrBuffer0} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:138:13-138:91)
[Info][Unsound] Unknown value in {&g_history[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:138:13-138:91)
[Info][Unsound] Unknown value in {&wrBuffer0} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:388:7-388:55)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:139:13-139:37)
[Info][Unsound] Unknown value in {&g_history[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:133:13-133:66)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:134:13-134:37)
[Info][Unsound] Unknown value in {&wrBuffer0} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:127:13-127:78)
[Info][Unsound] Unknown value in {&g_history[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:127:13-127:78)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:128:13-128:37)
[Info][Unsound] Unknown value in {&g_history[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:262:5-262:45)
[Info][Unsound] Unknown value in {&g_history[def_exc:0; intervals:[0,0]; enums:{0}]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:310:3-310:42)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 333
  dead: 0
  total: 333
[Warning][Deadcode][CWE-571] condition 'event_i1 == -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:476:16-480:31)
[Warning][Deadcode][CWE-570] condition 'tmp >= 10U' (possibly inserted by CIL) is always false (:-1)
[Warning][Deadcode][CWE-570] condition 'tmp >= 10U' (possibly inserted by CIL) is always false (:-1)
[Warning][Deadcode][CWE-571] condition 'event_i2 == -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:485:16-490:31)
[Warning][Deadcode][CWE-571] condition 'i___1 < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:286:7-286:35)
[Warning][Deadcode][CWE-570] condition 'i___1 < cpu2_operations' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:287:9-287:28)
[Warning][Deadcode][CWE-570] condition 'tmp >= 10U' (possibly inserted by CIL) is always false (:-1)
[Warning][Deadcode][CWE-571] condition 'event_i3 == -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:495:16-499:31)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:235:20-235:24)
[Warning][Deadcode][CWE-570] condition 'tmp >= 10U' (possibly inserted by CIL) is always false (:-1)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:238:18-238:22)
[Warning][Deadcode][CWE-571] condition 'event_i4 == -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:504:16-509:31)
[Warning][Deadcode][CWE-571] condition 'tmp >= 10U' (possibly inserted by CIL) is always true (:-1)
[Warning][Deadcode][CWE-570] condition 'i___1 < cpu2_operations' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:287:9-287:28)
[Warning][Deadcode][CWE-571] condition 'event_i5 == -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:514:16-518:31)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:246:16-246:20)
[Warning][Deadcode][CWE-571] condition 'event_i6 == -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:523:16-528:31)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:366:6-366:26)
[Warning][Deadcode][CWE-571] condition 'event_i7 == -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:533:16-537:31)
[Warning][Deadcode][CWE-571] condition 'i___2 < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:294:7-294:36)
[Warning][Deadcode][CWE-571] condition 'i___2 < cpu3_operations' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:295:9-295:28)
[Warning][Deadcode][CWE-571] condition 'i < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:464:7-464:35)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:366:6-366:26)
[Warning][Deadcode][CWE-571] condition 'i___2 < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:294:7-294:36)
[Warning][Deadcode][CWE-571] condition 'i___2 < cpu3_operations' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:295:9-295:28)
[Warning][Deadcode][CWE-571] condition 'i < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:270:7-270:35)
[Warning][Deadcode][CWE-571] condition 'i < cpu0_operations' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:271:9-271:28)
[Warning][Deadcode][CWE-570] condition 'i < 2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:366:6-366:26)
[Warning][Deadcode][CWE-571] condition 'i___2 < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:294:7-294:36)
[Warning][Deadcode][CWE-570] condition 'i___2 < cpu3_operations' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:295:9-295:28)
[Warning][Deadcode][CWE-571] condition 'i < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:270:7-270:35)
[Warning][Deadcode][CWE-571] condition 'i < cpu0_operations' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:271:9-271:28)
[Warning][Deadcode][CWE-570] condition 'i___2 < cpu3_operations' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:295:9-295:28)
[Warning][Deadcode][CWE-571] condition 'i < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:270:7-270:35)
[Warning][Deadcode][CWE-570] condition 'i < cpu0_operations' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:271:9-271:28)
[Warning][Deadcode][CWE-570] condition 'i < cpu0_operations' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:271:9-271:28)
[Warning][Deadcode][CWE-571] condition 'i < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:313:6-313:34)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:142:20-142:24)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:145:18-145:22)
[Warning][Deadcode][CWE-571] condition 'i < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:313:6-313:34)
[Warning][Deadcode][CWE-571] condition 'i___0 < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:278:7-278:36)
[Warning][Deadcode][CWE-571] condition 'i___0 < cpu1_operations' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:279:9-279:28)
[Warning][Deadcode][CWE-571] condition 'i < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:313:6-313:34)
[Warning][Deadcode][CWE-571] condition 'i___0 < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:278:7-278:36)
[Warning][Deadcode][CWE-571] condition 'i < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:313:6-313:34)
[Warning][Deadcode][CWE-571] condition 'i___0 < cpu1_operations' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:279:9-279:28)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:173:20-173:24)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:176:18-176:22)
[Warning][Deadcode][CWE-571] condition 'i___0 < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:278:7-278:36)
[Warning][Deadcode][CWE-570] condition 'i___0 < cpu1_operations' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:279:9-279:28)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:322:6-322:28)
[Warning][Deadcode][CWE-570] condition 'i___0 < cpu1_operations' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:279:9-279:28)
[Warning][Deadcode][CWE-571] condition 'event_i1 != -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:543:16-555:16)
[Warning][Deadcode][CWE-570] condition 'tmp >= 10U' (possibly inserted by CIL) is always false (:-1)
[Warning][Deadcode][CWE-571] condition 'event_i3 != -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:543:16-555:16)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:322:6-322:28)
[Warning][Deadcode][CWE-571] condition 'event_i5 != -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:543:16-555:16)
[Warning][Deadcode][CWE-571] condition 'event_i7 != -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:543:16-555:16)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:543:16-555:16)
[Warning][Deadcode][CWE-570] condition 'tmp >= 10U' (possibly inserted by CIL) is always false (:-1)
[Warning][Deadcode][CWE-570] condition 'i < 2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:322:6-322:28)
[Warning][Deadcode][CWE-571] condition 'i___1 < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:286:7-286:35)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:204:20-204:24)
[Warning][Deadcode][CWE-570] condition 'tmp >= 10U' (possibly inserted by CIL) is always false (:-1)
[Warning][Deadcode][CWE-571] condition 'i___1 < cpu2_operations' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:287:9-287:28)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:207:18-207:22)
[Warning][Deadcode][CWE-570] condition 'tmp >= 10U' (possibly inserted by CIL) is always false (:-1)
[Warning][Deadcode][CWE-571] condition 'i < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:464:7-464:35)
[Warning][Deadcode][CWE-571] condition 'event_i0 == -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:466:16-471:31)
[Warning][Deadcode][CWE-570] condition 'tmp >= 10U' (possibly inserted by CIL) is always false (:-1)
[Warning][Deadcode][CWE-571] condition 'i___1 < 14' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:286:7-286:35)
[Warning][Deadcode][CWE-571] condition 'i___1 < cpu2_operations' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/4SB.i:287:9-287:28)
SV-COMP result: unknown
