/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 cbmc/aiob_4.c.v+lhb-reducer.yml.witness.yml --witness.yaml.validate cbmc/aiob_4.c.v+lhb-reducer.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/aiob_4.c.v+lhb-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())) )

runtime: 00:00:15.693
vars: 13, evals: 6

|rho|=13
|called|=5
|stable|=13
|infl|=3
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=6
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=34.72MB, max=9.61MB, minor=31.89MB, major=8.59MB, promoted=5.76MB
    minor collections=22  major collections=3 compactions=0


runtime: 00:00:20.431
vars: 13, evals: 6

|rho|=13
|called|=3
|stable|=13
|infl|=5
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=6
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=35.21MB, max=9.61MB, minor=32.38MB, major=8.60MB, promoted=5.77MB
    minor collections=25  major collections=4 compactions=0


runtime: 00:00:30.456
vars: 193, evals: 184

|rho|=193
|called|=161
|stable|=193
|infl|=27
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=184
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=49.43MB, max=9.61MB, minor=46.60MB, major=9.02MB, promoted=6.19MB
    minor collections=48  major collections=6 compactions=0


runtime: 00:00:40.429
vars: 193, evals: 184

|rho|=193
|called|=121
|stable|=193
|infl|=67
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=184
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=156.59MB, max=9.61MB, minor=153.75MB, major=10.28MB, promoted=7.44MB
    minor collections=110  major collections=16 compactions=0


runtime: 00:00:50.562
vars: 193, evals: 184

|rho|=193
|called|=84
|stable|=193
|infl|=104
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=184
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=347.92MB, max=9.61MB, minor=345.07MB, major=12.48MB, promoted=9.63MB
    minor collections=222  major collections=29 compactions=0


runtime: 00:01:00.495
vars: 193, evals: 184

|rho|=193
|called|=48
|stable|=193
|infl|=140
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=184
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=589.28MB, max=9.61MB, minor=586.43MB, major=15.23MB, promoted=12.38MB
    minor collections=356  major collections=39 compactions=0


runtime: 00:01:10.593
vars: 193, evals: 184

|rho|=193
|called|=12
|stable|=193
|infl|=176
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=184
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=899.48MB, max=9.61MB, minor=896.63MB, major=18.61MB, promoted=15.75MB
    minor collections=522  major collections=50 compactions=0


runtime: 00:01:20.465
vars: 224, evals: 208

|rho|=224
|called|=13
|stable|=224
|infl|=206
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=208
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=1020.86MB, max=9.61MB, minor=1018.00MB, major=19.99MB, promoted=17.13MB
    minor collections=597  major collections=55 compactions=0


runtime: 00:01:36.838
vars: 350, evals: 581

|rho|=350
|called|=287
|stable|=339
|infl|=336
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=305
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=1487.72MB, max=12.71MB, minor=1484.85MB, major=25.57MB, promoted=22.70MB
    minor collections=826  major collections=58 compactions=0


runtime: 00:01:40.848
vars: 350, evals: 581

|rho|=350
|called|=286
|stable|=339
|infl|=336
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=305
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=1487.97MB, max=12.71MB, minor=1485.11MB, major=25.58MB, promoted=22.71MB
    minor collections=828  major collections=58 compactions=0


runtime: 00:01:50.607
vars: 350, evals: 581

|rho|=350
|called|=260
|stable|=339
|infl|=336
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=305
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=1509.16MB, max=12.71MB, minor=1506.29MB, major=25.76MB, promoted=22.90MB
    minor collections=851  major collections=62 compactions=0


runtime: 00:02:00.722
vars: 350, evals: 581

|rho|=350
|called|=221
|stable|=339
|infl|=336
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=305
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=1634.44MB, max=12.71MB, minor=1631.57MB, major=27.06MB, promoted=24.19MB
    minor collections=922  major collections=72 compactions=0


runtime: 00:02:10.609
vars: 350, evals: 581

|rho|=350
|called|=185
|stable|=339
|infl|=336
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=305
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=1828.71MB, max=12.71MB, minor=1825.84MB, major=29.10MB, promoted=26.23MB
    minor collections=1032  major collections=82 compactions=0


runtime: 00:02:20.729
vars: 350, evals: 581

