/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/id_build.i.p+nlh-reducer.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/id_build.i.p+nlh-reducer.yml/witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/id_build.i.p+nlh-reducer.c


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Warning][Witness] couldn't locate invariant: 4 <= main__i (../plain/id_build.i.p+nlh-reducer.c:1775:2)
[Warning][Witness] couldn't locate invariant: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1775:2)
[Warning][Witness] couldn't locate invariant: (-40LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1775:2)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1775:2)
[Warning][Witness] couldn't locate invariant: 7LL - (long long )main__j >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1775:2)
[Warning][Witness] couldn't locate invariant: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1775:2)
[Warning][Witness] couldn't locate invariant: main__i != 0 (../plain/id_build.i.p+nlh-reducer.c:1775:2)
[Warning][Witness] couldn't locate invariant: (-40LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1777:2)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1777:2)
[Warning][Witness] couldn't locate invariant: 7LL - (long long )main__j >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1777:2)
[Warning][Witness] couldn't locate invariant: (-40LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1778:6)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1778:6)
[Warning][Witness] couldn't locate invariant: 7LL - (long long )main__j >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1778:6)
[Warning][Witness] couldn't locate invariant: 4 <= main__i (../plain/id_build.i.p+nlh-reducer.c:1791:2)
[Warning][Witness] couldn't locate invariant: -4LL + (long long )main__i >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1791:2)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1791:2)
[Warning][Witness] couldn't locate invariant: main__i != 0 (../plain/id_build.i.p+nlh-reducer.c:1791:2)
[Warning][Witness] couldn't locate invariant: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1792:6)
[Warning][Witness] couldn't locate invariant: 5 <= main__i (../plain/id_build.i.p+nlh-reducer.c:1792:6)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__i >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1792:6)
[Warning][Witness] couldn't locate invariant: (0LL - (long long )main__i) + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1792:6)
[Warning][Witness] couldn't locate invariant: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1792:6)
[Warning][Witness] couldn't locate invariant: main__i != 1 (../plain/id_build.i.p+nlh-reducer.c:1792:6)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__i >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1794:2)
[Warning][Witness] couldn't locate invariant: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1794:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__i >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1799:3)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__i >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1800:2)
[Warning][Witness] couldn't locate invariant: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1811:2)
[Warning][Witness] couldn't locate invariant: 4 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1812:6)
[Warning][Witness] couldn't locate invariant: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1812:6)
[Warning][Witness] couldn't locate invariant: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1812:6)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1814:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1815:6)
[Warning][Witness] couldn't locate invariant: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1819:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1819:2)
[Warning][Witness] couldn't locate invariant: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1819:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1821:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1822:6)
[Warning][Witness] couldn't locate invariant: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1830:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1830:2)
[Warning][Witness] couldn't locate invariant: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1830:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1832:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1833:6)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1839:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1840:6)
[Warning][Witness] couldn't locate invariant: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1844:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1844:2)
[Warning][Witness] couldn't locate invariant: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1844:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1846:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1847:6)
[Warning][Witness] couldn't locate invariant: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1855:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1855:2)
[Warning][Witness] couldn't locate invariant: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1855:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1857:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1858:6)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1864:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1865:6)
[Warning][Witness] couldn't locate invariant: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1869:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1869:2)
[Warning][Witness] couldn't locate invariant: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1869:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1871:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1872:6)
[Warning][Witness] couldn't locate invariant: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1880:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1880:2)
[Warning][Witness] couldn't locate invariant: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1880:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1882:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1883:6)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1889:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1890:6)
[Warning][Witness] couldn't locate invariant: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1894:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1894:2)
[Warning][Witness] couldn't locate invariant: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1894:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1896:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1897:6)
[Warning][Witness] couldn't locate invariant: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1905:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1905:2)
[Warning][Witness] couldn't locate invariant: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1905:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1907:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1908:6)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1914:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1915:6)
[Warning][Witness] couldn't locate invariant: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1919:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1919:2)
[Warning][Witness] couldn't locate invariant: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1919:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1921:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1922:6)
[Warning][Witness] couldn't locate invariant: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1930:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1930:2)
[Warning][Witness] couldn't locate invariant: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1930:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1932:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1933:6)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1939:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1940:6)
[Warning][Witness] couldn't locate invariant: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1944:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1944:2)
[Warning][Witness] couldn't locate invariant: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1944:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1946:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1947:6)
[Warning][Witness] couldn't locate invariant: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1955:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1955:2)
[Warning][Witness] couldn't locate invariant: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1955:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1957:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1958:6)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1964:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1965:6)
[Warning][Witness] couldn't locate invariant: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1969:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1969:2)
[Warning][Witness] couldn't locate invariant: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1969:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1971:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1972:6)
[Warning][Witness] couldn't locate invariant: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1980:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1980:2)
[Warning][Witness] couldn't locate invariant: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1980:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1982:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1983:6)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1989:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1990:6)
[Warning][Witness] couldn't locate invariant: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1994:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1994:2)
[Warning][Witness] couldn't locate invariant: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1994:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1996:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1997:6)
[Warning][Witness] couldn't locate invariant: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:2005:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:2005:2)
[Warning][Witness] couldn't locate invariant: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:2005:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:2007:2)
[Warning][Witness] couldn't locate invariant: -5LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:2008:6)
[Warning][Witness] couldn't locate invariant: 0LL - (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:2690:2)

runtime: 00:00:10.464
vars: 103, evals: 76

|rho|=103
|called|=3
|stable|=103
|infl|=98
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=76
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=415.09MB, max=24.36MB, minor=407.09MB, major=54.33MB, promoted=46.33MB
    minor collections=291  major collections=24 compactions=0


runtime: 00:00:20.533
vars: 283, evals: 234

|rho|=283
|called|=4
|stable|=283
|infl|=277
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=234
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=468.41MB, max=24.36MB, minor=459.99MB, major=56.64MB, promoted=48.21MB
    minor collections=393  major collections=37 compactions=0


runtime: 00:00:30.553
vars: 455, evals: 386

|rho|=455
|called|=3
|stable|=455
|infl|=450
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=386
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=537.43MB, max=24.36MB, minor=528.62MB, major=58.95MB, promoted=50.15MB
    minor collections=490  major collections=49 compactions=0


runtime: 00:00:40.640
vars: 626, evals: 538

|rho|=626
|called|=6
|stable|=626
|infl|=618
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=538
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=620.86MB, max=24.36MB, minor=611.66MB, major=61.45MB, promoted=52.24MB
    minor collections=593  major collections=59 compactions=0


runtime: 00:00:50.696
vars: 698, evals: 592

|rho|=698
|called|=2
|stable|=698
|infl|=694
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=592
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=720.15MB, max=24.36MB, minor=710.59MB, major=63.96MB, promoted=54.40MB
    minor collections=692  major collections=70 compactions=0


runtime: 00:01:00.710
vars: 892, evals: 767

|rho|=892
|called|=37
|stable|=892
|infl|=854
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=767
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=846.59MB, max=24.36MB, minor=836.71MB, major=66.70MB, promoted=56.82MB
    minor collections=793  major collections=77 compactions=0


runtime: 00:01:10.799
vars: 902, evals: 767

|rho|=902
|called|=11
|stable|=902
|infl|=890
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=767
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=966.10MB, max=24.36MB, minor=955.99MB, major=70.05MB, promoted=59.93MB
    minor collections=891  major collections=83 compactions=0


runtime: 00:01:20.760
vars: 904, evals: 783

|rho|=904
|called|=9
|stable|=904
|infl|=894
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=767
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=1154.37MB, max=24.36MB, minor=1143.90MB, major=75.40MB, promoted=64.93MB
    minor collections=1055  major collections=95 compactions=0


runtime: 00:01:30.824
vars: 905, evals: 798

|rho|=905
|called|=11
|stable|=905
|infl|=900
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=767
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=1317.36MB, max=24.36MB, minor=1306.66MB, major=79.61MB, promoted=68.91MB
    minor collections=1189  major collections=104 compactions=0


runtime: 00:01:40.805
vars: 933, evals: 829

|rho|=933
|called|=2
|stable|=933
|infl|=929
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=794
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=1559.79MB, max=24.36MB, minor=1548.67MB, major=85.28MB, promoted=74.15MB
    minor collections=1421  major collections=118 compactions=0


