./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/pc_sfifo_3.cil+token_ring.06.cil-1.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/pc_sfifo_3.cil+token_ring.06.cil-1.yml/witness.yml --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/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:172:3-195:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:218:3-255:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:418:3-458:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:499:3-536:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:664:3-697:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:720:3-733:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:756:3-769:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:792:3-805:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:828:3-841:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:864:3-877:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:900:3-913:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1644:3-1681:3 with factor 1
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:191:5-191:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:678:9-678:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:728:5-728:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:764:5-764:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:800:5-800:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:836:5-836:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:872:5-872:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:908:5-908:15)
[Warning][Deadcode] Function 'error1' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:23:1-30:1)
[Warning][Deadcode] Function 'immediate_notify_threads' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:128:1-152:1)
[Warning][Deadcode] Function 'do_read_c' has dead code:
  on lines 225..229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:225-229)
  on line 233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:233-233)
  on lines 237..243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:237-243)
  on line 247 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:247-247)
  on line 252 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:252-252)
[Warning][Deadcode] Function 'error2' has dead code:
  on line 600 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:600-600)
[Warning][Deadcode] Function 'fire_delta_events2' has dead code:
  on line 1276 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1276-1276)
  on line 1281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1281-1281)
  on line 1286 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1286-1286)
  on line 1291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1291-1291)
  on line 1296 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1296-1296)
  on line 1301 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1301-1301)
  on line 1306 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1306-1306)
  on line 1311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1311-1311)
  on line 1316 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1316-1316)
  on line 1321 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1321-1321)
  on line 1326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1326-1326)
  on line 1331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1331-1331)
  on line 1336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1336-1336)
  on line 1341 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1341-1341)
[Warning][Deadcode] Function 'init_threads1' has dead code:
  on line 284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:284-284)
  on line 289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:289-289)
[Warning][Deadcode] Function 'init_threads2' has dead code:
  on line 1069 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1069-1069)
  on line 1074 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1074-1074)
  on line 1079 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1079-1079)
  on line 1084 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1084-1084)
  on line 1089 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1089-1089)
  on line 1094 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1094-1094)
  on line 1099 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1099-1099)
[Warning][Deadcode] Function 'is_do_read_c_triggered' has dead code:
  on lines 114..115 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:114-115)
[Warning][Deadcode] Function 'reset_delta_events2' has dead code:
  on line 1354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1354-1354)
  on line 1359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1359-1359)
  on line 1364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1364-1364)
  on line 1369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1369-1369)
  on line 1374 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1374-1374)
  on line 1379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1379-1379)
  on line 1384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1384-1384)
  on line 1389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1389-1389)
  on line 1394 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1394-1394)
  on line 1399 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1399-1399)
  on line 1404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1404-1404)
  on line 1409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1409-1409)
  on line 1414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1414-1414)
  on line 1419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1419-1419)
[Warning][Deadcode] Function 'reset_time_events2' has dead code:
  on line 1527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1527-1527)
  on line 1532 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1532-1532)
  on line 1537 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1537-1537)
  on line 1542 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1542-1542)
  on line 1547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1547-1547)
  on line 1552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1552-1552)
  on line 1557 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1557-1557)
  on line 1562 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1562-1562)
  on line 1567 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1567-1567)
  on line 1572 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1572-1572)
  on line 1577 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1577-1577)
  on line 1582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1582-1582)
  on line 1587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1587-1587)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 499
  dead: 77 (9 in uncalled functions)
  total lines: 576
[Warning][Deadcode][CWE-571] condition 'c_dr_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:286:7-286:24)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:864:10-864:11)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:820:9-820:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:828:10-828:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:499:10-499:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:664:10-664:11)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1521:7-1521:15)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1275:7-1275:15)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1066:7-1066:15)
[Warning][Deadcode][CWE-571] condition 't6_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:892:9-892:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:172:10-172:11)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1526:7-1526:16)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1280:7-1280:16)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1071:7-1071:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:900:10-900:11)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1531:7-1531:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1285:7-1285:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1536:7-1536:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1290:7-1290:16)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1076:7-1076:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1541:7-1541:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1295:7-1295:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1546:7-1546:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1300:7-1300:16)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1081:7-1081:16)
[Warning][Deadcode][CWE-571] condition 'tmp_var == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:691:17-691:29)
[Warning][Deadcode][CWE-571] condition 'fast_clk_edge == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:373:7-373:31)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1551:7-1551:16)
[Warning][Deadcode][CWE-570] condition 'T6_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1305:7-1305:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:499:10-499:11)
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1086:7-1086:16)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1556:7-1556:15)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1310:7-1310:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1561:7-1561:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1315:7-1315:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:756:10-756:11)
[Warning][Deadcode][CWE-571] condition 't5_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1091:7-1091:16)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:712:9-712:19)
[Warning][Deadcode][CWE-570] condition 'c_dr_pc == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:210:9-210:27)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1566:7-1566:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1320:7-1320:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:720:10-720:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:218:10-218:11)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1571:7-1571:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1325:7-1325:15)
[Warning][Deadcode][CWE-571] condition 't6_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1096:7-1096:16)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1576:7-1576:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1330:7-1330:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:418:10-418:11)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1581:7-1581:15)
[Warning][Deadcode][CWE-570] condition 'E_5 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1335:7-1335:15)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1586:7-1586:15)
[Warning][Deadcode][CWE-570] condition 'E_6 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1340:7-1340:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:828:10-828:11)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:784:9-784:19)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1353:7-1353:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:792:10-792:11)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1358:7-1358:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1363:7-1363:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1368:7-1368:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1373:7-1373:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:900:10-900:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:418:10-418:11)
[Warning][Deadcode][CWE-571] condition 't5_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:856:9-856:19)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1378:7-1378:16)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1383:7-1383:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:864:10-864:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:218:10-218:11)
[Warning][Deadcode][CWE-570] condition 'c_dr_pc == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:113:7-113:25)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1388:7-1388:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1393:7-1393:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1644:10-1644:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1398:7-1398:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1156:10-1156:11)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:656:9-656:18)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1403:7-1403:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1408:7-1408:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:664:10-664:11)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1413:7-1413:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:720:10-720:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:418:10-418:11)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1418:7-1418:15)
[Warning][Deadcode][CWE-571] condition 'p_dw_pc == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:163:11-163:29)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:1644:10-1644:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:792:10-792:11)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:748:9-748:19)
[Warning][Deadcode][CWE-571] condition 'p_dw_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:281:7-281:24)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_3.cil+token_ring.06.cil-1.c:756:10-756:11)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
