./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.04.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.04.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.04.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.04.cil.c:78:5-85:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:111:3-123:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:146:3-158:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:181:3-193:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:216:3-226:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:411:3-491:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:776:3-813: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___2, tmp___3, tmp, tmp_ndt_1, tmp_ndt_2, tmp_ndt_3, tmp_ndt_4, tmp_ndt_5, __retres1, __retres1, __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.04.cil.c:22-22)
[Warning][Deadcode] Function 'fire_delta_events' has dead code:
  on line 503 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:503-503)
  on line 508 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:508-508)
  on line 513 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:513-513)
  on line 518 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:518-518)
  on line 523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:523-523)
  on line 528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:528-528)
  on line 533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:533-533)
  on line 538 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:538-538)
  on line 543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:543-543)
[Warning][Deadcode] Function 'init_threads' has dead code:
  on line 344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:344-344)
  on line 349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:349-349)
  on line 354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:354-354)
  on line 359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:359-359)
  on line 364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:364-364)
[Warning][Deadcode] Function 'reset_delta_events' has dead code:
  on line 556 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:556-556)
  on line 561 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:561-561)
  on line 566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:566-566)
  on line 571 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:571-571)
  on line 576 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:576-576)
  on line 581 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:581-581)
  on line 586 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:586-586)
  on line 591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:591-591)
  on line 596 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:596-596)
[Warning][Deadcode] Function 'reset_time_events' has dead code:
  on line 686 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:686-686)
  on line 691 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:691-691)
  on line 696 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:696-696)
  on line 701 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:701-701)
  on line 706 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:706-706)
  on line 711 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:711-711)
  on line 716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:716-716)
  on line 721 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:721-721)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 240
  dead: 32
  total lines: 272
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:411:10-411:11)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:138:9-138:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:146:10-146:11)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:680:7-680:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:685:7-685:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:690:7-690:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:181:10-181:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:695:7-695:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:700:7-700:16)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:705:7-705:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:710:7-710:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:715:7-715:15)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:208:9-208:19)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:720:7-720:15)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:341:7-341:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:216:10-216:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:78:12-78:13)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:346:7-346:16)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:351:7-351:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:502:7-502:15)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:356:7-356:16)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:507:7-507:16)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:103:9-103:19)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:512:7-512:16)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:62:9-62:18)
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:361:7-361:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:517:7-517:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:111:10-111:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:776:10-776:11)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:522:7-522:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:70:10-70:11)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:527:7-527:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:146:10-146:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:532:7-532:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:78:12-78:13)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:537:7-537:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:542:7-542:15)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:555:7-555:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:560:7-560:16)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:173:9-173:19)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:565:7-565:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:570:7-570:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:411:10-411:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:181:10-181:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:776:10-776:11)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:575:7-575:16)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:580:7-580:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:585:7-585:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:590:7-590:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:595:7-595:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.04.cil.c:111:10-111: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)