runtime: 00:01:50.843
vars: 971, evals: 867

|rho|=973
|called|=0
|stable|=973
|infl|=969
|wpoint|=0
|side_dep|=19
|side_infl|=28
|var_messages|=0
|rho_write|=26
|dep|=832
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=1722.94MB, max=24.36MB, minor=1710.93MB, major=90.08MB, promoted=78.07MB
    minor collections=1611  major collections=130 compactions=0


runtime: 00:02:01.036
vars: 971, evals: 867

|rho|=973
|called|=0
|stable|=973
|infl|=969
|wpoint|=0
|side_dep|=36
|side_infl|=56
|var_messages|=0
|rho_write|=54
|dep|=832
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=1768.63MB, max=24.36MB, minor=1755.75MB, major=93.98MB, promoted=81.10MB
    minor collections=1730  major collections=139 compactions=0


runtime: 00:02:11.027
vars: 971, evals: 867

|rho|=973
|called|=0
|stable|=973
|infl|=969
|wpoint|=0
|side_dep|=51
|side_infl|=81
|var_messages|=0
|rho_write|=79
|dep|=832
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=1818.87MB, max=24.36MB, minor=1805.23MB, major=97.39MB, promoted=83.75MB
    minor collections=1830  major collections=148 compactions=0


runtime: 00:02:21.081
vars: 971, evals: 867

|rho|=973
|called|=0
|stable|=973
|infl|=969
|wpoint|=0
|side_dep|=67
|side_infl|=107
|var_messages|=0
|rho_write|=105
|dep|=832
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=1879.55MB, max=24.36MB, minor=1865.19MB, major=100.71MB, promoted=86.35MB
    minor collections=1927  major collections=156 compactions=0


runtime: 00:02:31.162
vars: 971, evals: 867

|rho|=973
|called|=0
|stable|=973
|infl|=969
|wpoint|=0
|side_dep|=80
|side_infl|=128
|var_messages|=0
|rho_write|=126
|dep|=832
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=1947.60MB, max=24.36MB, minor=1932.57MB, major=103.94MB, promoted=88.91MB
    minor collections=2026  major collections=164 compactions=0


runtime: 00:02:41.291
vars: 971, evals: 867

|rho|=973
|called|=0
|stable|=973
|infl|=969
|wpoint|=0
|side_dep|=93
|side_infl|=150
|var_messages|=0
|rho_write|=148
|dep|=832
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=2029.18MB, max=24.36MB, minor=2013.53MB, major=107.19MB, promoted=91.54MB
    minor collections=2122  major collections=172 compactions=0


runtime: 00:02:51.294
vars: 971, evals: 867

|rho|=973
|called|=0
|stable|=973
|infl|=969
|wpoint|=0
|side_dep|=105
|side_infl|=170
|var_messages|=0
|rho_write|=168
|dep|=832
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=2117.08MB, max=24.36MB, minor=2100.82MB, major=110.35MB, promoted=94.09MB
    minor collections=2218  major collections=180 compactions=0

