./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.03.cil-1.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.03.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_2.cil-1+token_ring.03.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_2.cil-1+token_ring.03.cil-1.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.03.cil-1.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.03.cil-1.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.03.cil-1.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.03.cil-1.c:543:3-576:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:599:3-612:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:635:3-648:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:671:3-684:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:840:3-906:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:1166:3-1203: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.03.cil-1.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.03.cil-1.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.03.cil-1.c:557:9-557:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:607:5-607:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:643:5-643:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:679:5-679: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.03.cil-1.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.03.cil-1.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.03.cil-1.c:497-497)
[Warning][Deadcode] Function 'fire_delta_events2' has dead code:
  on line 918 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:918-918)
  on line 923 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:923-923)
  on line 928 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:928-928)
  on line 933 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:933-933)
  on line 938 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:938-938)
  on line 943 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:943-943)
  on line 948 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:948-948)
  on line 953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:953-953)
[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.03.cil-1.c:248-248)
  on line 253 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:253-253)
[Warning][Deadcode] Function 'init_threads2' has dead code:
  on line 783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:783-783)
  on line 788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:788-788)
  on line 793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:793-793)
  on line 798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:798-798)
[Warning][Deadcode] Function 'reset_delta_events2' has dead code:
  on line 966 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:966-966)
  on line 971 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:971-971)
  on line 976 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:976-976)
  on line 981 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:981-981)
  on line 986 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:986-986)
  on line 991 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:991-991)
  on line 996 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:996-996)
  on line 1001 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:1001-1001)
[Warning][Deadcode] Function 'reset_time_events2' has dead code:
  on line 1082 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:1082-1082)
  on line 1087 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:1087-1087)
  on line 1092 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:1092-1092)
  on line 1097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:1097-1097)
  on line 1102 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:1102-1102)
  on line 1107 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:1107-1107)
  on line 1112 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/combinations/pc_sfifo_2.cil-1+token_ring.03.cil-1.c:1112-1112)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 375
  dead: 38 (7 in uncalled functions)
  total lines: 413
[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.03.cil-1.c:245:7-245:24)
[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.03.cil-1.c:250:7-250:24)
[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.03.cil-1.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.03.cil-1.c:543:10-543: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.03.cil-1.c:1166:10-1166:11)
[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.03.cil-1.c:917:7-917: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.03.cil-1.c:922:7-922: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.03.cil-1.c:427:10-427:11)
[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.03.cil-1.c:927:7-927: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.03.cil-1.c:147:10-147:11)
[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.03.cil-1.c:932:7-932: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.03.cil-1.c:570:17-570:29)
[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.03.cil-1.c:780:7-780:15)
[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.03.cil-1.c:937:7-937:15)
[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.03.cil-1.c:942:7-942: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.03.cil-1.c:785:7-785:16)
[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.03.cil-1.c:947:7-947: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.03.cil-1.c:635:10-635: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.03.cil-1.c:591:9-591:19)
[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.03.cil-1.c:952:7-952:15)
[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.03.cil-1.c:790:7-790: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.03.cil-1.c:1166:10-1166: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.03.cil-1.c:599:10-599: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.03.cil-1.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.03.cil-1.c:965:7-965:15)
[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.03.cil-1.c:795:7-795:16)
[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.03.cil-1.c:180:9-180:27)
[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.03.cil-1.c:970:7-970:16)
[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.03.cil-1.c:975:7-975: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.03.cil-1.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.03.cil-1.c:980:7-980:16)
[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.03.cil-1.c:663:9-663: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.03.cil-1.c:985:7-985: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.03.cil-1.c:990:7-990: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.03.cil-1.c:671:10-671:11)
[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.03.cil-1.c:995:7-995:15)
[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.03.cil-1.c:1000:7-1000: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.03.cil-1.c:840:10-840: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.03.cil-1.c:347:10-347: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.03.cil-1.c:535:9-535:18)
[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.03.cil-1.c:543:10-543: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.03.cil-1.c:599:10-599:11)
[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.03.cil-1.c:1076:7-1076: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.03.cil-1.c:347:10-347: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.03.cil-1.c:1081:7-1081: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.03.cil-1.c:139:9-139:27)
[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.03.cil-1.c:188:10-188: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.03.cil-1.c:1086:7-1086:16)
[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.03.cil-1.c:1091:7-1091:16)
[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.03.cil-1.c:1096:7-1096: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.03.cil-1.c:840:10-840: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.03.cil-1.c:671:10-671: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.03.cil-1.c:1101:7-1101:15)
[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.03.cil-1.c:627:9-627:19)
[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.03.cil-1.c:1106:7-1106: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.03.cil-1.c:635:10-635:11)
[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.03.cil-1.c:1111:7-1111:15)
[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
