./goblint --conf conf/svcomp.json --set ana.malloc.unique_address_count 1 --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.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/mem_slave_tlm.1.cil.c:145:5-173:5 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:178:5-206:5 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:288:5-316:5 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:495:5-523:5 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:528:5-556:5 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:638:5-666:5 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:879:5-903:5 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1001:5-1025:5 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1119:3-1160:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1255:3-1344:3 with factor 2
[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] Setting "ana.int.interval" to true
[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 ! overflow) )
[Warning][Deadcode] Function 'error' has dead code:
  on line 21 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:21-21)
[Warning][Deadcode] Function 'm_run' has dead code:
  on line 216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:216-216)
  on line 224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:224-224)
  on line 232 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:232-232)
  on lines 239..240 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:239-240)
  on lines 247..248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:247-248)
  on lines 255..256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:255-256)
  on line 278 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:278-278)
  on line 326 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:326-326)
  on line 334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:334-334)
  on line 342 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:342-342)
  on lines 349..350 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:349-350)
  on lines 357..358 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:357-358)
  on lines 365..366 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:365-366)
  on line 380 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:380-380)
  on line 416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:416-416)
  on line 424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:424-424)
  on lines 431..432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:431-432)
  on lines 439..440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:439-440)
  on lines 447..448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:447-448)
  on line 462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:462-462)
  on line 470 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:470-470)
  on line 566 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:566-566)
  on line 574 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:574-574)
  on line 582 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:582-582)
  on line 590 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:590-590)
  on line 598 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:598-598)
  on line 606 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:606-606)
  on line 628 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:628-628)
  on line 676 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:676-676)
  on line 684 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:684-684)
  on line 692 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:692-692)
  on line 700 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:700-700)
  on line 708 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:708-708)
  on line 716 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:716-716)
  on line 730 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:730-730)
  on line 766 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:766-766)
  on line 774 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:774-774)
  on line 790 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:790-790)
  on line 798 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:798-798)
  on line 812 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:812-812)
  on line 820 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:820-820)
[Warning][Deadcode] Function 's_memory_read' has dead code:
  on line 69 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:69-69)
[Warning][Deadcode] Function 's_memory_write' has dead code:
  on line 79 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:79-79)
[Warning][Deadcode] Function 's_run' has dead code:
  on line 913 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:913-913)
  on line 929 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:929-929)
  on line 937 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:937-937)
  on line 953 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:953-953)
  on line 967 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:967-967)
  on line 975 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:975-975)
  on line 997 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:997-997)
  on line 1035 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1035-1035)
  on line 1043 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1043-1043)
  on line 1059 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1059-1059)
  on line 1067 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1067-1067)
  on line 1089 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1089-1089)
  on line 1097 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1097-1097)
[Warning][Deadcode] Function 'start_simulation' has dead code:
  on line 1175 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1175-1175)
  on line 1180 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1180-1180)
  on lines 1183..1184 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1183-1184)
  on lines 1191..1192 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1191-1192)
  on lines 1199..1200 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1199-1200)
  on lines 1207..1208 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1207-1208)
  on lines 1215..1216 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1215-1216)
  on lines 1223..1224 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1223-1224)
  on lines 1237..1238 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1237-1238)
  on lines 1245..1246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1245-1246)
  on line 1265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1265-1265)
  on line 1273 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1273-1273)
  on line 1281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1281-1281)
  on line 1289 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1289-1289)
  on line 1297 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1297-1297)
  on line 1305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1305-1305)
  on line 1319 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1319-1319)
  on line 1327 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1327-1327)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 450
  dead: 92
  total lines: 542