[Info][Witness] unassume invariant: ((((((((((((main__i != 0 && main__nlen != 0) && 8LL - (long long )main__j >= 0LL) && (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL) && (-40LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL) && main__j <= 8) && 5 <= main__nlen) && 4 <= main__i) && 0 <= main__j) && 8LL - (long long )main__j >= 0LL) && (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL) && (-40LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL) && main__j <= 8) && 0 <= main__j (../plain/id_build.i.p+nlh-reducer.c:1794:2-1794:13)

runtime: 00:03:01.292
vars: 971, evals: 867

|rho|=973
|called|=0
|stable|=973
|infl|=969
|wpoint|=0
|side_dep|=119
|side_infl|=187
|var_messages|=1
|rho_write|=185
|dep|=832
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=2229.78MB, max=24.36MB, minor=2212.93MB, major=113.72MB, promoted=96.88MB
    minor collections=2321  major collections=188 compactions=0


runtime: 00:03:11.356
vars: 971, evals: 867

|rho|=973
|called|=0
|stable|=973
|infl|=969
|wpoint|=0
|side_dep|=131
|side_infl|=199
|var_messages|=1
|rho_write|=197
|dep|=832
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=2344.65MB, max=24.36MB, minor=2327.26MB, major=116.84MB, promoted=99.46MB
    minor collections=2412  major collections=194 compactions=0

[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((main__i != 0 && main__nlen != 0) && 7LL - (long long )main__j >= 0LL) && (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL) && (-39LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL) && main__j <= 7) && 5 <= main__nlen) && 4 <= main__i) && 0 <= main__j) && 7LL - (long long )main__j >= 0LL) && (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL) && (-40LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL) && 7LL - (long long )main__j >= 0LL) && (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL) && (-40LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL) && main__i != 0) && main__nlen != 0) && 7LL - (long long )main__j >= 0LL) && (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL) && (-40LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL) && 5 <= main__nlen) && 4 <= main__i) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -3LL + (long long )main__nlen >= 0LL) && 3 <= main__nlen) && -3LL + (long long )main__nlen >= 0LL) && 7LL - (long long )main__j >= 0LL) && (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL) && (-39LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL) && main__j <= 7) && 0 <= main__j (../plain/id_build.i.p+nlh-reducer.c:2008:6-2008:34)
[Info][Witness] unassume invariant: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((main__i != 0 && main__nlen != 0) && 7LL - (long long )main__j >= 0LL) && (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL) && (-39LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL) && main__j <= 7) && 5 <= main__nlen) && 4 <= main__i) && 0 <= main__j) && 7LL - (long long )main__j >= 0LL) && (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL) && (-40LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL) && 7LL - (long long )main__j >= 0LL) && (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL) && (-40LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL) && main__i != 0) && main__nlen != 0) && 7LL - (long long )main__j >= 0LL) && (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL) && (-40LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL) && 5 <= main__nlen) && 4 <= main__i) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -4LL + (long long )main__nlen >= 0LL) && 4 <= main__nlen) && -4LL + (long long )main__nlen >= 0LL) && -4LL + (long long )main__nlen >= 0LL) && main__nlen != 0) && -3LL + (long long )main__nlen >= 0LL) && 3 <= main__nlen) && -3LL + (long long )main__nlen >= 0LL) && 7LL - (long long )main__j >= 0LL) && (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL) && (-39LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL) && main__j <= 7) && 0 <= main__j (../plain/id_build.i.p+nlh-reducer.c:1761:6-1761:34)
[Info][Witness] unassume invariant: ((((((((((((main__i != 0 && main__nlen != 0) && 8LL - (long long )main__j >= 0LL) && (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL) && (-40LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL) && main__j <= 8) && 5 <= main__nlen) && 4 <= main__i) && 0 <= main__j) && 8LL - (long long )main__j >= 0LL) && (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL) && (-40LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL) && main__j <= 8) && 0 <= main__j (../plain/id_build.i.p+nlh-reducer.c:1769:2-1769:23)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (../plain/id_build.i.p+nlh-reducer.c:4:1-4:90)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (../plain/id_build.i.p+nlh-reducer.c:6:1-8:1)
[Warning][Deadcode] Function 'main' has dead code:
  on line 34 (../plain/id_build.i.p+nlh-reducer.c:34-34)
  on line 45 (../plain/id_build.i.p+nlh-reducer.c:45-45)
  on line 59 (../plain/id_build.i.p+nlh-reducer.c:59-59)
  on line 70 (../plain/id_build.i.p+nlh-reducer.c:70-70)
  on line 84 (../plain/id_build.i.p+nlh-reducer.c:84-84)
  on line 95 (../plain/id_build.i.p+nlh-reducer.c:95-95)
  on line 109 (../plain/id_build.i.p+nlh-reducer.c:109-109)
  on line 120 (../plain/id_build.i.p+nlh-reducer.c:120-120)
  on line 134 (../plain/id_build.i.p+nlh-reducer.c:134-134)
  on line 145 (../plain/id_build.i.p+nlh-reducer.c:145-145)
  on line 159 (../plain/id_build.i.p+nlh-reducer.c:159-159)
  on line 170 (../plain/id_build.i.p+nlh-reducer.c:170-170)
  on line 184 (../plain/id_build.i.p+nlh-reducer.c:184-184)
  on line 195 (../plain/id_build.i.p+nlh-reducer.c:195-195)
  on line 209 (../plain/id_build.i.p+nlh-reducer.c:209-209)
  on line 220 (../plain/id_build.i.p+nlh-reducer.c:220-220)
  on line 229 (../plain/id_build.i.p+nlh-reducer.c:229-229)
  on lines 231..232 (../plain/id_build.i.p+nlh-reducer.c:231-232)
  on line 234 (../plain/id_build.i.p+nlh-reducer.c:234-234)
  on line 240 (../plain/id_build.i.p+nlh-reducer.c:240-240)
  on lines 242..243 (../plain/id_build.i.p+nlh-reducer.c:242-243)
  on line 245 (../plain/id_build.i.p+nlh-reducer.c:245-245)
  on lines 249..250 (../plain/id_build.i.p+nlh-reducer.c:249-250)
  on line 254 (../plain/id_build.i.p+nlh-reducer.c:254-254)
  on lines 256..257 (../plain/id_build.i.p+nlh-reducer.c:256-257)
  on line 259 (../plain/id_build.i.p+nlh-reducer.c:259-259)
  on line 265 (../plain/id_build.i.p+nlh-reducer.c:265-265)
  on lines 267..268 (../plain/id_build.i.p+nlh-reducer.c:267-268)
  on line 270 (../plain/id_build.i.p+nlh-reducer.c:270-270)
  on lines 274..275 (../plain/id_build.i.p+nlh-reducer.c:274-275)
  on line 279 (../plain/id_build.i.p+nlh-reducer.c:279-279)
  on lines 281..282 (../plain/id_build.i.p+nlh-reducer.c:281-282)
  on line 284 (../plain/id_build.i.p+nlh-reducer.c:284-284)
  on line 290 (../plain/id_build.i.p+nlh-reducer.c:290-290)
  on lines 292..293 (../plain/id_build.i.p+nlh-reducer.c:292-293)
  on line 295 (../plain/id_build.i.p+nlh-reducer.c:295-295)
  on lines 299..300 (../plain/id_build.i.p+nlh-reducer.c:299-300)
  on line 304 (../plain/id_build.i.p+nlh-reducer.c:304-304)
  on lines 306..307 (../plain/id_build.i.p+nlh-reducer.c:306-307)
  on line 309 (../plain/id_build.i.p+nlh-reducer.c:309-309)
  on line 315 (../plain/id_build.i.p+nlh-reducer.c:315-315)
  on lines 317..318 (../plain/id_build.i.p+nlh-reducer.c:317-318)
  on line 320 (../plain/id_build.i.p+nlh-reducer.c:320-320)
  on lines 324..325 (../plain/id_build.i.p+nlh-reducer.c:324-325)
  on line 329 (../plain/id_build.i.p+nlh-reducer.c:329-329)
  on lines 331..332 (../plain/id_build.i.p+nlh-reducer.c:331-332)
  on line 334 (../plain/id_build.i.p+nlh-reducer.c:334-334)
  on line 340 (../plain/id_build.i.p+nlh-reducer.c:340-340)
  on lines 342..343 (../plain/id_build.i.p+nlh-reducer.c:342-343)
  on line 345 (../plain/id_build.i.p+nlh-reducer.c:345-345)
  on lines 349..350 (../plain/id_build.i.p+nlh-reducer.c:349-350)
  on line 354 (../plain/id_build.i.p+nlh-reducer.c:354-354)
  on lines 356..357 (../plain/id_build.i.p+nlh-reducer.c:356-357)
  on line 359 (../plain/id_build.i.p+nlh-reducer.c:359-359)
  on line 365 (../plain/id_build.i.p+nlh-reducer.c:365-365)
  on lines 367..368 (../plain/id_build.i.p+nlh-reducer.c:367-368)
  on line 370 (../plain/id_build.i.p+nlh-reducer.c:370-370)
  on lines 374..375 (../plain/id_build.i.p+nlh-reducer.c:374-375)
  on line 379 (../plain/id_build.i.p+nlh-reducer.c:379-379)
  on lines 381..382 (../plain/id_build.i.p+nlh-reducer.c:381-382)
  on line 384 (../plain/id_build.i.p+nlh-reducer.c:384-384)
  on line 390 (../plain/id_build.i.p+nlh-reducer.c:390-390)
  on lines 392..393 (../plain/id_build.i.p+nlh-reducer.c:392-393)
  on line 395 (../plain/id_build.i.p+nlh-reducer.c:395-395)
  on lines 399..400 (../plain/id_build.i.p+nlh-reducer.c:399-400)
  on line 404 (../plain/id_build.i.p+nlh-reducer.c:404-404)
  on lines 406..407 (../plain/id_build.i.p+nlh-reducer.c:406-407)
  on line 409 (../plain/id_build.i.p+nlh-reducer.c:409-409)
  on line 415 (../plain/id_build.i.p+nlh-reducer.c:415-415)
  on lines 417..418 (../plain/id_build.i.p+nlh-reducer.c:417-418)
  on line 420 (../plain/id_build.i.p+nlh-reducer.c:420-420)
  on line 424 (../plain/id_build.i.p+nlh-reducer.c:424-424)
  on line 426 (../plain/id_build.i.p+nlh-reducer.c:426-426)
  on line 430 (../plain/id_build.i.p+nlh-reducer.c:430-430)
  on lines 432..433 (../plain/id_build.i.p+nlh-reducer.c:432-433)
  on line 435 (../plain/id_build.i.p+nlh-reducer.c:435-435)
  on line 441 (../plain/id_build.i.p+nlh-reducer.c:441-441)
  on lines 443..444 (../plain/id_build.i.p+nlh-reducer.c:443-444)
  on line 446 (../plain/id_build.i.p+nlh-reducer.c:446-446)
  on line 473 (../plain/id_build.i.p+nlh-reducer.c:473-473)
  on line 484 (../plain/id_build.i.p+nlh-reducer.c:484-484)
  on line 498 (../plain/id_build.i.p+nlh-reducer.c:498-498)
  on line 509 (../plain/id_build.i.p+nlh-reducer.c:509-509)
  on line 523 (../plain/id_build.i.p+nlh-reducer.c:523-523)
  on line 534 (../plain/id_build.i.p+nlh-reducer.c:534-534)
  on line 548 (../plain/id_build.i.p+nlh-reducer.c:548-548)
  on line 559 (../plain/id_build.i.p+nlh-reducer.c:559-559)
  on line 573 (../plain/id_build.i.p+nlh-reducer.c:573-573)
  on line 584 (../plain/id_build.i.p+nlh-reducer.c:584-584)
  on line 598 (../plain/id_build.i.p+nlh-reducer.c:598-598)
  on line 609 (../plain/id_build.i.p+nlh-reducer.c:609-609)
  on line 623 (../plain/id_build.i.p+nlh-reducer.c:623-623)
  on line 634 (../plain/id_build.i.p+nlh-reducer.c:634-634)
  on line 648 (../plain/id_build.i.p+nlh-reducer.c:648-648)
  on line 659 (../plain/id_build.i.p+nlh-reducer.c:659-659)
  on line 668 (../plain/id_build.i.p+nlh-reducer.c:668-668)
  on lines 670..671 (../plain/id_build.i.p+nlh-reducer.c:670-671)
  on line 673 (../plain/id_build.i.p+nlh-reducer.c:673-673)
  on line 679 (../plain/id_build.i.p+nlh-reducer.c:679-679)
  on lines 681..682 (../plain/id_build.i.p+nlh-reducer.c:681-682)
  on line 684 (../plain/id_build.i.p+nlh-reducer.c:684-684)
  on lines 688..689 (../plain/id_build.i.p+nlh-reducer.c:688-689)
  on line 693 (../plain/id_build.i.p+nlh-reducer.c:693-693)
  on lines 695..696 (../plain/id_build.i.p+nlh-reducer.c:695-696)
  on line 698 (../plain/id_build.i.p+nlh-reducer.c:698-698)
  on line 704 (../plain/id_build.i.p+nlh-reducer.c:704-704)
  on lines 706..707 (../plain/id_build.i.p+nlh-reducer.c:706-707)
  on line 709 (../plain/id_build.i.p+nlh-reducer.c:709-709)
  on lines 713..714 (../plain/id_build.i.p+nlh-reducer.c:713-714)
  on line 718 (../plain/id_build.i.p+nlh-reducer.c:718-718)
  on lines 720..721 (../plain/id_build.i.p+nlh-reducer.c:720-721)
  on line 723 (../plain/id_build.i.p+nlh-reducer.c:723-723)
  on line 729 (../plain/id_build.i.p+nlh-reducer.c:729-729)
  on lines 731..732 (../plain/id_build.i.p+nlh-reducer.c:731-732)
  on line 734 (../plain/id_build.i.p+nlh-reducer.c:734-734)
  on lines 738..739 (../plain/id_build.i.p+nlh-reducer.c:738-739)
  on line 743 (../plain/id_build.i.p+nlh-reducer.c:743-743)
  on lines 745..746 (../plain/id_build.i.p+nlh-reducer.c:745-746)
  on line 748 (../plain/id_build.i.p+nlh-reducer.c:748-748)
  on line 754 (../plain/id_build.i.p+nlh-reducer.c:754-754)
  on lines 756..757 (../plain/id_build.i.p+nlh-reducer.c:756-757)
  on line 759 (../plain/id_build.i.p+nlh-reducer.c:759-759)
  on lines 763..764 (../plain/id_build.i.p+nlh-reducer.c:763-764)
  on line 768 (../plain/id_build.i.p+nlh-reducer.c:768-768)
  on lines 770..771 (../plain/id_build.i.p+nlh-reducer.c:770-771)
  on line 773 (../plain/id_build.i.p+nlh-reducer.c:773-773)
  on line 779 (../plain/id_build.i.p+nlh-reducer.c:779-779)
  on lines 781..782 (../plain/id_build.i.p+nlh-reducer.c:781-782)
  on line 784 (../plain/id_build.i.p+nlh-reducer.c:784-784)
  on lines 788..789 (../plain/id_build.i.p+nlh-reducer.c:788-789)
  on line 793 (../plain/id_build.i.p+nlh-reducer.c:793-793)
  on lines 795..796 (../plain/id_build.i.p+nlh-reducer.c:795-796)
  on line 798 (../plain/id_build.i.p+nlh-reducer.c:798-798)
  on line 804 (../plain/id_build.i.p+nlh-reducer.c:804-804)
  on lines 806..807 (../plain/id_build.i.p+nlh-reducer.c:806-807)
  on line 809 (../plain/id_build.i.p+nlh-reducer.c:809-809)
  on lines 813..814 (../plain/id_build.i.p+nlh-reducer.c:813-814)
  on line 818 (../plain/id_build.i.p+nlh-reducer.c:818-818)
  on lines 820..821 (../plain/id_build.i.p+nlh-reducer.c:820-821)
  on line 823 (../plain/id_build.i.p+nlh-reducer.c:823-823)
  on line 829 (../plain/id_build.i.p+nlh-reducer.c:829-829)
  on lines 831..832 (../plain/id_build.i.p+nlh-reducer.c:831-832)
  on line 834 (../plain/id_build.i.p+nlh-reducer.c:834-834)
  on lines 838..839 (../plain/id_build.i.p+nlh-reducer.c:838-839)
  on line 843 (../plain/id_build.i.p+nlh-reducer.c:843-843)
  on lines 845..846 (../plain/id_build.i.p+nlh-reducer.c:845-846)
  on line 848 (../plain/id_build.i.p+nlh-reducer.c:848-848)
  on line 854 (../plain/id_build.i.p+nlh-reducer.c:854-854)
  on lines 856..857 (../plain/id_build.i.p+nlh-reducer.c:856-857)
  on line 859 (../plain/id_build.i.p+nlh-reducer.c:859-859)
  on line 863 (../plain/id_build.i.p+nlh-reducer.c:863-863)
  on line 865 (../plain/id_build.i.p+nlh-reducer.c:865-865)
  on line 869 (../plain/id_build.i.p+nlh-reducer.c:869-869)
  on lines 871..872 (../plain/id_build.i.p+nlh-reducer.c:871-872)
  on line 874 (../plain/id_build.i.p+nlh-reducer.c:874-874)
  on line 880 (../plain/id_build.i.p+nlh-reducer.c:880-880)
  on lines 882..883 (../plain/id_build.i.p+nlh-reducer.c:882-883)
  on line 885 (../plain/id_build.i.p+nlh-reducer.c:885-885)
  on line 912 (../plain/id_build.i.p+nlh-reducer.c:912-912)
  on line 923 (../plain/id_build.i.p+nlh-reducer.c:923-923)
  on line 937 (../plain/id_build.i.p+nlh-reducer.c:937-937)
  on line 948 (../plain/id_build.i.p+nlh-reducer.c:948-948)
  on line 962 (../plain/id_build.i.p+nlh-reducer.c:962-962)
  on line 973 (../plain/id_build.i.p+nlh-reducer.c:973-973)
  on line 987 (../plain/id_build.i.p+nlh-reducer.c:987-987)
  on line 998 (../plain/id_build.i.p+nlh-reducer.c:998-998)
  on line 1012 (../plain/id_build.i.p+nlh-reducer.c:1012-1012)
  on line 1023 (../plain/id_build.i.p+nlh-reducer.c:1023-1023)
  on line 1037 (../plain/id_build.i.p+nlh-reducer.c:1037-1037)
  on line 1048 (../plain/id_build.i.p+nlh-reducer.c:1048-1048)
  on line 1062 (../plain/id_build.i.p+nlh-reducer.c:1062-1062)
  on line 1073 (../plain/id_build.i.p+nlh-reducer.c:1073-1073)
  on line 1087 (../plain/id_build.i.p+nlh-reducer.c:1087-1087)
  on line 1098 (../plain/id_build.i.p+nlh-reducer.c:1098-1098)
  on line 1107 (../plain/id_build.i.p+nlh-reducer.c:1107-1107)
  on lines 1109..1110 (../plain/id_build.i.p+nlh-reducer.c:1109-1110)
  on line 1112 (../plain/id_build.i.p+nlh-reducer.c:1112-1112)
  on line 1118 (../plain/id_build.i.p+nlh-reducer.c:1118-1118)
  on lines 1120..1121 (../plain/id_build.i.p+nlh-reducer.c:1120-1121)
  on line 1123 (../plain/id_build.i.p+nlh-reducer.c:1123-1123)
  on lines 1127..1128 (../plain/id_build.i.p+nlh-reducer.c:1127-1128)
  on line 1132 (../plain/id_build.i.p+nlh-reducer.c:1132-1132)
  on lines 1134..1135 (../plain/id_build.i.p+nlh-reducer.c:1134-1135)
  on line 1137 (../plain/id_build.i.p+nlh-reducer.c:1137-1137)
  on line 1143 (../plain/id_build.i.p+nlh-reducer.c:1143-1143)
  on lines 1145..1146 (../plain/id_build.i.p+nlh-reducer.c:1145-1146)
  on line 1148 (../plain/id_build.i.p+nlh-reducer.c:1148-1148)
  on lines 1152..1153 (../plain/id_build.i.p+nlh-reducer.c:1152-1153)
  on line 1157 (../plain/id_build.i.p+nlh-reducer.c:1157-1157)
  on lines 1159..1160 (../plain/id_build.i.p+nlh-reducer.c:1159-1160)
  on line 1162 (../plain/id_build.i.p+nlh-reducer.c:1162-1162)
  on line 1168 (../plain/id_build.i.p+nlh-reducer.c:1168-1168)
  on lines 1170..1171 (../plain/id_build.i.p+nlh-reducer.c:1170-1171)
  on line 1173 (../plain/id_build.i.p+nlh-reducer.c:1173-1173)
  on lines 1177..1178 (../plain/id_build.i.p+nlh-reducer.c:1177-1178)
  on line 1182 (../plain/id_build.i.p+nlh-reducer.c:1182-1182)
  on lines 1184..1185 (../plain/id_build.i.p+nlh-reducer.c:1184-1185)
  on line 1187 (../plain/id_build.i.p+nlh-reducer.c:1187-1187)
  on line 1193 (../plain/id_build.i.p+nlh-reducer.c:1193-1193)
  on lines 1195..1196 (../plain/id_build.i.p+nlh-reducer.c:1195-1196)
  on line 1198 (../plain/id_build.i.p+nlh-reducer.c:1198-1198)
  on lines 1202..1203 (../plain/id_build.i.p+nlh-reducer.c:1202-1203)
  on line 1207 (../plain/id_build.i.p+nlh-reducer.c:1207-1207)
  on lines 1209..1210 (../plain/id_build.i.p+nlh-reducer.c:1209-1210)
  on line 1212 (../plain/id_build.i.p+nlh-reducer.c:1212-1212)
  on line 1218 (../plain/id_build.i.p+nlh-reducer.c:1218-1218)
  on lines 1220..1221 (../plain/id_build.i.p+nlh-reducer.c:1220-1221)
  on line 1223 (../plain/id_build.i.p+nlh-reducer.c:1223-1223)
  on lines 1227..1228 (../plain/id_build.i.p+nlh-reducer.c:1227-1228)
  on line 1232 (../plain/id_build.i.p+nlh-reducer.c:1232-1232)
  on lines 1234..1235 (../plain/id_build.i.p+nlh-reducer.c:1234-1235)
  on line 1237 (../plain/id_build.i.p+nlh-reducer.c:1237-1237)
  on line 1243 (../plain/id_build.i.p+nlh-reducer.c:1243-1243)
  on lines 1245..1246 (../plain/id_build.i.p+nlh-reducer.c:1245-1246)
  on line 1248 (../plain/id_build.i.p+nlh-reducer.c:1248-1248)
  on lines 1252..1253 (../plain/id_build.i.p+nlh-reducer.c:1252-1253)
  on line 1257 (../plain/id_build.i.p+nlh-reducer.c:1257-1257)
  on lines 1259..1260 (../plain/id_build.i.p+nlh-reducer.c:1259-1260)
  on line 1262 (../plain/id_build.i.p+nlh-reducer.c:1262-1262)
  on line 1268 (../plain/id_build.i.p+nlh-reducer.c:1268-1268)
  on lines 1270..1271 (../plain/id_build.i.p+nlh-reducer.c:1270-1271)
  on line 1273 (../plain/id_build.i.p+nlh-reducer.c:1273-1273)
  on lines 1277..1278 (../plain/id_build.i.p+nlh-reducer.c:1277-1278)
  on line 1282 (../plain/id_build.i.p+nlh-reducer.c:1282-1282)
  on lines 1284..1285 (../plain/id_build.i.p+nlh-reducer.c:1284-1285)
  on line 1287 (../plain/id_build.i.p+nlh-reducer.c:1287-1287)
  on line 1293 (../plain/id_build.i.p+nlh-reducer.c:1293-1293)
  on lines 1295..1296 (../plain/id_build.i.p+nlh-reducer.c:1295-1296)
  on line 1298 (../plain/id_build.i.p+nlh-reducer.c:1298-1298)
  on line 1302 (../plain/id_build.i.p+nlh-reducer.c:1302-1302)
  on line 1304 (../plain/id_build.i.p+nlh-reducer.c:1304-1304)
  on line 1308 (../plain/id_build.i.p+nlh-reducer.c:1308-1308)
  on lines 1310..1311 (../plain/id_build.i.p+nlh-reducer.c:1310-1311)
  on line 1313 (../plain/id_build.i.p+nlh-reducer.c:1313-1313)
  on line 1319 (../plain/id_build.i.p+nlh-reducer.c:1319-1319)
  on lines 1321..1322 (../plain/id_build.i.p+nlh-reducer.c:1321-1322)
  on line 1324 (../plain/id_build.i.p+nlh-reducer.c:1324-1324)
  on line 1351 (../plain/id_build.i.p+nlh-reducer.c:1351-1351)
  on line 1362 (../plain/id_build.i.p+nlh-reducer.c:1362-1362)
  on line 1376 (../plain/id_build.i.p+nlh-reducer.c:1376-1376)
  on line 1387 (../plain/id_build.i.p+nlh-reducer.c:1387-1387)
  on line 1401 (../plain/id_build.i.p+nlh-reducer.c:1401-1401)
  on line 1412 (../plain/id_build.i.p+nlh-reducer.c:1412-1412)
  on line 1426 (../plain/id_build.i.p+nlh-reducer.c:1426-1426)
  on line 1437 (../plain/id_build.i.p+nlh-reducer.c:1437-1437)
  on line 1451 (../plain/id_build.i.p+nlh-reducer.c:1451-1451)
  on line 1462 (../plain/id_build.i.p+nlh-reducer.c:1462-1462)
  on line 1476 (../plain/id_build.i.p+nlh-reducer.c:1476-1476)
  on line 1487 (../plain/id_build.i.p+nlh-reducer.c:1487-1487)
  on line 1501 (../plain/id_build.i.p+nlh-reducer.c:1501-1501)
  on line 1512 (../plain/id_build.i.p+nlh-reducer.c:1512-1512)
  on line 1526 (../plain/id_build.i.p+nlh-reducer.c:1526-1526)
  on line 1537 (../plain/id_build.i.p+nlh-reducer.c:1537-1537)
  on line 1546 (../plain/id_build.i.p+nlh-reducer.c:1546-1546)
  on lines 1548..1549 (../plain/id_build.i.p+nlh-reducer.c:1548-1549)
  on line 1551 (../plain/id_build.i.p+nlh-reducer.c:1551-1551)
  on line 1557 (../plain/id_build.i.p+nlh-reducer.c:1557-1557)
  on lines 1559..1560 (../plain/id_build.i.p+nlh-reducer.c:1559-1560)
  on line 1562 (../plain/id_build.i.p+nlh-reducer.c:1562-1562)
  on lines 1566..1567 (../plain/id_build.i.p+nlh-reducer.c:1566-1567)
  on line 1571 (../plain/id_build.i.p+nlh-reducer.c:1571-1571)
  on lines 1573..1574 (../plain/id_build.i.p+nlh-reducer.c:1573-1574)
  on line 1576 (../plain/id_build.i.p+nlh-reducer.c:1576-1576)
  on line 1582 (../plain/id_build.i.p+nlh-reducer.c:1582-1582)
  on lines 1584..1585 (../plain/id_build.i.p+nlh-reducer.c:1584-1585)
  on line 1587 (../plain/id_build.i.p+nlh-reducer.c:1587-1587)
  on lines 1591..1592 (../plain/id_build.i.p+nlh-reducer.c:1591-1592)
  on line 1596 (../plain/id_build.i.p+nlh-reducer.c:1596-1596)
  on lines 1598..1599 (../plain/id_build.i.p+nlh-reducer.c:1598-1599)
  on line 1601 (../plain/id_build.i.p+nlh-reducer.c:1601-1601)
  on line 1607 (../plain/id_build.i.p+nlh-reducer.c:1607-1607)
  on lines 1609..1610 (../plain/id_build.i.p+nlh-reducer.c:1609-1610)
  on line 1612 (../plain/id_build.i.p+nlh-reducer.c:1612-1612)
  on lines 1616..1617 (../plain/id_build.i.p+nlh-reducer.c:1616-1617)
  on line 1621 (../plain/id_build.i.p+nlh-reducer.c:1621-1621)
  on lines 1623..1624 (../plain/id_build.i.p+nlh-reducer.c:1623-1624)
  on line 1626 (../plain/id_build.i.p+nlh-reducer.c:1626-1626)
  on line 1632 (../plain/id_build.i.p+nlh-reducer.c:1632-1632)
  on lines 1634..1635 (../plain/id_build.i.p+nlh-reducer.c:1634-1635)
  on line 1637 (../plain/id_build.i.p+nlh-reducer.c:1637-1637)
  on lines 1641..1642 (../plain/id_build.i.p+nlh-reducer.c:1641-1642)
  on line 1646 (../plain/id_build.i.p+nlh-reducer.c:1646-1646)
  on lines 1648..1649 (../plain/id_build.i.p+nlh-reducer.c:1648-1649)
  on line 1651 (../plain/id_build.i.p+nlh-reducer.c:1651-1651)
  on line 1657 (../plain/id_build.i.p+nlh-reducer.c:1657-1657)
  on lines 1659..1660 (../plain/id_build.i.p+nlh-reducer.c:1659-1660)
  on line 1662 (../plain/id_build.i.p+nlh-reducer.c:1662-1662)
  on lines 1666..1667 (../plain/id_build.i.p+nlh-reducer.c:1666-1667)
  on line 1671 (../plain/id_build.i.p+nlh-reducer.c:1671-1671)
  on lines 1673..1674 (../plain/id_build.i.p+nlh-reducer.c:1673-1674)
  on line 1676 (../plain/id_build.i.p+nlh-reducer.c:1676-1676)
  on line 1682 (../plain/id_build.i.p+nlh-reducer.c:1682-1682)
  on lines 1684..1685 (../plain/id_build.i.p+nlh-reducer.c:1684-1685)
  on line 1687 (../plain/id_build.i.p+nlh-reducer.c:1687-1687)
  on lines 1691..1692 (../plain/id_build.i.p+nlh-reducer.c:1691-1692)
  on line 1696 (../plain/id_build.i.p+nlh-reducer.c:1696-1696)
  on lines 1698..1699 (../plain/id_build.i.p+nlh-reducer.c:1698-1699)
  on line 1701 (../plain/id_build.i.p+nlh-reducer.c:1701-1701)
  on line 1707 (../plain/id_build.i.p+nlh-reducer.c:1707-1707)
  on lines 1709..1710 (../plain/id_build.i.p+nlh-reducer.c:1709-1710)
  on line 1712 (../plain/id_build.i.p+nlh-reducer.c:1712-1712)
  on lines 1716..1717 (../plain/id_build.i.p+nlh-reducer.c:1716-1717)
  on line 1721 (../plain/id_build.i.p+nlh-reducer.c:1721-1721)
  on lines 1723..1724 (../plain/id_build.i.p+nlh-reducer.c:1723-1724)
  on line 1726 (../plain/id_build.i.p+nlh-reducer.c:1726-1726)
  on line 1732 (../plain/id_build.i.p+nlh-reducer.c:1732-1732)
  on lines 1734..1735 (../plain/id_build.i.p+nlh-reducer.c:1734-1735)
  on line 1737 (../plain/id_build.i.p+nlh-reducer.c:1737-1737)
  on lines 1741..1742 (../plain/id_build.i.p+nlh-reducer.c:1741-1742)
  on line 1746 (../plain/id_build.i.p+nlh-reducer.c:1746-1746)
  on lines 1748..1749 (../plain/id_build.i.p+nlh-reducer.c:1748-1749)
  on line 1751 (../plain/id_build.i.p+nlh-reducer.c:1751-1751)
  on lines 1763..1764 (../plain/id_build.i.p+nlh-reducer.c:1763-1764)
  on lines 1780..1781 (../plain/id_build.i.p+nlh-reducer.c:1780-1781)
  on line 1824 (../plain/id_build.i.p+nlh-reducer.c:1824-1824)
  on line 1835 (../plain/id_build.i.p+nlh-reducer.c:1835-1835)
  on line 1849 (../plain/id_build.i.p+nlh-reducer.c:1849-1849)
  on line 1860 (../plain/id_build.i.p+nlh-reducer.c:1860-1860)
  on line 1874 (../plain/id_build.i.p+nlh-reducer.c:1874-1874)
  on line 1885 (../plain/id_build.i.p+nlh-reducer.c:1885-1885)
  on line 1899 (../plain/id_build.i.p+nlh-reducer.c:1899-1899)
  on line 1910 (../plain/id_build.i.p+nlh-reducer.c:1910-1910)
  on line 1924 (../plain/id_build.i.p+nlh-reducer.c:1924-1924)
  on line 1935 (../plain/id_build.i.p+nlh-reducer.c:1935-1935)
  on line 1949 (../plain/id_build.i.p+nlh-reducer.c:1949-1949)
  on line 1960 (../plain/id_build.i.p+nlh-reducer.c:1960-1960)
  on line 1974 (../plain/id_build.i.p+nlh-reducer.c:1974-1974)
  on line 1985 (../plain/id_build.i.p+nlh-reducer.c:1985-1985)
  on line 1999 (../plain/id_build.i.p+nlh-reducer.c:1999-1999)
  on line 2010 (../plain/id_build.i.p+nlh-reducer.c:2010-2010)
  on line 2022 (../plain/id_build.i.p+nlh-reducer.c:2022-2022)
  on line 2031 (../plain/id_build.i.p+nlh-reducer.c:2031-2031)
  on line 2040 (../plain/id_build.i.p+nlh-reducer.c:2040-2040)
  on line 2049 (../plain/id_build.i.p+nlh-reducer.c:2049-2049)
  on line 2058 (../plain/id_build.i.p+nlh-reducer.c:2058-2058)
  on line 2067 (../plain/id_build.i.p+nlh-reducer.c:2067-2067)
  on line 2076 (../plain/id_build.i.p+nlh-reducer.c:2076-2076)
  on line 2085 (../plain/id_build.i.p+nlh-reducer.c:2085-2085)
  on line 2172 (../plain/id_build.i.p+nlh-reducer.c:2172-2172)
  on line 2181 (../plain/id_build.i.p+nlh-reducer.c:2181-2181)
  on line 2190 (../plain/id_build.i.p+nlh-reducer.c:2190-2190)
  on line 2199 (../plain/id_build.i.p+nlh-reducer.c:2199-2199)
  on line 2208 (../plain/id_build.i.p+nlh-reducer.c:2208-2208)
  on line 2217 (../plain/id_build.i.p+nlh-reducer.c:2217-2217)
  on line 2226 (../plain/id_build.i.p+nlh-reducer.c:2226-2226)
  on line 2235 (../plain/id_build.i.p+nlh-reducer.c:2235-2235)
  on line 2322 (../plain/id_build.i.p+nlh-reducer.c:2322-2322)
  on line 2331 (../plain/id_build.i.p+nlh-reducer.c:2331-2331)
  on line 2340 (../plain/id_build.i.p+nlh-reducer.c:2340-2340)
  on line 2349 (../plain/id_build.i.p+nlh-reducer.c:2349-2349)
  on line 2358 (../plain/id_build.i.p+nlh-reducer.c:2358-2358)
  on line 2367 (../plain/id_build.i.p+nlh-reducer.c:2367-2367)
  on line 2376 (../plain/id_build.i.p+nlh-reducer.c:2376-2376)
  on line 2385 (../plain/id_build.i.p+nlh-reducer.c:2385-2385)
  on line 2472 (../plain/id_build.i.p+nlh-reducer.c:2472-2472)
  on line 2481 (../plain/id_build.i.p+nlh-reducer.c:2481-2481)
  on line 2490 (../plain/id_build.i.p+nlh-reducer.c:2490-2490)
  on line 2499 (../plain/id_build.i.p+nlh-reducer.c:2499-2499)
  on line 2508 (../plain/id_build.i.p+nlh-reducer.c:2508-2508)
  on line 2517 (../plain/id_build.i.p+nlh-reducer.c:2517-2517)
  on line 2526 (../plain/id_build.i.p+nlh-reducer.c:2526-2526)
  on line 2535 (../plain/id_build.i.p+nlh-reducer.c:2535-2535)
  on line 2622 (../plain/id_build.i.p+nlh-reducer.c:2622-2622)
  on line 2631 (../plain/id_build.i.p+nlh-reducer.c:2631-2631)
  on line 2640 (../plain/id_build.i.p+nlh-reducer.c:2640-2640)
  on line 2649 (../plain/id_build.i.p+nlh-reducer.c:2649-2649)
  on line 2658 (../plain/id_build.i.p+nlh-reducer.c:2658-2658)
  on line 2667 (../plain/id_build.i.p+nlh-reducer.c:2667-2667)
  on line 2676 (../plain/id_build.i.p+nlh-reducer.c:2676-2676)
  on line 2685 (../plain/id_build.i.p+nlh-reducer.c:2685-2685)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 359
  dead: 475 (3 in uncalled functions)
  total lines: 834
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:539:6-539:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___115 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1524:6-1524:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:50:6-50:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___77 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1035:6-1035:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___39 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:546:6-546:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___135 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1778:6-1778:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___116 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1535:6-1535:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___1 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:57:6-57:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___78 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1046:6-1046:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___40 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:557:6-557:34)
[Warning][Deadcode][CWE-570] condition 'main__j < 8' is always false (../plain/id_build.i.p+nlh-reducer.c:1542:6-1542:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___2 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:68:6-68:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1053:6-1053:17)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:564:6-564:17)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:75:6-75:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___79 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1060:6-1060:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___41 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:571:6-571:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___3 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:82:6-82:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___80 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1071:6-1071:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___42 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:582:6-582:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___4 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:93:6-93:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1078:6-1078:17)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1815:6-1815:17)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:589:6-589:17)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:100:6-100:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___81 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1085:6-1085:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___136 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1822:6-1822:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___43 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:596:6-596:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___5 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:107:6-107:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___82 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1096:6-1096:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___137 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1833:6-1833:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1342:6-1342:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___44 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:607:6-607:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___6 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:118:6-118:34)
[Warning][Deadcode][CWE-570] condition 'main__j < 8' is always false (../plain/id_build.i.p+nlh-reducer.c:1103:6-1103:17)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1840:6-1840:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___101 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1349:6-1349:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:614:6-614:17)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:125:6-125:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___138 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1847:6-1847:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___102 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1360:6-1360:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___45 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:621:6-621:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___7 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:132:6-132:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___139 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1858:6-1858:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1367:6-1367:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___46 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:632:6-632:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___8 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:143:6-143:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1865:6-1865:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___103 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1374:6-1374:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:639:6-639:17)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:150:6-150:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___140 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1872:6-1872:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___104 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1385:6-1385:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___47 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:646:6-646:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___9 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:157:6-157:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___141 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1883:6-1883:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1392:6-1392:17)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:903:6-903:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___48 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:657:6-657:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___10 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:168:6-168:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1890:6-1890:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___105 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1399:6-1399:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___67 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:910:6-910:34)
[Warning][Deadcode][CWE-570] condition 'main__j < 8' is always false (../plain/id_build.i.p+nlh-reducer.c:664:6-664:17)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:175:6-175:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___142 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1897:6-1897:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___106 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1410:6-1410:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___68 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:921:6-921:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___11 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:182:6-182:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___143 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1908:6-1908:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1417:6-1417:17)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:928:6-928:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___12 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:193:6-193:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1915:6-1915:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___107 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1424:6-1424:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___69 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:935:6-935:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:200:6-200:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___144 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1922:6-1922:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___108 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1435:6-1435:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___70 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:946:6-946:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___13 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:207:6-207:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___145 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1933:6-1933:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1442:6-1442:17)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:953:6-953:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___14 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:218:6-218:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1940:6-1940:17)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:464:6-464:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___109 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1449:6-1449:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___71 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:960:6-960:34)
[Warning][Deadcode][CWE-570] condition 'main__j < 8' is always false (../plain/id_build.i.p+nlh-reducer.c:225:6-225:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___146 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1947:6-1947:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___33 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:471:6-471:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___110 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1460:6-1460:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___72 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:971:6-971:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___147 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1958:6-1958:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___34 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:482:6-482:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1467:6-1467:17)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:978:6-978:17)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1965:6-1965:17)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:489:6-489:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___111 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1474:6-1474:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___73 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:985:6-985:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___148 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1972:6-1972:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___35 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:496:6-496:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___112 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1485:6-1485:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___74 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:996:6-996:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___149 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1983:6-1983:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___36 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:507:6-507:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1492:6-1492:17)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1003:6-1003:17)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1990:6-1990:17)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:514:6-514:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___113 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1499:6-1499:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:25:6-25:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___75 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1010:6-1010:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___150 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1997:6-1997:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___37 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:521:6-521:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___114 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1510:6-1510:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:32:6-32:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___76 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1021:6-1021:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___134 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:1761:6-1761:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___151 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:2008:6-2008:34)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___38 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:532:6-532:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1517:6-1517:17)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__cond___0 == 0' is always false (../plain/id_build.i.p+nlh-reducer.c:43:6-43:34)
[Warning][Deadcode][CWE-571] condition 'main__j < 8' is always true (../plain/id_build.i.p+nlh-reducer.c:1028:6-1028:17)
[Success][Witness] invariant confirmed: 0 <= main__j (../plain/id_build.i.p+nlh-reducer.c:1769:2)
[Success][Witness] invariant confirmed: main__j <= 7 (../plain/id_build.i.p+nlh-reducer.c:1769:2)
[Success][Witness] invariant confirmed: (-39LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1769:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1769:2)
[Success][Witness] invariant confirmed: 7LL - (long long )main__j >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1769:2)
[Success][Witness] invariant confirmed: 0 <= main__j (../plain/id_build.i.p+nlh-reducer.c:1771:6)
[Success][Witness] invariant confirmed: main__j <= 8 (../plain/id_build.i.p+nlh-reducer.c:1771:6)
[Success][Witness] invariant confirmed: (-40LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1771:6)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1771:6)
[Success][Witness] invariant confirmed: 8LL - (long long )main__j >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1771:6)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:899:2)
[Success][Witness] invariant confirmed: 2 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:900:6)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:900:6)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:900:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:902:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:903:6)
[Success][Witness] invariant confirmed: 3 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:907:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:907:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:907:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:909:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:910:6)
[Success][Witness] invariant confirmed: 3 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:918:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:918:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:918:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:920:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:921:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:927:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:928:6)
[Success][Witness] invariant confirmed: 3 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:932:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:932:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:932:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:934:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:935:6)
[Success][Witness] invariant confirmed: 3 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:943:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:943:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:943:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:945:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:946:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:952:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:953:6)
[Success][Witness] invariant confirmed: 3 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:957:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:957:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:957:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:959:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:960:6)
[Success][Witness] invariant confirmed: 3 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:968:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:968:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:968:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:970:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:971:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:977:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:978:6)
[Success][Witness] invariant confirmed: 3 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:982:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:982:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:982:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:984:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:985:6)
[Success][Witness] invariant confirmed: 3 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:993:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:993:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:993:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:995:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:996:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1002:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1003:6)
[Success][Witness] invariant confirmed: 3 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1007:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1007:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1007:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:24:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1009:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:25:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1010:6)
[Success][Witness] invariant confirmed: 1 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:29:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:29:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:29:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:31:2)
[Success][Witness] invariant confirmed: 3 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1018:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1018:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1018:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:32:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1020:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1021:6)
[Success][Witness] invariant confirmed: 1 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:40:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:40:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:40:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:42:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1027:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:43:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1028:6)
[Success][Witness] invariant confirmed: 3 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1032:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1032:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1032:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1034:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:49:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1035:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:50:6)
[Success][Witness] invariant confirmed: 1 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:54:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:54:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:54:2)
[Success][Witness] invariant confirmed: 3 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1043:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1043:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1043:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:56:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1045:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:57:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1046:6)
[Success][Witness] invariant confirmed: 1 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:65:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:65:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:65:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1052:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:67:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1053:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:68:6)
[Success][Witness] invariant confirmed: 3 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1057:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1057:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1057:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1059:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:74:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1060:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:75:6)
[Success][Witness] invariant confirmed: 1 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:79:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:79:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:79:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:81:2)
[Success][Witness] invariant confirmed: 3 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1068:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1068:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1068:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:82:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1070:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1071:6)
[Success][Witness] invariant confirmed: 1 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:90:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:90:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:90:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:92:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1077:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:93:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1078:6)
[Success][Witness] invariant confirmed: 3 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1082:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1082:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1082:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:99:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1084:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:100:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1085:6)
[Success][Witness] invariant confirmed: 1 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:104:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:104:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:104:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:106:2)
[Success][Witness] invariant confirmed: 3 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1093:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1093:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1093:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:107:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1095:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1096:6)
[Success][Witness] invariant confirmed: 1 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:115:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:115:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:115:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1102:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:117:2)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1103:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:118:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:124:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:125:6)
[Success][Witness] invariant confirmed: 1 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:129:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:129:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:129:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:131:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:132:6)
[Success][Witness] invariant confirmed: 1 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:140:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:140:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:140:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:142:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:143:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:149:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:150:6)
[Success][Witness] invariant confirmed: 1 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:154:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:154:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:154:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:156:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:157:6)
[Success][Witness] invariant confirmed: 1 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:165:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:165:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:165:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:167:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:168:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:174:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:175:6)
[Success][Witness] invariant confirmed: 1 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:179:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:179:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:179:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:181:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:182:6)
[Success][Witness] invariant confirmed: 1 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:190:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:190:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:190:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:192:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:193:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:199:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:200:6)
[Success][Witness] invariant confirmed: 1 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:204:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:204:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:204:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:206:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:207:6)
[Success][Witness] invariant confirmed: 1 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:215:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:215:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:215:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:217:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:218:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:224:2)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:225:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1338:2)
[Success][Witness] invariant confirmed: 3 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1339:6)
[Success][Witness] invariant confirmed: -3LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1339:6)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1339:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1341:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1342:6)
[Success][Witness] invariant confirmed: 4 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1346:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1346:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1346:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1348:2)

