./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/toy1.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/toy1.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/toy1.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/toy1.cil.c:87:3-138:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:160:3-183:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:205:3-228:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:250:3-260:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:306:3-404:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:553:3-693: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] e_g, e_f, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, __retres1, tmp, tmp___0, tmp___1, tmp___2, tmp___3, t
[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][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:168:7-168:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:213:7-213:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:119:9-119:19)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:122:11-122:21)
[Warning][Deadcode] Function 'error' has dead code:
  on line 24 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:24-24)
[Warning][Deadcode] Function 'read' has dead code:
  on line 275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:275-275)
[Warning][Deadcode] Function 'start_simulation' has dead code:
  on lines 417..419 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:417-419)
  on line 423 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:423-423)
  on line 430 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:430-430)
  on line 435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:435-435)
  on line 440 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:440-440)
  on line 445 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:445-445)
  on line 448 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:448-448)
  on line 453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:453-453)
  on line 458 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:458-458)
  on line 463 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:463-463)
  on line 468 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:468-468)
  on line 473 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:473-473)
  on lines 478..479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:478-479)
  on lines 486..487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:486-487)
  on lines 496..497 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:496-497)
  on lines 505..506 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:505-506)
  on lines 514..515 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:514-515)
  on line 523 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:523-523)
  on line 528 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:528-528)
  on line 533 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:533-533)
  on line 538 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:538-538)
  on line 543 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:543-543)
  on line 548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:548-548)
  on line 573 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:573-573)
  on line 578 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:578-578)
  on line 583 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:583-583)
  on line 607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:607-607)
  on line 617 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:617-617)
  on line 626 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:626-626)
  on line 635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:635-635)
  on line 648 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:648-648)
  on line 653 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:653-653)
  on line 658 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:658-658)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 208
  dead: 42
  total lines: 250
[Warning][Deadcode][CWE-570] condition 'e_e == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:606:13-606:27)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:250:10-250:11)
[Warning][Deadcode][CWE-570] condition 'e_f == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:616:11-616:25)
[Warning][Deadcode][CWE-570] condition 'c_req_up == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:416:7-416:26)
[Warning][Deadcode][CWE-571] condition 'c1_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:152:9-152:25)
[Warning][Deadcode][CWE-570] condition 'e_f == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:625:11-625:25)
[Warning][Deadcode][CWE-571] condition 'wl_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:427:7-427:22)
[Warning][Deadcode][CWE-570] condition 'e_g == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:634:11-634:25)
[Warning][Deadcode][CWE-571] condition 'c1_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:432:7-432:22)
[Warning][Deadcode][CWE-570] condition 'e_e == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:647:9-647:23)
[Warning][Deadcode][CWE-570] condition 'e_f == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:652:9-652:23)
[Warning][Deadcode][CWE-571] condition 'c2_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:437:7-437:22)
[Warning][Deadcode][CWE-570] condition 'e_wl == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:274:9-274:24)
[Warning][Deadcode][CWE-570] condition 'e_g == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:657:9-657:23)
[Warning][Deadcode][CWE-571] condition 'wb_i == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:442:7-442:22)
[Warning][Deadcode][CWE-571] condition 'e_e == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:282:11-282:25)
[Warning][Deadcode][CWE-570] condition 'r_i == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:447:7-447:21)
[Warning][Deadcode][CWE-570] condition 'c1_st == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:675:11-675:27)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:306:10-306:11)
[Warning][Deadcode][CWE-570] condition 'c2_st == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:678:13-678:29)
[Warning][Deadcode][CWE-570] condition 'wb_st == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:681:15-681:31)
[Warning][Deadcode][CWE-570] condition 'e_f == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:452:7-452:21)
[Warning][Deadcode][CWE-570] condition 'c1_st == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:311:11-311:27)
[Warning][Deadcode][CWE-570] condition 'e_g == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:457:7-457:21)
[Warning][Deadcode][CWE-570] condition 'c2_st == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:314:13-314:29)
[Warning][Deadcode][CWE-570] condition 'wb_st == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:317:15-317:31)
[Warning][Deadcode][CWE-570] condition 'e_e == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:462:7-462:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:553:10-553:11)
[Warning][Deadcode][CWE-570] condition 'e_c == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:467:7-467:21)
[Warning][Deadcode][CWE-570] condition 'e_wl == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:472:7-472:22)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:205:10-205:11)
[Warning][Deadcode][CWE-570] condition 'wl_pc == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:477:7-477:23)
[Warning][Deadcode][CWE-570] condition 'wl_pc == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:485:9-485:25)
[Warning][Deadcode][CWE-571] condition 'wl_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:72:11-72:27)
[Warning][Deadcode][CWE-570] condition 'e_f == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:572:9-572:23)
[Warning][Deadcode][CWE-571] condition 'e_g == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:216:13-216:27)
[Warning][Deadcode][CWE-570] condition 'c1_pc == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:495:7-495:23)
[Warning][Deadcode][CWE-570] condition 'e_g == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:577:9-577:23)
[Warning][Deadcode][CWE-570] condition 'e_e == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:582:9-582:23)
[Warning][Deadcode][CWE-570] condition 'c2_pc == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:504:7-504:23)
[Warning][Deadcode][CWE-570] condition 'wb_pc == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:513:7-513:23)
[Warning][Deadcode][CWE-571] condition 'wb_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:242:9-242:25)
[Warning][Deadcode][CWE-570] condition 'e_c == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:522:7-522:21)
[Warning][Deadcode][CWE-570] condition 'e_e == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:527:7-527:21)
[Warning][Deadcode][CWE-570] condition 'e_f == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:532:7-532:21)
[Warning][Deadcode][CWE-570] condition 'e_e == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:606:13-606:27)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:160:10-160:11)
[Warning][Deadcode][CWE-570] condition 'e_g == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:537:7-537:21)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:306:10-306:11)
[Warning][Deadcode][CWE-570] condition 'e_f == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:616:11-616:25)
[Warning][Deadcode][CWE-570] condition 'e_c == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:542:7-542:21)
[Warning][Deadcode][CWE-570] condition 'e_f == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:625:11-625:25)
[Warning][Deadcode][CWE-570] condition 'e_wl == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:547:7-547:22)
[Warning][Deadcode][CWE-570] condition 'e_g == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:634:11-634:25)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:553:10-553:11)
[Warning][Deadcode][CWE-571] condition 'e_g == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:171:13-171:27)
[Warning][Deadcode][CWE-570] condition 'e_e == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:647:9-647:23)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:87:10-87:11)
[Warning][Deadcode][CWE-570] condition 'e_f == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:652:9-652:23)
[Warning][Deadcode][CWE-571] condition 'c2_pc == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:197:9-197:25)
[Warning][Deadcode][CWE-570] condition 'e_g == 1' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:657:9-657:23)
[Warning][Deadcode][CWE-571] condition 'e_f == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:94:11-94:25)
[Warning][Deadcode][CWE-570] condition 'e_f == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:572:9-572:23)
[Warning][Deadcode][CWE-570] condition 'e_g == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:577:9-577:23)
[Warning][Deadcode][CWE-571] condition 'e_f == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:103:11-103:25)
[Warning][Deadcode][CWE-570] condition 'c1_st == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:675:11-675:27)
[Warning][Deadcode][CWE-570] condition 'e_e == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:582:9-582:23)
[Warning][Deadcode][CWE-570] condition 'c2_st == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:678:13-678:29)
[Warning][Deadcode][CWE-570] condition 'wb_st == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/systemc/toy1.cil.c:681:15-681:31)
[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
