/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint --conf conf/svcomp-yaml-validate.json --enable dbg.timing.enabled --set 'ana.activated[+]' apron --set ana.apron.domain polyhedra --witness.yaml.unassume /mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../results/st-cross-self2/ourtool.2023-02-15_09-12-33.files/ourtool/discover_list.yml/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../results/st-cross-self2/ourtool.2023-02-15_09-12-33.files/ourtool/discover_list.yml/witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/discover_list.c


--------------------------------------------------------------------------------


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Error][Imprecise][Unsound] Function definition missing for smp_send_req
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:424:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:424:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:424:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:425:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:425:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:425:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:426:5)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:426:5)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:426:5)
[Warning][Witness] couldn't locate invariant: 9 <= mnum_desc (../plain/discover_list.c:427:1)
[Warning][Witness] couldn't locate invariant: -9LL + (long long )mnum_desc >= 0LL (../plain/discover_list.c:427:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:427:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:427:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:427:1)
[Warning][Witness] couldn't locate invariant: mnum_desc != 0 (../plain/discover_list.c:427:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:428:5)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:428:5)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:428:5)
[Warning][Witness] couldn't locate invariant: 41 <= mnum_desc (../plain/discover_list.c:429:1)
[Warning][Witness] couldn't locate invariant: -41LL + (long long )mnum_desc >= 0LL (../plain/discover_list.c:429:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:429:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:429:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:429:1)
[Warning][Witness] couldn't locate invariant: mnum_desc != 0 (../plain/discover_list.c:429:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:430:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:430:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:430:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:431:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:431:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:431:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:432:4)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:432:4)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:432:4)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:433:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:433:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:433:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:434:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:434:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:434:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:435:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:435:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:435:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:436:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:436:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:436:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:437:4)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:437:4)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:437:4)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:439:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:439:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:439:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:441:4)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:441:4)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:441:4)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:443:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:443:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:443:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:445:5)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:445:5)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:445:5)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )i) + (long long )len >= 0LL (../plain/discover_list.c:197:1)
[Warning][Witness] couldn't locate invariant: ((60LL - (long long )a) - (long long )cpos) + (long long )i >= 0LL (../plain/discover_list.c:197:1)
[Warning][Witness] couldn't locate invariant: (175LL + (long long )bpos) - 3LL * (long long )cpos >= 0LL (../plain/discover_list.c:197:1)
[Warning][Witness] couldn't locate invariant: (long long )a >= 0LL (../plain/discover_list.c:197:1)
[Warning][Witness] couldn't locate invariant: 0 <= smp_rr.act_response_len (../plain/discover_list.c:445:5)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:447:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:447:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:447:1)
[Warning][Witness] couldn't locate invariant: 5 <= bpos (../plain/discover_list.c:198:1)
[Warning][Witness] couldn't locate invariant: bpos <= 2147483645 (../plain/discover_list.c:198:1)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )i) + (long long )len >= 0LL (../plain/discover_list.c:198:1)
[Warning][Witness] couldn't locate invariant: ((60LL - (long long )a) - (long long )cpos) + (long long )i >= 0LL (../plain/discover_list.c:198:1)
[Warning][Witness] couldn't locate invariant: (175LL + (long long )bpos) - 3LL * (long long )cpos >= 0LL (../plain/discover_list.c:198:1)
[Warning][Witness] couldn't locate invariant: (long long )a >= 0LL (../plain/discover_list.c:198:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:449:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:449:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:449:1)
[Warning][Witness] couldn't locate invariant: 8 <= bpos (../plain/discover_list.c:199:4)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )i) + (long long )len >= 0LL (../plain/discover_list.c:199:4)
[Warning][Witness] couldn't locate invariant: ((60LL - (long long )a) - (long long )cpos) + (long long )i >= 0LL (../plain/discover_list.c:199:4)
[Warning][Witness] couldn't locate invariant: (172LL + (long long )bpos) - 3LL * (long long )cpos >= 0LL (../plain/discover_list.c:199:4)
[Warning][Witness] couldn't locate invariant: (long long )a >= 0LL (../plain/discover_list.c:199:4)
[Warning][Witness] couldn't locate invariant: 0 <= len (../plain/discover_list.c:450:5)
[Warning][Witness] couldn't locate invariant: len <= 255 (../plain/discover_list.c:450:5)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:450:5)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:450:5)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:450:5)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )i) + (long long )len >= 0LL (../plain/discover_list.c:200:1)
[Warning][Witness] couldn't locate invariant: ((60LL - (long long )a) - (long long )cpos) + (long long )i >= 0LL (../plain/discover_list.c:200:1)
[Warning][Witness] couldn't locate invariant: 68LL - (long long )cpos >= 0LL (../plain/discover_list.c:200:1)
[Warning][Witness] couldn't locate invariant: (long long )a >= 0LL (../plain/discover_list.c:200:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:452:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:452:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:452:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:453:4)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:453:4)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:453:4)
[Warning][Witness] couldn't locate invariant: 8 <= bpos (../plain/discover_list.c:201:5)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )i) + (long long )len >= 0LL (../plain/discover_list.c:201:5)
[Warning][Witness] couldn't locate invariant: ((60LL - (long long )a) - (long long )cpos) + (long long )i >= 0LL (../plain/discover_list.c:201:5)
[Warning][Witness] couldn't locate invariant: (172LL + (long long )bpos) - 3LL * (long long )cpos >= 0LL (../plain/discover_list.c:201:5)
[Warning][Witness] couldn't locate invariant: (long long )a >= 0LL (../plain/discover_list.c:201:5)
[Warning][Witness] couldn't locate invariant: (long long )bpos >= 0LL (../plain/discover_list.c:201:5)
[Warning][Witness] couldn't locate invariant: bpos != 32 (../plain/discover_list.c:201:5)
[Warning][Witness] couldn't locate invariant: len <= -1 (../plain/discover_list.c:455:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:455:1)
[Warning][Witness] couldn't locate invariant: -1LL - (long long )len >= 0LL (../plain/discover_list.c:455:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:455:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:455:1)
[Warning][Witness] couldn't locate invariant: len != 0 (../plain/discover_list.c:455:1)
[Warning][Witness] couldn't locate invariant: 0 <= len (../plain/discover_list.c:459:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:459:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:459:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:459:1)
[Warning][Witness] couldn't locate invariant: 4 <= len (../plain/discover_list.c:460:4)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:460:4)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:460:4)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:460:4)
[Warning][Witness] couldn't locate invariant: 4 <= len (../plain/discover_list.c:462:4)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:462:4)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:462:4)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:462:4)
[Warning][Witness] couldn't locate invariant: 4 <= len (../plain/discover_list.c:463:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:463:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:463:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:463:1)
[Warning][Witness] couldn't locate invariant: 8 <= bpos (../plain/discover_list.c:202:5)
[Warning][Witness] couldn't locate invariant: bpos <= 2147483645 (../plain/discover_list.c:202:5)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )i) + (long long )len >= 0LL (../plain/discover_list.c:202:5)
[Warning][Witness] couldn't locate invariant: ((60LL - (long long )a) - (long long )cpos) + (long long )i >= 0LL (../plain/discover_list.c:202:5)
[Warning][Witness] couldn't locate invariant: (172LL + (long long )bpos) - 3LL * (long long )cpos >= 0LL (../plain/discover_list.c:202:5)
[Warning][Witness] couldn't locate invariant: (long long )a >= 0LL (../plain/discover_list.c:202:5)
[Warning][Witness] couldn't locate invariant: bpos != 32 (../plain/discover_list.c:202:5)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:466:4)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:466:4)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:466:4)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:467:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:467:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:467:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:468:4)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:468:4)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:468:4)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:469:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:469:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:469:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:470:4)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:470:4)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:470:4)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:472:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:472:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:472:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:474:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:474:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:474:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:476:4)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:476:4)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:476:4)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:478:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:478:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:478:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:480:4)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:480:4)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:480:4)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )i) + (long long )len >= 0LL (../plain/discover_list.c:203:4)
[Warning][Witness] couldn't locate invariant: ((60LL - (long long )a) - (long long )cpos) + (long long )i >= 0LL (../plain/discover_list.c:203:4)
[Warning][Witness] couldn't locate invariant: (172LL + (long long )bpos) - 3LL * (long long )cpos >= 0LL (../plain/discover_list.c:203:4)
[Warning][Witness] couldn't locate invariant: (long long )a >= 0LL (../plain/discover_list.c:203:4)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:482:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:482:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:482:1)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:484:4)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:484:4)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:484:4)
[Warning][Witness] couldn't locate invariant: 60 <= cpos (../plain/discover_list.c:204:3)
[Warning][Witness] couldn't locate invariant: cpos <= 75 (../plain/discover_list.c:204:3)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )i) + (long long )len >= 0LL (../plain/discover_list.c:204:3)
[Warning][Witness] couldn't locate invariant: ((60LL - (long long )a) - (long long )cpos) + (long long )i >= 0LL (../plain/discover_list.c:204:3)
[Warning][Witness] couldn't locate invariant: (172LL + (long long )bpos) - 3LL * (long long )cpos >= 0LL (../plain/discover_list.c:204:3)
[Warning][Witness] couldn't locate invariant: (long long )a >= 0LL (../plain/discover_list.c:204:3)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:486:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:486:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:486:1)
[Warning][Witness] couldn't locate invariant: 60 <= __tmpTR__int_1 (../plain/discover_list.c:204:3)
[Warning][Witness] couldn't locate invariant: __tmpTR__int_1 <= 75 (../plain/discover_list.c:204:3)
[Warning][Witness] couldn't locate invariant: (172LL - 3LL * (long long )__tmpTR__int_1) + (long long )bpos >= 0LL (../plain/discover_list.c:204:3)
[Warning][Witness] couldn't locate invariant: ((60LL - (long long )__tmpTR__int_1) - (long long )a) + (long long )i >= 0LL (../plain/discover_list.c:204:3)
[Warning][Witness] couldn't locate invariant: (-4LL - 4LL * (long long )dword_resp_len) + (long long )max_resp_len >= 0LL (../plain/discover_list.c:488:1)
[Warning][Witness] couldn't locate invariant: 255LL - (long long )dword_resp_len >= 0LL (../plain/discover_list.c:488:1)
[Warning][Witness] couldn't locate invariant: (12LL + 4LL * (long long )dword_resp_len) - (long long )max_resp_len >= 0LL (../plain/discover_list.c:488:1)
[Warning][Witness] couldn't locate invariant: (long long )__tmpTR__int_1 >= 0LL (../plain/discover_list.c:204:3)
[Warning][Witness] couldn't locate invariant: -128 <= ret (../plain/discover_list.c:497:1)
[Warning][Witness] couldn't locate invariant: -1 <= ret (../plain/discover_list.c:497:1)
[Warning][Witness] couldn't locate invariant: ret <= 255 (../plain/discover_list.c:497:1)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )cpos >= 0LL (../plain/discover_list.c:204:3)
[Warning][Witness] couldn't locate invariant: ((61LL - (long long )a) - (long long )cpos) + (long long )i >= 0LL (../plain/discover_list.c:204:3)
[Warning][Witness] couldn't locate invariant: 81LL - (long long )__tmpTR__int_1 >= 0LL (../plain/discover_list.c:204:3)
[Warning][Witness] couldn't locate invariant: 82LL - (long long )cpos >= 0LL (../plain/discover_list.c:204:3)
[Warning][Witness] couldn't locate invariant: (175LL + (long long )bpos) - 3LL * (long long )cpos >= 0LL (../plain/discover_list.c:204:3)
[Warning][Witness] couldn't locate invariant: 61 <= cpos (../plain/discover_list.c:211:4)
[Warning][Witness] couldn't locate invariant: cpos <= 76 (../plain/discover_list.c:211:4)
[Warning][Witness] couldn't locate invariant: k <= 2147483646 (../plain/discover_list.c:211:4)
[Warning][Witness] couldn't locate invariant: -1LL + (long long )cpos >= 0LL (../plain/discover_list.c:211:4)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )i) + (long long )len >= 0LL (../plain/discover_list.c:211:4)
[Warning][Witness] couldn't locate invariant: ((61LL - (long long )a) - (long long )cpos) + (long long )i >= 0LL (../plain/discover_list.c:211:4)
[Warning][Witness] couldn't locate invariant: 81LL - (long long )__tmpTR__int_1 >= 0LL (../plain/discover_list.c:211:4)
[Warning][Witness] couldn't locate invariant: 82LL - (long long )cpos >= 0LL (../plain/discover_list.c:211:4)
[Warning][Witness] couldn't locate invariant: (175LL + (long long )bpos) - 3LL * (long long )cpos >= 0LL (../plain/discover_list.c:211:4)
[Warning][Witness] couldn't locate invariant: (long long )__tmpTR__int_1 >= 0LL (../plain/discover_list.c:211:4)
[Warning][Witness] couldn't locate invariant: (long long )a >= 0LL (../plain/discover_list.c:211:4)
[Warning][Witness] couldn't locate invariant: -76LL + (long long )cpos >= 0LL (../plain/discover_list.c:213:1)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )i) + (long long )len >= 0LL (../plain/discover_list.c:213:1)
[Warning][Witness] couldn't locate invariant: ((61LL - (long long )a) - (long long )cpos) + (long long )i >= 0LL (../plain/discover_list.c:213:1)
[Warning][Witness] couldn't locate invariant: 81LL - (long long )__tmpTR__int_1 >= 0LL (../plain/discover_list.c:213:1)
[Warning][Witness] couldn't locate invariant: 82LL - (long long )cpos >= 0LL (../plain/discover_list.c:213:1)
[Warning][Witness] couldn't locate invariant: (175LL + (long long )bpos) - 3LL * (long long )cpos >= 0LL (../plain/discover_list.c:213:1)
[Warning][Witness] couldn't locate invariant: (long long )__tmpTR__int_1 >= 0LL (../plain/discover_list.c:213:1)
[Warning][Witness] couldn't locate invariant: (long long )a >= 0LL (../plain/discover_list.c:213:1)
[Warning][Witness] couldn't locate invariant: -76LL + (long long )cpos >= 0LL (../plain/discover_list.c:214:1)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )i) + (long long )len >= 0LL (../plain/discover_list.c:214:1)
[Warning][Witness] couldn't locate invariant: ((61LL - (long long )a) - (long long )cpos) + (long long )i >= 0LL (../plain/discover_list.c:214:1)
[Warning][Witness] couldn't locate invariant: 81LL - (long long )__tmpTR__int_1 >= 0LL (../plain/discover_list.c:214:1)
[Warning][Witness] couldn't locate invariant: 82LL - (long long )cpos >= 0LL (../plain/discover_list.c:214:1)
[Warning][Witness] couldn't locate invariant: (long long )__tmpTR__int_1 >= 0LL (../plain/discover_list.c:214:1)
[Warning][Witness] couldn't locate invariant: (long long )a >= 0LL (../plain/discover_list.c:214:1)
[Warning][Witness] couldn't locate invariant: 0 <= a (../plain/discover_list.c:215:1)
[Warning][Witness] couldn't locate invariant: (-15LL - (long long )a) + (long long )i >= 0LL (../plain/discover_list.c:215:1)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )i) + (long long )len >= 0LL (../plain/discover_list.c:215:1)
[Warning][Witness] couldn't locate invariant: 81LL - (long long )__tmpTR__int_1 >= 0LL (../plain/discover_list.c:215:1)
[Warning][Witness] couldn't locate invariant: (long long )__tmpTR__int_1 >= 0LL (../plain/discover_list.c:215:1)
[Warning][Witness] couldn't locate invariant: (long long )a >= 0LL (../plain/discover_list.c:215:1)
[Warning][Witness] couldn't locate invariant: 16 <= a (../plain/discover_list.c:216:1)
[Warning][Witness] couldn't locate invariant: -16LL + (long long )a >= 0LL (../plain/discover_list.c:216:1)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )i) + (long long )len >= 0LL (../plain/discover_list.c:216:1)
[Warning][Witness] couldn't locate invariant: (1LL - (long long )a) + (long long )i >= 0LL (../plain/discover_list.c:216:1)
[Warning][Witness] couldn't locate invariant: 81LL - (long long )__tmpTR__int_1 >= 0LL (../plain/discover_list.c:216:1)
[Warning][Witness] couldn't locate invariant: (long long )__tmpTR__int_1 >= 0LL (../plain/discover_list.c:216:1)
[Warning][Witness] couldn't locate invariant: 16 <= a (../plain/discover_list.c:217:1)
[Warning][Witness] couldn't locate invariant: -16LL + (long long )a >= 0LL (../plain/discover_list.c:217:1)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )i) + (long long )len >= 0LL (../plain/discover_list.c:217:1)
[Warning][Witness] couldn't locate invariant: (1LL - (long long )a) + (long long )i >= 0LL (../plain/discover_list.c:217:1)
[Warning][Witness] couldn't locate invariant: 81LL - (long long )__tmpTR__int_1 >= 0LL (../plain/discover_list.c:217:1)
[Warning][Witness] couldn't locate invariant: (long long )__tmpTR__int_1 >= 0LL (../plain/discover_list.c:217:1)
[Warning][Witness] couldn't locate invariant: -1 <= k (../plain/discover_list.c:218:5)
[Warning][Witness] couldn't locate invariant: k <= 2147483646 (../plain/discover_list.c:218:5)
[Warning][Witness] couldn't locate invariant: -16LL + (long long )a >= 0LL (../plain/discover_list.c:218:5)
[Warning][Witness] couldn't locate invariant: 1LL + (long long )k >= 0LL (../plain/discover_list.c:218:5)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )i) + (long long )len >= 0LL (../plain/discover_list.c:218:5)
[Warning][Witness] couldn't locate invariant: (1LL - (long long )a) + (long long )i >= 0LL (../plain/discover_list.c:218:5)
[Warning][Witness] couldn't locate invariant: 81LL - (long long )__tmpTR__int_1 >= 0LL (../plain/discover_list.c:218:5)
[Warning][Witness] couldn't locate invariant: (long long )__tmpTR__int_1 >= 0LL (../plain/discover_list.c:218:5)
[Warning][Witness] couldn't locate invariant: ((60LL - (long long )a) - (long long )cpos) + (long long )i >= 0LL (../plain/discover_list.c:222:1)
[Warning][Witness] couldn't locate invariant: (175LL + (long long )bpos) - 3LL * (long long )cpos >= 0LL (../plain/discover_list.c:222:1)
[Warning][Witness] couldn't locate invariant: (long long )i - (long long )len >= 0LL (../plain/discover_list.c:222:1)
[Warning][Witness] couldn't locate invariant: (long long )a >= 0LL (../plain/discover_list.c:222:1)
[Error][Witness] CIL couldn't parse invariant: 0 <= func_code (../plain/discover_list.c:164:4)
[Info][Witness] invariant has undefined variables or side effects: 0 <= func_code (../plain/discover_list.c:164:4)
../plain/discover_list.c:164: Error: Cannot resolve variable func_code.
[Error][Witness] CIL couldn't parse invariant: func_code <= 255 (../plain/discover_list.c:164:4)
[Info][Witness] invariant has undefined variables or side effects: func_code <= 255 (../plain/discover_list.c:164:4)
../plain/discover_list.c:164: Error: Cannot resolve variable func_code.
[Info][Unsound] Unknown address in {&opts} has escaped. (../plain/discover_list.c:496:5-496:91)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (../plain/discover_list.c:496:5-496:91)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (../plain/discover_list.c:424:1-424:21)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (../plain/discover_list.c:430:1-430:23)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (../plain/discover_list.c:431:1-431:31)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (../plain/discover_list.c:433:1-433:20)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (../plain/discover_list.c:434:1-434:34)
[Error][Imprecise][Unsound] Function definition missing for smp_send_req (../plain/discover_list.c:436:1-436:47)
[Info][Imprecise] INVALIDATING ALL GLOBALS! (../plain/discover_list.c:436:1-436:47)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(smp_def_rrlen_arr,
                                     NoOffset)), AddrOf(Var(__tmpTR__int_1, NoOffset)), CastE(TPtr(TComp(struct smp_target_obj, device_name : TArray(TInt(char, ), Some(Const(Int(256,int,256))), ), subvalue : TInt(int, ), sas_addr : TArray(TInt(unsigned char, ), Some(Const(Int(8,int,8))), ), interface_selector : TInt(int, ), opened : TInt(int, ), fd : TInt(int, ), ,  const  ), ), Lval(Var(top, NoOffset))), AddrOf(Var(smp_rr, NoOffset)), Lval(Mem(Lval(Var(op, NoOffset)), Field(verbose:TInt(int, ), NoOffset))) (../plain/discover_list.c:436:1-436:47)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(res,
                                     NoOffset)) (../plain/discover_list.c:436:1-436:47)