runtime: 00:03:21.444
vars: 971, evals: 867

|rho|=972
|called|=0
|stable|=972
|infl|=969
|wpoint|=0
|side_dep|=138
|side_infl|=271
|var_messages|=4
|rho_write|=267
|dep|=832
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_nondet_int (320) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:22:60-22:111
1	contexts for entry state of main (2011) on ../plain/id_build.i.p+nlh-reducer.c:13:2-2692:2

Memory statistics: total=2871.19MB, max=28.02MB, minor=2850.20MB, major=146.94MB, promoted=125.95MB
    minor collections=2796  major collections=210 compactions=0

[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1349:6)
[Success][Witness] invariant confirmed: 4 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1357:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1357:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1357:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1359:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1360:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1366:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1367:6)
[Success][Witness] invariant confirmed: 4 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1371:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1371:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1371:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1373:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1374:6)
[Success][Witness] invariant confirmed: 4 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1382:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1382:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1382:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1384:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1385:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1391:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1392:6)
[Success][Witness] invariant confirmed: 4 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1396:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1396:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1396:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1398:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1399:6)
[Success][Witness] invariant confirmed: 4 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1407:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1407:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1407:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1409:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1410:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1416:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1417:6)
[Success][Witness] invariant confirmed: 4 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1421:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1421:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1421:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1423:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1424:6)
[Success][Witness] invariant confirmed: 4 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1432:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1432:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1432:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1434:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1435:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1441:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1442:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:460:2)
[Success][Witness] invariant confirmed: 1 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:461:6)
[Success][Witness] invariant confirmed: -1LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:461:6)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:461:6)
[Success][Witness] invariant confirmed: 4 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1446:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1446:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1446:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:463:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1448:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:464:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1449:6)
[Success][Witness] invariant confirmed: 2 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:468:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:468:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:468:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:470:2)
[Success][Witness] invariant confirmed: 4 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1457:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1457:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1457:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:471:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1459:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1460:6)
[Success][Witness] invariant confirmed: 2 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:479:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:479:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:479:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:481:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1466:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:482:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1467:6)
[Success][Witness] invariant confirmed: 4 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1471:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1471:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1471:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:488:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1473:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:489:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1474:6)
[Success][Witness] invariant confirmed: 2 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:493:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:493:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:493:2)
[Success][Witness] invariant confirmed: 4 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1482:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1482:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1482:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:495:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1484:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:496:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1485:6)
[Success][Witness] invariant confirmed: 2 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:504:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:504:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:504:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1491:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:506:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1492:6)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:507:6)
[Success][Witness] invariant confirmed: 4 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1496:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1496:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1496:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1498:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:513:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1499:6)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:514:6)
[Success][Witness] invariant confirmed: 2 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:518:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:518:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:518:2)
[Success][Witness] invariant confirmed: 4 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1507:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1507:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1507:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:520:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1509:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:521:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1510:6)
[Success][Witness] invariant confirmed: 2 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:529:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:529:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:529:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:531:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1516:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:532:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1517:6)
[Success][Witness] invariant confirmed: 4 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1521:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1521:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1521:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:538:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1523:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:539:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1524:6)
[Success][Witness] invariant confirmed: 2 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:543:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:543:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:543:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:545:2)
[Success][Witness] invariant confirmed: 4 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1532:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1532:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1532:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:546:6)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1534:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1535:6)
[Success][Witness] invariant confirmed: 2 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:554:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:554:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:554:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1541:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:556:2)
[Success][Witness] invariant confirmed: -4LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1542:6)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:557:6)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:563:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:564:6)
[Success][Witness] invariant confirmed: 2 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:568:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:568:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:568:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:570:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:571:6)
[Success][Witness] invariant confirmed: 2 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:579:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:579:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:579:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:581:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:582:6)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:588:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:589:6)
[Success][Witness] invariant confirmed: 2 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:593:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:593:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:593:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:595:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:596:6)
[Success][Witness] invariant confirmed: 2 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:604:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:604:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:604:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:606:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:607:6)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:613:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:614:6)
[Success][Witness] invariant confirmed: 2 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:618:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:618:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:618:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:620:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:621:6)
[Success][Witness] invariant confirmed: 2 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:629:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:629:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:629:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:631:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:632:6)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:638:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:639:6)
[Success][Witness] invariant confirmed: 2 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:643:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:643:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:643:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:645:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:646:6)
[Success][Witness] invariant confirmed: 2 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:654:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:654:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:654:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:656:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:657:6)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:663:2)
[Success][Witness] invariant confirmed: -2LL + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:664:6)
[Success][Witness] invariant confirmed: 4 <= main__i (../plain/id_build.i.p+nlh-reducer.c:1758:2)
[Success][Witness] invariant confirmed: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1758:2)
[Warning][Witness] invariant unconfirmed: (-40LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1758:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1758:2)
[Success][Witness] invariant confirmed: 7LL - (long long )main__j >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1758:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1758:2)
[Success][Witness] invariant confirmed: main__i != 0 (../plain/id_build.i.p+nlh-reducer.c:1758:2)
[Warning][Witness] invariant unconfirmed: (-40LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1760:2)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1760:2)
[Success][Witness] invariant confirmed: 7LL - (long long )main__j >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1760:2)
[Warning][Witness] invariant unconfirmed: (-40LL + 8LL * (long long )main__i) + (long long )main__j >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1761:6)
[Success][Witness] invariant confirmed: (-1LL - (long long )main__i) + (long long )main__nlen >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1761:6)
[Success][Witness] invariant confirmed: 7LL - (long long )main__j >= 0LL (../plain/id_build.i.p+nlh-reducer.c:1761:6)
[Success][Witness] invariant confirmed: 4 <= main__i (../plain/id_build.i.p+nlh-reducer.c:1769:2)
[Success][Witness] invariant confirmed: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1769:2)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1769:2)
[Success][Witness] invariant confirmed: main__i != 0 (../plain/id_build.i.p+nlh-reducer.c:1769:2)
[Success][Witness] invariant confirmed: 4 <= main__i (../plain/id_build.i.p+nlh-reducer.c:1771:6)
[Success][Witness] invariant confirmed: 5 <= main__nlen (../plain/id_build.i.p+nlh-reducer.c:1771:6)
[Success][Witness] invariant confirmed: main__nlen != 0 (../plain/id_build.i.p+nlh-reducer.c:1771:6)
[Success][Witness] invariant confirmed: main__i != 0 (../plain/id_build.i.p+nlh-reducer.c:1771:6)
[Info][Witness] witness validation summary:
  confirmed: 442
  unconfirmed: 3
  refuted: 0
  error: 128
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 573
SV-COMP result: unknown