|rho|=350
|called|=150
|stable|=339
|infl|=336
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=305
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=2080.28MB, max=12.71MB, minor=2077.42MB, major=31.78MB, promoted=28.91MB
    minor collections=1172  major collections=92 compactions=0


runtime: 00:02:31.228
vars: 350, evals: 581

|rho|=350
|called|=114
|stable|=339
|infl|=336
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=305
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=2403.83MB, max=12.71MB, minor=2400.96MB, major=35.10MB, promoted=32.23MB
    minor collections=1345  major collections=102 compactions=0


runtime: 00:02:40.654
vars: 350, evals: 581

|rho|=350
|called|=92
|stable|=339
|infl|=336
|wpoint|=1
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=305
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2

Memory statistics: total=2525.76MB, max=12.71MB, minor=2522.90MB, major=36.36MB, promoted=33.49MB
    minor collections=1418  major collections=107 compactions=0


runtime: 00:02:50.896
vars: 395, evals: 707

|rho|=395
|called|=2
|stable|=386
|infl|=391
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=3959.31MB, max=16.82MB, minor=3956.43MB, major=51.68MB, promoted=48.79MB
    minor collections=2119  major collections=113 compactions=0


runtime: 00:03:08.500
vars: 395, evals: 716

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=1
|side_infl|=1
|var_messages|=0
|rho_write|=1
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=4260.57MB, max=16.82MB, minor=4257.68MB, major=53.46MB, promoted=50.57MB
    minor collections=2280  major collections=119 compactions=0


runtime: 00:03:13.487
vars: 395, evals: 716

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=1
|side_infl|=1
|var_messages|=0
|rho_write|=1
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=4260.86MB, max=16.82MB, minor=4257.97MB, major=53.47MB, promoted=50.58MB
    minor collections=2284  major collections=119 compactions=0

[Info][Imprecise] Invalidating expressions: AddrOf(Var(main__Id_MCDC_112, NoOffset)) (../plain/aiob_4.c.v+lhb-reducer.c:163:2-163:42)
[Info][Unsound] Unknown address in {&main__Id_MCDC_112} has escaped. (../plain/aiob_4.c.v+lhb-reducer.c:163:2-163:42)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (../plain/aiob_4.c.v+lhb-reducer.c:163:2-163:42)

runtime: 00:03:20.968
vars: 395, evals: 716

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=4263.46MB, max=16.82MB, minor=4260.57MB, major=53.73MB, promoted=50.84MB
    minor collections=2300  major collections=121 compactions=0


runtime: 00:03:30.897
vars: 395, evals: 716

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=4272.14MB, max=16.82MB, minor=4269.25MB, major=53.81MB, promoted=50.92MB
    minor collections=2323  major collections=124 compactions=0


runtime: 00:03:40.974
vars: 395, evals: 716

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=4294.27MB, max=16.82MB, minor=4291.38MB, major=53.96MB, promoted=51.07MB
    minor collections=2348  major collections=128 compactions=0


runtime: 00:03:50.892
vars: 395, evals: 716

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=4334.18MB, max=16.82MB, minor=4331.29MB, major=54.32MB, promoted=51.43MB
    minor collections=2377  major collections=132 compactions=0


runtime: 00:04:01.155
vars: 395, evals: 716

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=4393.83MB, max=16.82MB, minor=4390.94MB, major=54.96MB, promoted=52.07MB
    minor collections=2428  major collections=140 compactions=0


runtime: 00:04:11.127
vars: 395, evals: 716

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=4464.48MB, max=16.82MB, minor=4461.59MB, major=55.66MB, promoted=52.77MB
    minor collections=2482  major collections=148 compactions=0


runtime: 00:04:21.221
vars: 395, evals: 716

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=4546.31MB, max=16.82MB, minor=4543.42MB, major=56.47MB, promoted=53.58MB
    minor collections=2540  major collections=158 compactions=0


runtime: 00:04:31.313
vars: 395, evals: 716

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=4636.46MB, max=16.82MB, minor=4633.57MB, major=57.38MB, promoted=54.49MB
    minor collections=2605  major collections=169 compactions=0


runtime: 00:04:41.575
vars: 395, evals: 716

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=4742.07MB, max=16.82MB, minor=4739.18MB, major=58.44MB, promoted=55.55MB
    minor collections=2676  major collections=181 compactions=0


