./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/transmitter.02.cil.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/transmitter.02.cil.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/systemc/transmitter.02.cil.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/systemc/transmitter.02.cil.c:66:5-73:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:99:3-111:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:134:3-144:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:271:3-323:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:528:3-565: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] Enabled congruence domain.
[Info] Enabled octagon domain ONLY for:
[Info] M_E, E_1, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, __retres1, tmp, tmp___0, tmp, __retres2, tmp, tmp___0, tmp___1, tmp, tmp_ndt_1, tmp_ndt_2, tmp_ndt_3, __retres1, __retres1, __retres1, __retres1
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid
[Warning][Deadcode] Function 'error' has dead code:
  on line 22 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:22-22)
[Warning][Deadcode] Function 'fire_delta_events' has dead code:
  on line 335 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:335-335)
  on line 340 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:340-340)
  on line 345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:345-345)
  on line 350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:350-350)
  on line 355 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:355-355)
[Warning][Deadcode] Function 'init_threads' has dead code:
  on line 224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:224-224)
  on line 229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:229-229)
  on line 234 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:234-234)
[Warning][Deadcode] Function 'reset_delta_events' has dead code:
  on line 368 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:368-368)
  on line 373 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:373-373)
  on line 378 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:378-378)
  on line 383 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:383-383)
  on line 388 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:388-388)
[Warning][Deadcode] Function 'reset_time_events' has dead code:
  on line 460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:460-460)
  on line 465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:465-465)
  on line 470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:470-470)
  on line 475 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:475-475)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 170
  dead: 18
  total lines: 188
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:226:7-226:16)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:231:7-231:16)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:126:9-126:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:134:10-134:11)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:454:7-454:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:459:7-459:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:464:7-464:16)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:469:7-469:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:474:7-474:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:271:10-271:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:66:12-66:13)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:528:10-528:11)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:91:9-91:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:271:10-271:11)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:50:9-50:18)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:99:10-99:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:58:10-58:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:66:12-66:13)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:528:10-528:11)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:334:7-334:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:339:7-339:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:344:7-344:16)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:349:7-349:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:354:7-354:15)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:367:7-367:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:372:7-372:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:377:7-377:16)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:382:7-382:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:387:7-387:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:99:10-99:11)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.02.cil.c:221:7-221:15)
[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)