vars = 971    evals = 867    narrow_reuses = 3

Timings:
                                  cputime   walltime   allocated   count
Default                          205.690s   205.720s   2946.44MB      1×
  preprocess                         0.024s     0.023s      0.01MB      1×
  FrontC                             0.009s     0.009s      8.47MB      4×
  Cabs2cil                           0.011s     0.011s      9.92MB      4×
  mergeCIL                           0.004s     0.004s      3.88MB      1×
  analysis                         205.638s   205.669s   2917.53MB      1×
    createCFG                          0.006s     0.006s      3.22MB      1×
      handle                             0.001s     0.001s      0.88MB     33×
      iter_connect                       0.005s     0.005s      2.06MB     33×
        computeSCCs                        0.002s     0.002s      1.62MB     34×
    FrontC                             0.021s     0.023s      6.66MB    890×
    Cabs2cil                           0.196s     0.197s     92.36MB    890×
    global_inits                       0.001s     0.001s      0.28MB      1×
    solving                          200.078s   200.107s   2234.40MB      1×
      S.Dom.equal                        0.002s     0.005s      0.30MB    870×
      base unassume                      0.215s     0.215s     50.44MB     18×
      cheap_full_reach                   0.001s     0.001s      0.33MB      1×
      postsolver                        97.672s    97.688s    917.56MB      1×
        postsolver_iter                   97.670s    97.686s    916.94MB      1×
    warn_global                        0.008s     0.008s      4.16MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