[Warning][Deadcode][CWE-571] condition 'c_write_req_ev == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:269:11-269:36)
[Warning][Deadcode][CWE-570] condition 'c_write_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1304:21-1304:46)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:879:12-879:13)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:145:12-145:13)
[Warning][Deadcode][CWE-570] condition 'c_write_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:423:15-423:40)
[Warning][Deadcode][CWE-570] condition 'c_write_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1318:11-1318:36)
[Warning][Deadcode][CWE-570] condition 'c_read_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:277:13-277:37)
[Warning][Deadcode][CWE-570] condition 'm_run_pc == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:430:15-430:34)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1001:12-1001:13)
[Warning][Deadcode][CWE-570] condition 'c_read_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1326:13-1326:37)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:288:12-288:13)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:528:12-528:13)
[Warning][Deadcode][CWE-570] condition 'm_run_st == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1335:9-1335:28)
[Warning][Deadcode][CWE-570] condition 'm_run_pc == 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:438:17-438:36)
[Warning][Deadcode][CWE-570] condition 's_run_st == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1338:11-1338:30)
[Warning][Deadcode][CWE-570] condition 'm_run_pc == 6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:446:19-446:38)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1119:10-1119:11)
[Warning][Deadcode][CWE-570] condition 'c_write_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:461:11-461:36)
[Warning][Deadcode][CWE-570] condition 'c_m_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:675:11-675:28)
[Warning][Deadcode][CWE-570] condition 'c_read_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:469:13-469:37)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:879:12-879:13)
[Warning][Deadcode][CWE-570] condition 'c_read_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:683:13-683:37)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:178:12-178:13)
[Warning][Deadcode][CWE-570] condition 'c_write_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:691:15-691:40)
[Warning][Deadcode][CWE-570] condition 'c_m_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1034:11-1034:28)
[Warning][Deadcode][CWE-570] condition 'c_m_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:699:17-699:34)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:485:10-485:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:288:12-288:13)
[Warning][Deadcode][CWE-570] condition 'c_read_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1042:13-1042:37)
[Warning][Deadcode][CWE-570] condition 'c_read_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:707:19-707:43)
[Warning][Deadcode][CWE-571] condition 'm_run_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1172:7-1172:25)
[Warning][Deadcode][CWE-570] condition 'c_m_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:565:11-565:28)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:495:12-495:13)
[Warning][Deadcode][CWE-571] condition 'c_write_rsp_ev == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1050:15-1050:40)
[Warning][Deadcode][CWE-570] condition 'c_write_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:715:21-715:46)
[Warning][Deadcode][CWE-571] condition 's_run_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1177:7-1177:25)
[Warning][Deadcode][CWE-570] condition 'c_read_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:573:13-573:37)
[Warning][Deadcode][CWE-570] condition 'c_write_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:729:11-729:36)
[Warning][Deadcode][CWE-570] condition 'c_m_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1058:17-1058:34)
[Warning][Deadcode][CWE-570] condition 'm_run_pc == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1182:7-1182:26)
[Warning][Deadcode][CWE-570] condition 'c_write_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:581:15-581:40)
[Warning][Deadcode][CWE-571] condition 'c_read_rsp_ev == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:737:13-737:37)
[Warning][Deadcode][CWE-570] condition 'c_read_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1066:19-1066:43)
[Warning][Deadcode][CWE-570] condition 'c_m_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:912:11-912:28)
[Warning][Deadcode][CWE-571] condition 'i == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:66:7-66:11)
[Warning][Deadcode][CWE-570] condition 'm_run_pc == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1190:9-1190:28)
[Warning][Deadcode][CWE-570] condition 'c_m_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:589:17-589:34)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:178:12-178:13)
[Warning][Deadcode][CWE-571] condition 'c_write_rsp_ev == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1074:21-1074:46)
[Warning][Deadcode][CWE-571] condition 'c_read_req_ev == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:920:13-920:37)
[Warning][Deadcode][CWE-571] condition 'i == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:76:7-76:11)
[Warning][Deadcode][CWE-570] condition 'm_run_pc == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1198:11-1198:30)
[Warning][Deadcode][CWE-570] condition 'c_read_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:597:19-597:43)
[Warning][Deadcode][CWE-570] condition 'c_write_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1088:11-1088:36)
[Warning][Deadcode][CWE-570] condition 'c_write_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:928:15-928:40)
[Warning][Deadcode][CWE-571] condition 'c_m_ev == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:757:11-757:28)
[Warning][Deadcode][CWE-570] condition 'm_run_pc == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1206:13-1206:32)
[Warning][Deadcode][CWE-570] condition 'c_write_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:605:21-605:46)
[Warning][Deadcode][CWE-570] condition 'c_read_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1096:13-1096:37)
[Warning][Deadcode][CWE-570] condition 'c_m_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:936:17-936:34)
[Warning][Deadcode][CWE-570] condition 'c_read_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:765:13-765:37)
[Warning][Deadcode][CWE-571] condition 'c_write_req_ev == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:619:11-619:36)
[Warning][Deadcode][CWE-570] condition 'c_m_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:325:11-325:28)
[Warning][Deadcode][CWE-570] condition 'm_run_pc == 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1214:15-1214:34)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:495:12-495:13)
[Warning][Deadcode][CWE-571] condition 'c_read_req_ev == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:944:19-944:43)
[Warning][Deadcode][CWE-570] condition 'c_write_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:773:15-773:40)
[Warning][Deadcode][CWE-570] condition 'c_read_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:627:13-627:37)
[Warning][Deadcode][CWE-570] condition 'c_read_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:333:13-333:37)
[Warning][Deadcode][CWE-570] condition 'm_run_pc == 6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1222:17-1222:36)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1119:10-1119:11)
[Warning][Deadcode][CWE-571] condition 'm_run_pc == 6' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:120:19-120:38)
[Warning][Deadcode][CWE-570] condition 'c_write_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:952:21-952:46)
[Warning][Deadcode][CWE-570] condition 's_run_pc == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1236:7-1236:26)
[Warning][Deadcode][CWE-571] condition 'm_run_st == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1121:9-1121:28)
[Warning][Deadcode][CWE-571] condition 'c_m_ev == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:781:17-781:34)
[Warning][Deadcode][CWE-570] condition 'c_write_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:341:15-341:40)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:638:12-638:13)
[Warning][Deadcode][CWE-571] condition 'm_run_st == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1130:9-1130:28)
[Warning][Deadcode][CWE-570] condition 'c_write_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:966:11-966:36)
[Warning][Deadcode][CWE-570] condition 'm_run_pc == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:348:15-348:34)
[Warning][Deadcode][CWE-570] condition 's_run_pc == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1244:9-1244:28)
[Warning][Deadcode][CWE-570] condition 'c_read_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:789:19-789:43)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:134:10-134:11)
[Warning][Deadcode][CWE-570] condition 'c_read_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:974:13-974:37)
[Warning][Deadcode][CWE-570] condition 'm_run_pc == 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:356:17-356:36)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1255:10-1255:11)
[Warning][Deadcode][CWE-571] condition 's_run_st == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1145:9-1145:28)
[Warning][Deadcode][CWE-570] condition 'c_write_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:797:21-797:46)
[Warning][Deadcode][CWE-570] condition 'c_m_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:215:11-215:28)
[Warning][Deadcode][CWE-570] condition 'c_write_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:811:11-811:36)
[Warning][Deadcode][CWE-570] condition 'm_run_pc == 6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:364:19-364:38)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:145:12-145:13)
[Warning][Deadcode][CWE-570] condition 'c_m_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1264:11-1264:28)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1119:10-1119:11)
[Warning][Deadcode][CWE-571] condition 'req_type == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:991:11-991:30)
[Warning][Deadcode][CWE-570] condition 'c_read_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:223:13-223:37)
[Warning][Deadcode][CWE-570] condition 'c_read_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:819:13-819:37)
[Warning][Deadcode][CWE-570] condition 'c_write_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:379:11-379:36)
[Warning][Deadcode][CWE-570] condition 'c_read_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1272:13-1272:37)
[Warning][Deadcode][CWE-570] condition 'c_write_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:231:15-231:40)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:528:12-528:13)
[Warning][Deadcode][CWE-571] condition 'c_read_rsp_ev == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:387:13-387:37)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1001:12-1001:13)
[Warning][Deadcode][CWE-570] condition 'm_run_pc == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:238:15-238:34)
[Warning][Deadcode][CWE-570] condition 'c_write_rsp_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1280:15-1280:40)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:638:12-638:13)
[Warning][Deadcode][CWE-570] condition 'm_run_pc == 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:246:17-246:36)
[Warning][Deadcode][CWE-570] condition 'c_m_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1288:17-1288:34)
[Warning][Deadcode][CWE-571] condition 's_run_pc == 2' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:867:11-867:30)
[Warning][Deadcode][CWE-571] condition 'c_m_ev == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:407:11-407:28)
[Warning][Deadcode][CWE-570] condition 'm_run_pc == 6' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:254:19-254:38)
[Warning][Deadcode][CWE-570] condition 'c_read_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1296:19-1296:43)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:1119:10-1119:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:876:10-876:11)
[Warning][Deadcode][CWE-570] condition 'c_read_req_ev == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/mem_slave_tlm.1.cil.c:415:13-415:37)
SV-COMP result: true
[Info][Witness] witness generation summary:
  total generation entries: 1
