./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/transmitter.03.cil.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/transmitter.03.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.03.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.03.cil.c:72:5-79:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:105:3-117:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:140:3-152:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:175:3-185:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:341:3-407:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:652:3-689: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, tmp_ndt_1, tmp_ndt_2, tmp_ndt_3, tmp_ndt_4, __retres1, __retres1, __retres1, __retres1, __retres1
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Deadcode] Function 'error' has dead code:
  on line 22 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:22-22)
[Warning][Deadcode] Function 'fire_delta_events' has dead code:
  on line 419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:419-419)
  on line 424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:424-424)
  on line 429 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:429-429)
  on line 434 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:434-434)
  on line 439 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:439-439)
  on line 444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:444-444)
  on line 449 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:449-449)
[Warning][Deadcode] Function 'init_threads' has dead code:
  on line 284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:284-284)
  on line 289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:289-289)
  on line 294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:294-294)
  on line 299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:299-299)
[Warning][Deadcode] Function 'reset_delta_events' has dead code:
  on line 462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:462-462)
  on line 467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:467-467)
  on line 472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:472-472)
  on line 477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:477-477)
  on line 482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:482-482)
  on line 487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:487-487)
  on line 492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:492-492)
[Warning][Deadcode] Function 'reset_time_events' has dead code:
  on line 573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:573-573)
  on line 578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:578-578)
  on line 583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:583-583)
  on line 588 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:588-588)
  on line 593 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:593-593)
  on line 598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:598-598)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 205
  dead: 25
  total lines: 230
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:132:9-132:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:140:10-140:11)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:567:7-567:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:572:7-572:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:577:7-577:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:582:7-582:16)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:587:7-587:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:592:7-592:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:597:7-597:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:341:10-341:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:72:12-72:13)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:97:9-97:19)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:56:9-56:18)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:652:10-652:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:105:10-105:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:64:10-64:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:140:10-140:11)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:418:7-418:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:72:12-72:13)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:423:7-423:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:428:7-428:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:433:7-433:16)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:281:7-281:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:438:7-438:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:652:10-652:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:443:7-443:15)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:167:9-167:19)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:286:7-286:16)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:448:7-448:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:175:10-175:11)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:291:7-291:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:461:7-461:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:466:7-466:16)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:296:7-296:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:471:7-471:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:476:7-476:16)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:481:7-481:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:486:7-486:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:491:7-491:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:105:10-105:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.03.cil.c:341:10-341:11)
[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
