./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpv.2023-12-02_00-12-47.files/SV-COMP24_unreach-call/pc_sfifo_2.cil-1+token_ring.04.cil-2.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpv.2023-12-02_00-12-47.files/SV-COMP24_unreach-call/pc_sfifo_2.cil-1+token_ring.04.cil-2.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_2.cil-1+token_ring.04.cil-2.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_2.cil-1+token_ring.04.cil-2.c:147:3-165:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:188:3-219:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:347:3-387:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:427:3-449:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:549:3-582:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:605:3-618:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:641:3-654:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:677:3-690:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:713:3-726:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:911:3-991:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1291:3-1328: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] cannot unassume entry of type violation_sequence
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:161:5-161:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:203:5-203:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:563:9-563:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:613:5-613:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:649:5-649:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:685:5-685:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:721:5-721:15)
[Warning][Deadcode] Function 'immediate_notify_threads' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:107:1-131:1)
[Warning][Deadcode] Function 'error1' has dead code:
  on line 29 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:29-29)
[Warning][Deadcode] Function 'error2' has dead code:
  on line 497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:497-497)
[Warning][Deadcode] Function 'fire_delta_events2' has dead code:
  on line 1003 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1003-1003)
  on line 1008 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1008-1008)
  on line 1013 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1013-1013)
  on line 1018 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1018-1018)
  on line 1023 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1023-1023)
  on line 1028 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1028-1028)
  on line 1033 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1033-1033)
  on line 1038 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1038-1038)
  on line 1043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1043-1043)
  on line 1048 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1048-1048)
[Warning][Deadcode] Function 'init_threads1' has dead code:
  on line 248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:248-248)
  on line 253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:253-253)
[Warning][Deadcode] Function 'init_threads2' has dead code:
  on line 844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:844-844)
  on line 849 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:849-849)
  on line 854 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:854-854)
  on line 859 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:859-859)
  on line 864 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:864-864)
[Warning][Deadcode] Function 'reset_delta_events2' has dead code:
  on line 1061 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1061-1061)
  on line 1066 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1066-1066)
  on line 1071 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1071-1071)
  on line 1076 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1076-1076)
  on line 1081 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1081-1081)
  on line 1086 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1086-1086)
  on line 1091 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1091-1091)
  on line 1096 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1096-1096)
  on line 1101 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1101-1101)
  on line 1106 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1106-1106)
[Warning][Deadcode] Function 'reset_time_events2' has dead code:
  on line 1196 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1196-1196)
  on line 1201 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1201-1201)
  on line 1206 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1206-1206)
  on line 1211 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1211-1211)
  on line 1216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1216-1216)
  on line 1221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1221-1221)
  on line 1226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1226-1226)
  on line 1231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1231-1231)
  on line 1236 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1236-1236)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 411
  dead: 45 (7 in uncalled functions)
  total lines: 456
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:861:7-861:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1017:7-1017:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:713:10-713:11)
[Warning][Deadcode][CWE-571] condition 'p_dw_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:245:7-245:24)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1022:7-1022:16)
[Warning][Deadcode][CWE-571] condition 'c_dr_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:250:7-250:24)
[Warning][Deadcode][CWE-570] condition 'E_M == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1027:7-1027:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:427:10-427:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:549:10-549:11)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1032:7-1032:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1291:10-1291:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1037:7-1037:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1042:7-1042:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1047:7-1047:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:427:10-427:11)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1060:7-1060:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:147:10-147:11)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1065:7-1065:16)
[Warning][Deadcode][CWE-571] condition 'tmp_var == 5' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:576:17-576:29)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1070:7-1070:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:911:10-911:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1075:7-1075:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1080:7-1080:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:641:10-641:11)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:597:9-597:19)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1085:7-1085:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1291:10-1291:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:605:10-605:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:427:10-427:11)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1090:7-1090:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1095:7-1095:15)
[Warning][Deadcode][CWE-571] condition 'c_dr_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:180:9-180:27)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1100:7-1100:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:347:10-347:11)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1105:7-1105:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:713:10-713:11)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:669:9-669:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:677:10-677:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:347:10-347:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:911:10-911:11)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:541:9-541:18)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1190:7-1190:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:549:10-549:11)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1195:7-1195:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:605:10-605:11)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1200:7-1200:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:347:10-347:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1205:7-1205:16)
[Warning][Deadcode][CWE-571] condition 'p_dw_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:139:9-139:27)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1210:7-1210:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:188:10-188:11)
[Warning][Deadcode][CWE-570] condition 'E_M == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1215:7-1215:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1220:7-1220:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1225:7-1225:15)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:841:7-841:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:677:10-677:11)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:633:9-633:19)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1230:7-1230:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1235:7-1235:15)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:846:7-846:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:641:10-641:11)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:851:7-851:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1002:7-1002:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1007:7-1007:16)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:856:7-856:16)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:705:9-705:19)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.04.cil-2.c:1012:7-1012:16)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
