./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.13.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.13.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.13.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.13.cil.c:132:5-139:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:165:3-177:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:200:3-212:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:235:3-247:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:270:3-282:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:305:3-317:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:340:3-352:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:375:3-387:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:410:3-422:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:445:3-457:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:480:3-492:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:515:3-527:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:550:3-562:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:585:3-595:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1892:3-1929: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] 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.13.cil.c:22-22)
[Warning][Deadcode] Function 'fire_delta_events' has dead code:
  on line 1259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1259-1259)
  on line 1264 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1264-1264)
  on line 1269 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1269-1269)
  on line 1274 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1274-1274)
  on line 1279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1279-1279)
  on line 1284 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1284-1284)
  on line 1289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1289-1289)
  on line 1294 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1294-1294)
  on line 1299 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1299-1299)
  on line 1304 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1304-1304)
  on line 1309 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1309-1309)
  on line 1314 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1314-1314)
  on line 1319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1319-1319)
  on line 1324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1324-1324)
  on line 1329 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1329-1329)
  on line 1334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1334-1334)
  on line 1339 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1339-1339)
  on line 1344 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1344-1344)
  on line 1349 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1349-1349)
  on line 1354 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1354-1354)
  on line 1359 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1359-1359)
  on line 1364 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1364-1364)
  on line 1369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1369-1369)
  on line 1374 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1374-1374)
  on line 1379 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1379-1379)
  on line 1384 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1384-1384)
  on line 1389 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1389-1389)
[Warning][Deadcode] Function 'init_threads' has dead code:
  on line 884 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:884-884)
  on line 889 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:889-889)
  on line 894 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:894-894)
  on line 899 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:899-899)
  on line 904 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:904-904)
  on line 909 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:909-909)
  on line 914 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:914-914)
  on line 919 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:919-919)
  on line 924 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:924-924)
  on line 929 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:929-929)
  on line 934 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:934-934)
  on line 939 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:939-939)
  on line 944 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:944-944)
  on line 949 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:949-949)
[Warning][Deadcode] Function 'reset_delta_events' has dead code:
  on line 1402 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1402-1402)
  on line 1407 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1407-1407)
  on line 1412 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1412-1412)
  on line 1417 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1417-1417)
  on line 1422 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1422-1422)
  on line 1427 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1427-1427)
  on line 1432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1432-1432)
  on line 1437 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1437-1437)
  on line 1442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1442-1442)
  on line 1447 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1447-1447)
  on line 1452 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1452-1452)
  on line 1457 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1457-1457)
  on line 1462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1462-1462)
  on line 1467 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1467-1467)
  on line 1472 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1472-1472)
  on line 1477 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1477-1477)
  on line 1482 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1482-1482)
  on line 1487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1487-1487)
  on line 1492 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1492-1492)
  on line 1497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1497-1497)
  on line 1502 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1502-1502)
  on line 1507 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1507-1507)
  on line 1512 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1512-1512)
  on line 1517 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1517-1517)
  on line 1522 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1522-1522)
  on line 1527 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1527-1527)
  on line 1532 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1532-1532)