[Info][Witness] unassume invariant: func_code <= 255 && 0 <= func_code (../plain/discover_list.c:162:4-162:56)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:162:4-162:56)
[Info][Witness] unassume invariant: func_code <= 255 && 0 <= func_code (../plain/discover_list.c:162:4-162:56)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:459:1-459:20)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), PlusPI(StartOf(Var(buff, NoOffset)), Const(Int(1,int,1)))) (../plain/discover_list.c:193:1-193:33)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(k,
                                     NoOffset)) (../plain/discover_list.c:193:1-193:33)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:194:5-194:83)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:194:5-194:83)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (../plain/discover_list.c:194:5-194:83)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((((((((((len != 0 && (long long )a >= 0LL) && (175LL + (long long )bpos) - 3LL * (long long )cpos >= 0LL) && ((60LL - (long long )a) - (long long )cpos) + (long long )i >= 0LL) && k <= 2147483646) && bpos <= 2147483645) && cpos <= 75) && 60 <= cpos) && 5 <= bpos) && 4 <= len) && 0 <= i) && 0 <= a) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && -1LL + (long long )len >= 0LL) && k <= 2147483646) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && 1LL + (long long )k >= 0LL) && -1LL + (long long )len >= 0LL) && k <= 2147483646) && -1 <= k) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && -1LL + (long long )len >= 0LL) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && -1LL + (long long )len >= 0LL) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && -1LL + (long long )len >= 0LL) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && -1LL + (long long )len >= 0LL) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && 4 <= len) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL (../plain/discover_list.c:195:4-195:27)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:197:1-197:11)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (../plain/discover_list.c:197:1-197:11)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:198:1-198:10)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), AddrOf(Var(buff, Index(Lval(Var(bpos, NoOffset)), NoOffset)))) (../plain/discover_list.c:201:5-201:163)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(__tmpTR__int_1,
                                     NoOffset)) (../plain/discover_list.c:201:5-201:163)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:202:5-202:92)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:157:3-157:9)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:213:1-213:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:215:1-215:8)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TInt(char,
                                     ),  __restrict  ), PlusPI(StartOf(Var(buff, NoOffset)), Const(Int(1,int,1)))) (../plain/discover_list.c:217:1-217:33)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(k,
                                     NoOffset)) (../plain/discover_list.c:217:1-217:33)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:218:5-218:83)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (../plain/discover_list.c:218:5-218:83)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/discover_list.c:218:5-218:83)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((((((((((len != 0 && (long long )a >= 0LL) && (175LL + (long long )bpos) - 3LL * (long long )cpos >= 0LL) && ((60LL - (long long )a) - (long long )cpos) + (long long )i >= 0LL) && k <= 2147483646) && bpos <= 2147483645) && cpos <= 75) && 60 <= cpos) && 5 <= bpos) && 4 <= len) && 0 <= i) && 0 <= a) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && -1LL + (long long )len >= 0LL) && k <= 2147483646) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && 1LL + (long long )k >= 0LL) && -1LL + (long long )len >= 0LL) && k <= 2147483646) && -1 <= k) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && -1LL + (long long )len >= 0LL) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && -1LL + (long long )len >= 0LL) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && -1LL + (long long )len >= 0LL) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && -1LL + (long long )len >= 0LL) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && 4 <= len) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL) && (long long )c >= 0LL) && 255LL - (long long )c >= 0LL (../plain/discover_list.c:195:4-195:27)
