./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/transmitter.01.cil.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/transmitter.01.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.01.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.01.cil.c:60:5-67:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:93:3-103:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:201:3-239:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:404:3-441: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_st, t1_st, 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, tmp_ndt_1, tmp_ndt_2, __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.01.cil.c:22-22)
[Warning][Deadcode] Function 'fire_delta_events' has dead code:
  on line 251 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:251-251)
  on line 256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:256-256)
  on line 261 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:261-261)
[Warning][Deadcode] Function 'init_threads' has dead code:
  on line 164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:164-164)
  on line 169 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:169-169)
[Warning][Deadcode] Function 'reset_delta_events' has dead code:
  on line 274 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:274-274)
  on line 279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:279-279)
  on line 284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:284-284)
[Warning][Deadcode] Function 'reset_time_events' has dead code:
  on line 347 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:347-347)
  on line 352 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:352-352)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 135
  dead: 11
  total lines: 146
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:250:7-250:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:255:7-255:16)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:260:7-260:15)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:273:7-273:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:278:7-278:16)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:283:7-283:15)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:161:7-161:15)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:341:7-341:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:346:7-346:16)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:166:7-166:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:60:12-60:13)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:351:7-351:15)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:85:9-85:19)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:44:9-44:18)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:201:10-201:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:93:10-93:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:52:10-52:11)
[Warning][Deadcode][CWE-571] condition 'm_st == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:211:9-211:18)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:404:10-404:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:60:12-60:13)
[Warning][Deadcode][CWE-571] condition 'tmp == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:423:9-423:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:201:10-201:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:404:10-404:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:201:10-201:11)
[Warning][Deadcode][CWE-571] condition 'tmp == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.01.cil.c:423:9-423:17)
[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