runtime: 00:04:51.469
vars: 395, evals: 716

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=4842.47MB, max=16.82MB, minor=4839.58MB, major=59.45MB, promoted=56.56MB
    minor collections=2743  major collections=195 compactions=0


runtime: 00:05:01.757
vars: 395, evals: 716

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=4959.24MB, max=16.82MB, minor=4956.35MB, major=60.62MB, promoted=57.74MB
    minor collections=2824  major collections=209 compactions=0


runtime: 00:05:11.694
vars: 395, evals: 716

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=5090.20MB, max=16.82MB, minor=5087.31MB, major=61.89MB, promoted=59.00MB
    minor collections=2908  major collections=223 compactions=0


runtime: 00:05:21.826
vars: 395, evals: 716

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=4
|var_messages|=3
|rho_write|=3
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=5232.67MB, max=16.82MB, minor=5229.78MB, major=63.25MB, promoted=60.36MB
    minor collections=2998  major collections=238 compactions=0


runtime: 00:05:31.927
vars: 395, evals: 716

|rho|=396
|called|=0
|stable|=396
|infl|=391
|wpoint|=0
|side_dep|=10
|side_infl|=13
|var_messages|=3
|rho_write|=10
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=5336.25MB, max=16.82MB, minor=5333.36MB, major=64.26MB, promoted=61.37MB
    minor collections=3070  major collections=251 compactions=0

[Info][Witness] unassume invariant: (int )main__Id_MCDC_116 == 0 && (int )main__Id_MCDC_115 == 0 (../plain/aiob_4.c.v+lhb-reducer.c:414:2-414:47)
[Info][Witness] unassume invariant: (int )main__Id_MCDC_116 == 0 && (int )main__Id_MCDC_115 == 0 (../plain/aiob_4.c.v+lhb-reducer.c:447:2-447:47)

runtime: 00:05:41.992
vars: 395, evals: 716

|rho|=397
|called|=0
|stable|=397
|infl|=391
|wpoint|=0
|side_dep|=50
|side_infl|=102
|var_messages|=5
|rho_write|=84
|dep|=344
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of main (2009) on ../plain/aiob_4.c.v+lhb-reducer.c:136:2-636:2
1	contexts for entry state of reach_error (2000) on ../plain/aiob_4.c.v+lhb-reducer.c:4:1-4:88

Memory statistics: total=6323.54MB, max=16.82MB, minor=6320.65MB, major=72.31MB, promoted=69.42MB
    minor collections=3560  major collections=259 compactions=0