[Warning][Deadcode] Function 'reset_time_events' has dead code:
  on line 1703 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1703-1703)
  on line 1708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1708-1708)
  on line 1713 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1713-1713)
  on line 1718 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1718-1718)
  on line 1723 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1723-1723)
  on line 1728 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1728-1728)
  on line 1733 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1733-1733)
  on line 1738 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1738-1738)
  on line 1743 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1743-1743)
  on line 1748 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1748-1748)
  on line 1753 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1753-1753)
  on line 1758 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1758-1758)
  on line 1763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1763-1763)
  on line 1768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1768-1768)
  on line 1773 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1773-1773)
  on line 1778 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1778-1778)
  on line 1783 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1783-1783)
  on line 1788 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1788-1788)
  on line 1793 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1793-1793)
  on line 1798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1798-1798)
  on line 1803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1803-1803)
  on line 1808 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1808-1808)
  on line 1813 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1813-1813)
  on line 1818 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1818-1818)
  on line 1823 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1823-1823)
  on line 1828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1828-1828)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 555
  dead: 95
  total lines: 650
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:515:10-515:11)
[Warning][Deadcode][CWE-571] condition 't2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:192:9-192:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:200:10-200:11)
[Warning][Deadcode][CWE-571] condition 'M_E == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1697:7-1697:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1702:7-1702:16)
[Warning][Deadcode][CWE-571] condition 't12_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:542:9-542:20)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1707:7-1707:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1712:7-1712:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:550:10-550:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:410:10-410:11)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1717:7-1717:16)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1722:7-1722:16)
[Warning][Deadcode][CWE-570] condition 'M_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1258:7-1258:15)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1727:7-1727:16)
[Warning][Deadcode][CWE-570] condition 'T1_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1263:7-1263:16)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1732:7-1732:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1268:7-1268:16)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1737:7-1737:16)
[Warning][Deadcode][CWE-570] condition 'T3_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1273:7-1273:16)
[Warning][Deadcode][CWE-570] condition 'T9_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1742:7-1742:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1278:7-1278:16)
[Warning][Deadcode][CWE-571] condition 't9_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:437:9-437:19)
[Warning][Deadcode][CWE-570] condition 'T10_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1747:7-1747:17)
[Warning][Deadcode][CWE-570] condition 'T5_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1283:7-1283:16)
[Warning][Deadcode][CWE-571] condition 'm_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:881:7-881:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:445:10-445:11)
[Warning][Deadcode][CWE-570] condition 'T11_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1752:7-1752:17)
[Warning][Deadcode][CWE-570] condition 'T6_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1288:7-1288:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:305:10-305:11)
[Warning][Deadcode][CWE-570] condition 'T12_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1757:7-1757:17)
[Warning][Deadcode][CWE-570] condition 'T7_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1293:7-1293:16)
[Warning][Deadcode][CWE-571] condition 't1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:886:7-886:16)
[Warning][Deadcode][CWE-570] condition 'T13_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1762:7-1762:17)
[Warning][Deadcode][CWE-570] condition 'T8_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1298:7-1298:16)
[Warning][Deadcode][CWE-571] condition 't2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:891:7-891:16)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1767:7-1767:15)
[Warning][Deadcode][CWE-570] condition 'T9_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1303:7-1303:16)
[Warning][Deadcode][CWE-571] condition 'm_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:116:9-116:18)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1772:7-1772:15)
[Warning][Deadcode][CWE-570] condition 'T10_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1308:7-1308:17)
[Warning][Deadcode][CWE-571] condition 't3_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:896:7-896:16)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1777:7-1777:15)
[Warning][Deadcode][CWE-570] condition 'T11_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1313:7-1313:17)
[Warning][Deadcode][CWE-571] condition 't6_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:332:9-332:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:124:10-124:11)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1782:7-1782:15)
[Warning][Deadcode][CWE-570] condition 'T12_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1318:7-1318:17)
[Warning][Deadcode][CWE-571] condition 't4_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:901:7-901:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:340:10-340:11)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1787:7-1787:15)
[Warning][Deadcode][CWE-570] condition 'T13_E == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1323:7-1323:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:200:10-200:11)
[Warning][Deadcode][CWE-571] condition 't5_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:906:7-906:16)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1792:7-1792:15)
[Warning][Deadcode][CWE-570] condition 'E_1 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1328:7-1328:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:132:12-132:13)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1797:7-1797:15)
[Warning][Deadcode][CWE-570] condition 'E_2 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1333:7-1333:15)
[Warning][Deadcode][CWE-571] condition 't6_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:911:7-911:16)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1802:7-1802:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1338:7-1338:15)
[Warning][Deadcode][CWE-570] condition 'E_9 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1807:7-1807:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1343:7-1343:15)
[Warning][Deadcode][CWE-571] condition 't7_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:916:7-916:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:550:10-550:11)
[Warning][Deadcode][CWE-570] condition 'E_10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1812:7-1812:16)
[Warning][Deadcode][CWE-570] condition 'E_5 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1348:7-1348:15)
[Warning][Deadcode][CWE-571] condition 't8_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:921:7-921:16)
[Warning][Deadcode][CWE-571] condition 't3_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:227:9-227:19)
[Warning][Deadcode][CWE-570] condition 'E_11 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1817:7-1817:16)
[Warning][Deadcode][CWE-570] condition 'E_6 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1353:7-1353:15)
[Warning][Deadcode][CWE-570] condition 'E_12 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1822:7-1822:16)
[Warning][Deadcode][CWE-570] condition 'E_7 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1358:7-1358:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:235:10-235:11)
[Warning][Deadcode][CWE-571] condition 't9_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:926:7-926:16)
[Warning][Deadcode][CWE-570] condition 'E_13 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1827:7-1827:16)
[Warning][Deadcode][CWE-570] condition 'E_8 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1363:7-1363:15)
[Warning][Deadcode][CWE-570] condition 'E_9 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1368:7-1368:15)
[Warning][Deadcode][CWE-571] condition 't10_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:931:7-931:17)
[Warning][Deadcode][CWE-571] condition 't13_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:577:9-577:20)
[Warning][Deadcode][CWE-570] condition 'E_10 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1373:7-1373:16)
[Warning][Deadcode][CWE-571] condition 't11_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:936:7-936:17)
[Warning][Deadcode][CWE-570] condition 'E_11 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1378:7-1378:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:585:10-585:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:445:10-445:11)
[Warning][Deadcode][CWE-570] condition 'E_12 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1383:7-1383:16)
[Warning][Deadcode][CWE-571] condition 't12_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:941:7-941:17)
[Warning][Deadcode][CWE-570] condition 'E_13 == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1388:7-1388:16)
[Warning][Deadcode][CWE-571] condition 't13_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:946:7-946:17)
[Warning][Deadcode][CWE-570] condition 'M_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1401:7-1401:15)
[Warning][Deadcode][CWE-570] condition 'T1_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1406:7-1406:16)
[Warning][Deadcode][CWE-570] condition 'T2_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1411:7-1411:16)
[Warning][Deadcode][CWE-571] condition 't10_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:472:9-472:20)
[Warning][Deadcode][CWE-570] condition 'T3_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1416:7-1416:16)
[Warning][Deadcode][CWE-570] condition 'T4_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1421:7-1421:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:480:10-480:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:340:10-340:11)
[Warning][Deadcode][CWE-570] condition 'T5_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1426:7-1426:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1892:10-1892:11)
[Warning][Deadcode][CWE-570] condition 'T6_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1431:7-1431:16)
[Warning][Deadcode][CWE-570] condition 'T7_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1436:7-1436:16)
[Warning][Deadcode][CWE-570] condition 'T8_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1441:7-1441:16)
[Warning][Deadcode][CWE-570] condition 'T9_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1446:7-1446:16)
[Warning][Deadcode][CWE-570] condition 'T10_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1451:7-1451:17)
[Warning][Deadcode][CWE-571] condition 't7_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:367:9-367:19)
[Warning][Deadcode][CWE-570] condition 'T11_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1456:7-1456:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:375:10-375:11)
[Warning][Deadcode][CWE-570] condition 'T12_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1461:7-1461:17)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:235:10-235:11)
[Warning][Deadcode][CWE-570] condition 'T13_E == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1466:7-1466:17)
[Warning][Deadcode][CWE-570] condition 'E_1 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1471:7-1471:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1892:10-1892:11)
[Warning][Deadcode][CWE-570] condition 'E_2 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1476:7-1476:15)
[Warning][Deadcode][CWE-570] condition 'E_3 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1481:7-1481:15)
[Warning][Deadcode][CWE-570] condition 'E_4 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1486:7-1486:15)
[Warning][Deadcode][CWE-571] condition 't4_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:262:9-262:19)
[Warning][Deadcode][CWE-570] condition 'E_5 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1491:7-1491:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:270:10-270:11)
[Warning][Deadcode][CWE-570] condition 'E_6 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1496:7-1496:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:132:12-132:13)
[Warning][Deadcode][CWE-570] condition 'E_7 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1501:7-1501:15)
[Warning][Deadcode][CWE-570] condition 'E_8 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1506:7-1506:15)
[Warning][Deadcode][CWE-570] condition 'E_9 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1511:7-1511:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1041:10-1041:11)
[Warning][Deadcode][CWE-570] condition 'E_10 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1516:7-1516:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:480:10-480:11)
[Warning][Deadcode][CWE-570] condition 'E_11 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1521:7-1521:16)
[Warning][Deadcode][CWE-571] condition 't1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:157:9-157:19)
[Warning][Deadcode][CWE-570] condition 'E_12 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1526:7-1526:16)
[Warning][Deadcode][CWE-570] condition 'E_13 == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:1531:7-1531:16)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:165:10-165:11)
[Warning][Deadcode][CWE-571] condition 't11_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:507:9-507:20)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:515:10-515:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:375:10-375:11)
[Warning][Deadcode][CWE-571] condition 't8_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:402:9-402:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:410:10-410:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:270:10-270:11)
[Warning][Deadcode][CWE-571] condition 't5_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:297:9-297:19)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:305:10-305:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/transmitter.13.cil.c:165:10-165: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