[Warning][Deadcode] Function 'smp_is_naa5' is uncalled: 1 LLoC (../plain/discover_list.c:169:1-172:1)
[Warning][Deadcode] Function 'smp_get_num' is uncalled: 62 LLoC (../plain/discover_list.c:223:1-310:1)
[Warning][Deadcode] Function 'smp_get_llnum' is uncalled: 77 LLoC (../plain/discover_list.c:311:1-412:1)
[Warning][Deadcode] Function 'dStrHex' has dead code:
  on line 186 (../plain/discover_list.c:186-186)
  on line 191 (../plain/discover_list.c:191-191)
  on lines 207..209 (../plain/discover_list.c:207-209)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 91
  dead: 145 (140 in uncalled functions)
  total lines: 236
[Warning][Deadcode][CWE-571] condition 'dword_resp_len < 0x100' (possibly inserted by CIL) is always true (../plain/discover_list.c:423:1-423:62)
[Warning][Deadcode][CWE-570] condition 'len <= 0' is always false (../plain/discover_list.c:185:4-185:12)
[Warning][Deadcode][CWE-570] condition 'no_ascii < 0' is always false (../plain/discover_list.c:189:4-189:16)
[Warning][Deadcode][CWE-571] condition 'bpos >= 0' (possibly inserted by CIL) is always true (../plain/discover_list.c:201:5-201:163)
[Warning][Deadcode][CWE-571] condition 'bpos + 2 >= 0' (possibly inserted by CIL) is always true (../plain/discover_list.c:202:5-202:92)
[Warning][Deadcode][CWE-571] condition 'no_ascii' is always true (../plain/discover_list.c:203:4-203:12)
[Warning][Deadcode][CWE-571] condition '__tmpTR__int_1 >= 0' (possibly inserted by CIL) is always true (../plain/discover_list.c:204:3-204:166)
[Warning][Deadcode][CWE-571] condition '__tmpTR__int_1 < 82' is always true (../plain/discover_list.c:204:3-204:166)
[Success][Witness] invariant confirmed: 255LL - (long long )c >= 0LL (../plain/discover_list.c:175:11)
[Success][Witness] invariant confirmed: (long long )c >= 0LL (../plain/discover_list.c:175:11)
[Success][Witness] invariant confirmed: 255LL - (long long )c >= 0LL (../plain/discover_list.c:178:5)
[Success][Witness] invariant confirmed: (long long )c >= 0LL (../plain/discover_list.c:178:5)
[Success][Witness] invariant confirmed: 255LL - (long long )c >= 0LL (../plain/discover_list.c:179:11)
[Success][Witness] invariant confirmed: (long long )c >= 0LL (../plain/discover_list.c:179:11)
[Success][Witness] invariant confirmed: 255LL - (long long )c >= 0LL (../plain/discover_list.c:180:11)
[Success][Witness] invariant confirmed: (long long )c >= 0LL (../plain/discover_list.c:180:11)
[Success][Witness] invariant confirmed: 255LL - (long long )c >= 0LL (../plain/discover_list.c:181:5)
[Success][Witness] invariant confirmed: (long long )c >= 0LL (../plain/discover_list.c:181:5)
[Success][Witness] invariant confirmed: 255LL - (long long )c >= 0LL (../plain/discover_list.c:182:5)
[Success][Witness] invariant confirmed: (long long )c >= 0LL (../plain/discover_list.c:182:5)
[Success][Witness] invariant confirmed: 4 <= len (../plain/discover_list.c:185:4)
[Success][Witness] invariant confirmed: 255LL - (long long )c >= 0LL (../plain/discover_list.c:185:4)
[Success][Witness] invariant confirmed: (long long )c >= 0LL (../plain/discover_list.c:185:4)
[Success][Witness] invariant confirmed: -1LL + (long long )len >= 0LL (../plain/discover_list.c:187:1)
[Success][Witness] invariant confirmed: 255LL - (long long )c >= 0LL (../plain/discover_list.c:187:1)
[Success][Witness] invariant confirmed: (long long )c >= 0LL (../plain/discover_list.c:187:1)
[Success][Witness] invariant confirmed: -1LL + (long long )len >= 0LL (../plain/discover_list.c:188:1)
[Success][Witness] invariant confirmed: 255LL - (long long )c >= 0LL (../plain/discover_list.c:188:1)
[Success][Witness] invariant confirmed: (long long )c >= 0LL (../plain/discover_list.c:188:1)
[Success][Witness] invariant confirmed: -1LL + (long long )len >= 0LL (../plain/discover_list.c:189:4)
[Success][Witness] invariant confirmed: 255LL - (long long )c >= 0LL (../plain/discover_list.c:189:4)
[Success][Witness] invariant confirmed: (long long )c >= 0LL (../plain/discover_list.c:189:4)
[Success][Witness] invariant confirmed: -1LL + (long long )len >= 0LL (../plain/discover_list.c:193:1)
[Success][Witness] invariant confirmed: 255LL - (long long )c >= 0LL (../plain/discover_list.c:193:1)
[Success][Witness] invariant confirmed: (long long )c >= 0LL (../plain/discover_list.c:193:1)
[Warning][Witness] invariant unconfirmed: -1 <= k (../plain/discover_list.c:194:5)
[Success][Witness] invariant confirmed: k <= 2147483646 (../plain/discover_list.c:194:5)
[Success][Witness] invariant confirmed: -1LL + (long long )len >= 0LL (../plain/discover_list.c:194:5)
[Warning][Witness] invariant unconfirmed: 1LL + (long long )k >= 0LL (../plain/discover_list.c:194:5)
[Success][Witness] invariant confirmed: 255LL - (long long )c >= 0LL (../plain/discover_list.c:194:5)
[Success][Witness] invariant confirmed: (long long )c >= 0LL (../plain/discover_list.c:194:5)
../plain/discover_list.c:164: Error: Cannot resolve variable func_code.
../plain/discover_list.c:164: Error: Cannot resolve variable func_code.
[Success][Witness] invariant confirmed: 0 <= a (../plain/discover_list.c:195:4)
[Success][Witness] invariant confirmed: 0 <= i (../plain/discover_list.c:195:4)
[Success][Witness] invariant confirmed: 4 <= len (../plain/discover_list.c:195:4)
[Success][Witness] invariant confirmed: 5 <= bpos (../plain/discover_list.c:195:4)
[Success][Witness] invariant confirmed: 60 <= cpos (../plain/discover_list.c:195:4)
[Success][Witness] invariant confirmed: cpos <= 75 (../plain/discover_list.c:195:4)
[Success][Witness] invariant confirmed: bpos <= 2147483645 (../plain/discover_list.c:195:4)
[Success][Witness] invariant confirmed: k <= 2147483646 (../plain/discover_list.c:195:4)
[Success][Witness] invariant confirmed: ((60LL - (long long )a) - (long long )cpos) + (long long )i >= 0LL (../plain/discover_list.c:195:4)
[Warning][Witness] invariant unconfirmed: (175LL + (long long )bpos) - 3LL * (long long )cpos >= 0LL (../plain/discover_list.c:195:4)
[Success][Witness] invariant confirmed: (long long )a >= 0LL (../plain/discover_list.c:195:4)
[Success][Witness] invariant confirmed: len != 0 (../plain/discover_list.c:195:4)
[Success][Witness] invariant confirmed: 0 <= func_code (../plain/discover_list.c:162:4)
[Success][Witness] invariant confirmed: func_code <= 255 (../plain/discover_list.c:162:4)
[Info][Witness] witness validation summary:
  confirmed: 48
  unconfirmed: 3
  refuted: 0
  error: 303
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 354
SV-COMP result: unknown