[Warning][Deadcode] Function 'main' has dead code:
  on line 194 (../plain/aiob_4.c.v+lhb-reducer.c:194-194)
  on line 220 (../plain/aiob_4.c.v+lhb-reducer.c:220-220)
  on line 246 (../plain/aiob_4.c.v+lhb-reducer.c:246-246)
  on line 272 (../plain/aiob_4.c.v+lhb-reducer.c:272-272)
  on line 298 (../plain/aiob_4.c.v+lhb-reducer.c:298-298)
  on line 324 (../plain/aiob_4.c.v+lhb-reducer.c:324-324)
  on line 350 (../plain/aiob_4.c.v+lhb-reducer.c:350-350)
  on line 376 (../plain/aiob_4.c.v+lhb-reducer.c:376-376)
  on line 402 (../plain/aiob_4.c.v+lhb-reducer.c:402-402)
  on line 435 (../plain/aiob_4.c.v+lhb-reducer.c:435-435)
  on line 472 (../plain/aiob_4.c.v+lhb-reducer.c:472-472)
  on line 479 (../plain/aiob_4.c.v+lhb-reducer.c:479-479)
  on line 491 (../plain/aiob_4.c.v+lhb-reducer.c:491-491)
  on line 496 (../plain/aiob_4.c.v+lhb-reducer.c:496-496)
  on line 508 (../plain/aiob_4.c.v+lhb-reducer.c:508-508)
  on line 513 (../plain/aiob_4.c.v+lhb-reducer.c:513-513)
  on line 525 (../plain/aiob_4.c.v+lhb-reducer.c:525-525)
  on line 530 (../plain/aiob_4.c.v+lhb-reducer.c:530-530)
  on line 542 (../plain/aiob_4.c.v+lhb-reducer.c:542-542)
  on line 547 (../plain/aiob_4.c.v+lhb-reducer.c:547-547)
  on line 559 (../plain/aiob_4.c.v+lhb-reducer.c:559-559)
  on line 564 (../plain/aiob_4.c.v+lhb-reducer.c:564-564)
  on line 576 (../plain/aiob_4.c.v+lhb-reducer.c:576-576)
  on line 581 (../plain/aiob_4.c.v+lhb-reducer.c:581-581)
  on line 593 (../plain/aiob_4.c.v+lhb-reducer.c:593-593)
  on line 598 (../plain/aiob_4.c.v+lhb-reducer.c:598-598)
  on line 610 (../plain/aiob_4.c.v+lhb-reducer.c:610-610)
  on line 615 (../plain/aiob_4.c.v+lhb-reducer.c:615-615)
  on line 627 (../plain/aiob_4.c.v+lhb-reducer.c:627-627)
  on line 632 (../plain/aiob_4.c.v+lhb-reducer.c:632-632)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 147
  dead: 30
  total lines: 177
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:364:6-364:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 < 42U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:366:6-366:21)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92___6 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:374:6-374:40)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:390:6-390:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 < 42U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:392:6-392:21)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92___7 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:400:6-400:40)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:182:6-182:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 < 42U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:184:6-184:21)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:192:6-192:40)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:423:6-423:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:208:6-208:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 < 42U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:210:6-210:21)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92___8 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:433:6-433:40)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92___0 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:218:6-218:40)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:234:6-234:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 < 42U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:236:6-236:21)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92___1 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:244:6-244:40)
[Warning][Deadcode][CWE-571] condition '__VERIFIER_assert__Id_MCDC_92___9 == 0' is always true (../plain/aiob_4.c.v+lhb-reducer.c:465:6-465:40)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:260:6-260:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 < 42U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:262:6-262:21)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92___2 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:270:6-270:40)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:286:6-286:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 < 42U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:288:6-288:21)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92___3 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:296:6-296:40)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:312:6-312:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 < 42U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:314:6-314:21)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92___4 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:322:6-322:40)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 >= 0U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:338:6-338:21)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_93 < 42U' is always true (../plain/aiob_4.c.v+lhb-reducer.c:340:6-340:21)
[Warning][Deadcode][CWE-570] condition '__VERIFIER_assert__Id_MCDC_92___5 == 0' is always false (../plain/aiob_4.c.v+lhb-reducer.c:348:6-348:40)
[Success][Witness] invariant confirmed: main__Id_MCDC_115 == (0) (../plain/aiob_4.c.v+lhb-reducer.c:157:2)
[Success][Witness] invariant confirmed: main__Id_MCDC_116 == (0) (../plain/aiob_4.c.v+lhb-reducer.c:158:2)
[Info][Witness] witness validation summary:
  confirmed: 2
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 2
SV-COMP result: unknown

vars = 395    evals = 716    narrow_reuses = 1

Timings:
                                  cputime   walltime   allocated   count
Default                          342.848s   342.961s   6326.18MB      1×
  preprocess                         0.025s     0.024s      0.01MB      1×
  FrontC                             0.006s     0.006s      5.55MB      4×
  Cabs2cil                           0.006s     0.006s      7.28MB      4×
  mergeCIL                           0.003s     0.003s      3.66MB      1×
  analysis                         342.803s   342.916s   6304.15MB      1×
    createCFG                          0.005s     0.005s      1.55MB      1×
      handle                             0.003s     0.004s      0.36MB     32×
      iter_connect                       0.001s     0.001s      1.02MB     32×
        computeSCCs                        0.001s     0.001s      0.74MB     33×
    FrontC                             0.001s     0.001s      0.03MB      4×
    Cabs2cil                           0.001s     0.001s      0.41MB      4×
    global_inits                       0.001s     0.001s      0.60MB      1×
    solving                          342.778s   342.890s   6292.64MB      1×
      S.Dom.equal                        0.003s     0.006s      0.25MB    717×
      base unassume                      0.002s     0.002s      3.65MB     12×
      cheap_full_reach                   0.001s     0.001s      0.19MB      1×
      postsolver                       170.056s   170.065s   2066.77MB      1×
        postsolver_iter                  170.056s   170.064s   2066.45MB      1×
    warn_global                        0.002s     0.002s      1.26MB      1×
    witness                            0.006s     0.006s      1.12MB      1×
      determine                          0.006s     0.006s      1.12MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
