./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.05.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.05.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.05.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.05.cil.c:84:5-91:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:117:3-129:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:152:3-164:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:187:3-199:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:222:3-234:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:257:3-267:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:900:3-937: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] immediate_notify, M_E, 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___4, tmp, tmp_ndt_1, tmp_ndt_2, tmp_ndt_3, tmp_ndt_4, tmp_ndt_5, tmp_ndt_6, __retres1, __retres1, __retres1, __retres1, __retres1, __retres1, __retres1
[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.05.cil.c:22-22)
[Warning][Deadcode] Function 'fire_delta_events' has dead code:
  on line 587 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:587-587)
  on line 592 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:592-592)
  on line 597 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:597-597)
  on line 602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:602-602)
  on line 607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:607-607)
  on line 612 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:612-612)
  on line 617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:617-617)
  on line 622 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:622-622)
  on line 627 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:627-627)
  on line 632 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:632-632)
  on line 637 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:637-637)
[Warning][Deadcode] Function 'init_threads' has dead code:
  on line 404 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:404-404)
  on line 409 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:409-409)
  on line 414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:414-414)
  on line 419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:419-419)
  on line 424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:424-424)
  on line 429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:429-429)
[Warning][Deadcode] Function 'reset_delta_events' has dead code:
  on line 650 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:650-650)
  on line 655 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:655-655)
  on line 660 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:660-660)
  on line 665 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:665-665)
  on line 670 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:670-670)
  on line 675 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:675-675)
  on line 680 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:680-680)
  on line 685 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:685-685)
  on line 690 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:690-690)
  on line 695 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:695-695)
  on line 700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:700-700)
[Warning][Deadcode] Function 'reset_time_events' has dead code:
  on line 799 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:799-799)
  on line 804 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:804-804)
  on line 809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:809-809)
  on line 814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:814-814)
  on line 819 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:819-819)
  on line 824 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:824-824)
  on line 829 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:829-829)
  on line 834 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:834-834)
  on line 839 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:839-839)
  on line 844 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:844-844)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 275
  dead: 39
  total lines: 314
[Warning][Deadcode][CWE-570] condition 'T5_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:611:7-611:16)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:401:7-401:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:616:7-616:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:621:7-621:15)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:406:7-406:16)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:626:7-626:15)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:144:9-144:19)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:411:7-411:16)
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:631:7-631:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:152:10-152:11)
[Warning][Deadcode][CWE-570] condition 'E_5 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:636:7-636:15)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:416:7-416:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:649:7-649:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:900:10-900:11)
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:421:7-421:16)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:654:7-654:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:187:10-187:11)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:659:7-659:16)
[Warning][Deadcode][CWE-571] condition 't5_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:426:7-426:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:664:7-664:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:669:7-669:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:674:7-674:16)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:679:7-679:15)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:214:9-214:19)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:684:7-684:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:222:10-222:11)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:689:7-689:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:84:12-84:13)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:694:7-694:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:900:10-900:11)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:699:7-699:15)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:109:9-109:19)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:68:9-68:18)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:481:10-481:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:117:10-117:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:76:10-76:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:152:10-152:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:84:12-84:13)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:179:9-179:19)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:793:7-793:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:187:10-187:11)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:798:7-798:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:803:7-803:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:808:7-808:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:222:10-222:11)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:813:7-813:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:818:7-818:16)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:823:7-823:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:828:7-828:15)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:586:7-586:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:833:7-833:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:591:7-591:16)
[Warning][Deadcode][CWE-571] condition 't5_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:249:9-249:19)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:838:7-838:15)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:596:7-596:16)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:843:7-843:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:257:10-257:11)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:601:7-601:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:117:10-117:11)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.05.cil.c:606:7-606:16)
[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)