vars = 335    evals = 689    narrow_reuses = 2

Timings:
                                  cputime   walltime   allocated   count
Default                            1.780s     1.781s   1097.64MB      1×
  preprocess                         0.023s     0.022s      0.01MB      1×
  FrontC                             0.006s     0.006s      5.73MB      4×
  Cabs2cil                           0.006s     0.006s      7.13MB      4×
  mergeCIL                           0.003s     0.003s      3.73MB      1×
  analysis                           1.738s     1.738s   1075.34MB      1×
    createCFG                          0.005s     0.005s      1.75MB      1×
      handle                             0.001s     0.001s      0.44MB     39×
      iter_connect                       0.002s     0.002s      1.12MB     39×
        computeSCCs                        0.001s     0.001s      0.81MB     40×
    FrontC                             0.002s     0.002s      0.76MB    106×
    Cabs2cil                           0.022s     0.022s     10.13MB    106×
    global_inits                       0.003s     0.003s      5.95MB      1×
    solving                            1.559s     1.559s    787.72MB      1×
      S.Dom.equal                        0.002s     0.003s      0.24MB    691×
      base unassume                      0.049s     0.049s     53.15MB     26×
      cheap_full_reach                   0.001s     0.001s      0.11MB      1×
      postsolver                         0.230s     0.230s    172.86MB      1×
        postsolver_iter                    0.230s     0.230s    172.63MB      1×
    warn_global                        0.001s     0.001s      0.83MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
