/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint --conf conf/svcomp-yaml.json --enable dbg.timing.enabled --set 'ana.activated[+]' apron --set ana.apron.domain polyhedra --enable witness.enabled --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.093
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=33.07MB, max=8.82MB, minor=30.29MB, major=8.36MB, promoted=5.58MB
    minor collections=21  major collections=3 compactions=0


runtime: 00:00:20.777
vars: 14, evals: 6

|rho|=14
|called|=2
|stable|=14
|infl|=7
|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=33.87MB, max=8.82MB, minor=31.09MB, major=8.40MB, promoted=5.62MB
    minor collections=26  major collections=4 compactions=0


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

|rho|=193
|called|=155
|stable|=193
|infl|=33
|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=58.32MB, max=8.82MB, minor=55.53MB, major=8.90MB, promoted=6.11MB
    minor collections=52  major collections=7 compactions=0


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

|rho|=193
|called|=116
|stable|=193
|infl|=72
|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=180.15MB, max=8.82MB, minor=177.36MB, major=10.43MB, promoted=7.64MB
    minor collections=123  major collections=18 compactions=0


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

|rho|=193
|called|=80
|stable|=193
|infl|=108
|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=373.29MB, max=8.82MB, minor=370.50MB, major=12.64MB, promoted=9.85MB
    minor collections=235  major collections=29 compactions=0


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

|rho|=193
|called|=45
|stable|=193
|infl|=143
|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=611.12MB, max=8.82MB, minor=608.32MB, major=15.36MB, promoted=12.55MB
    minor collections=366  major collections=37 compactions=0


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

|rho|=193
|called|=9
|stable|=193
|infl|=179
|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=925.18MB, max=8.82MB, minor=922.37MB, major=18.77MB, promoted=15.96MB
    minor collections=533  major collections=45 compactions=0


runtime: 00:01:20.463
vars: 225, evals: 208

|rho|=225
|called|=10
|stable|=225
|infl|=210
|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=1039.59MB, max=8.82MB, minor=1036.78MB, major=20.06MB, promoted=17.25MB
    minor collections=605  major collections=50 compactions=0


runtime: 00:01:35.750
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=1479.82MB, max=13.42MB, minor=1477.00MB, major=25.31MB, promoted=22.50MB
    minor collections=820  major collections=53 compactions=0


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

|rho|=350
|called|=284
|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=1480.61MB, max=13.42MB, minor=1477.79MB, major=25.32MB, promoted=22.50MB
    minor collections=823  major collections=53 compactions=0


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

|rho|=350
|called|=255
|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=1513.11MB, max=13.42MB, minor=1510.29MB, major=25.55MB, promoted=22.73MB
    minor collections=850  major collections=58 compactions=0


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

|rho|=350
|called|=218
|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=1644.67MB, max=13.42MB, minor=1641.85MB, major=26.99MB, promoted=24.17MB
    minor collections=925  major collections=67 compactions=0


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

|rho|=350
|called|=182
|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=1848.51MB, max=13.42MB, minor=1845.69MB, major=29.14MB, promoted=26.33MB
    minor collections=1039  major collections=77 compactions=0


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

|rho|=350
|called|=146
|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=2097.36MB, max=13.42MB, minor=2094.54MB, major=31.81MB, promoted=28.99MB
    minor collections=1179  major collections=87 compactions=0


runtime: 00:02:30.669
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=2395.15MB, max=13.42MB, minor=2392.33MB, major=34.84MB, promoted=32.02MB
    minor collections=1338  major collections=97 compactions=0


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

|rho|=350
|called|=85
|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=2550.94MB, max=13.42MB, minor=2548.12MB, major=36.42MB, promoted=33.60MB
    minor collections=1429  major collections=102 compactions=0


runtime: 00:02:50.689
vars: 395, evals: 741

|rho|=395
|called|=1
|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=4113.84MB, max=17.75MB, minor=4111.01MB, major=52.68MB, promoted=49.85MB
    minor collections=2195  major collections=109 compactions=0


runtime: 00:03:07.873
vars: 395, evals: 750

|rho|=397
|called|=0
|stable|=397
|infl|=391
|wpoint|=0
|side_dep|=2
|side_infl|=2
|var_messages|=0
|rho_write|=2
|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=4413.97MB, max=17.75MB, minor=4411.13MB, major=54.42MB, promoted=51.58MB
    minor collections=2351  major collections=114 compactions=0


runtime: 00:03:12.118
vars: 395, evals: 750

|rho|=398
|called|=0
|stable|=398
|infl|=391
|wpoint|=0
|side_dep|=3
|side_infl|=3
|var_messages|=0
|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=4414.29MB, max=17.75MB, minor=4411.45MB, major=54.43MB, promoted=51.59MB
    minor collections=2355  major collections=114 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.759
vars: 395, evals: 750

|rho|=405
|called|=0
|stable|=405
|infl|=391
|wpoint|=0
|side_dep|=12
|side_infl|=10
|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=4418.34MB, max=17.75MB, minor=4415.50MB, major=54.71MB, promoted=51.87MB
    minor collections=2375  major collections=117 compactions=0


runtime: 00:03:30.766
vars: 395, evals: 750

|rho|=419
|called|=0
|stable|=419
|infl|=391
|wpoint|=0
|side_dep|=26
|side_infl|=24
|var_messages|=3
|rho_write|=24
|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=4431.07MB, max=17.75MB, minor=4428.23MB, major=54.83MB, promoted=51.99MB
    minor collections=2400  major collections=120 compactions=0


runtime: 00:03:40.915
vars: 395, evals: 750

|rho|=434
|called|=0
|stable|=434
|infl|=391
|wpoint|=0
|side_dep|=41
|side_infl|=39
|var_messages|=3
|rho_write|=39
|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=4458.07MB, max=17.75MB, minor=4455.23MB, major=55.02MB, promoted=52.18MB
    minor collections=2427  major collections=124 compactions=0


runtime: 00:03:51.007
vars: 395, evals: 750

|rho|=449
|called|=0
|stable|=449
|infl|=391
|wpoint|=0
|side_dep|=56
|side_infl|=54
|var_messages|=3
|rho_write|=54
|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=4505.88MB, max=17.75MB, minor=4503.04MB, major=55.51MB, promoted=52.67MB
    minor collections=2462  major collections=129 compactions=0


runtime: 00:04:00.985
vars: 395, evals: 750

|rho|=463
|called|=0
|stable|=463
|infl|=391
|wpoint|=0
|side_dep|=70
|side_infl|=68
|var_messages|=3
|rho_write|=68
|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=4565.28MB, max=17.75MB, minor=4562.44MB, major=56.13MB, promoted=53.29MB
    minor collections=2511  major collections=136 compactions=0


runtime: 00:04:11.151
vars: 395, evals: 750

|rho|=477
|called|=0
|stable|=477
|infl|=391
|wpoint|=0
|side_dep|=84
|side_infl|=82
|var_messages|=3
|rho_write|=82
|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=4638.50MB, max=17.75MB, minor=4635.66MB, major=56.86MB, promoted=54.02MB
    minor collections=2567  major collections=145 compactions=0


runtime: 00:04:21.228
vars: 395, evals: 750

|rho|=491
|called|=0
|stable|=491
|infl|=391
|wpoint|=0
|side_dep|=98
|side_infl|=96
|var_messages|=3
|rho_write|=96
|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=4721.98MB, max=17.75MB, minor=4719.14MB, major=57.70MB, promoted=54.86MB
    minor collections=2627  major collections=155 compactions=0


runtime: 00:04:31.219
vars: 395, evals: 750

|rho|=505
|called|=0
|stable|=505
|infl|=391
|wpoint|=0
|side_dep|=112
|side_infl|=110
|var_messages|=3
|rho_write|=110
|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=4813.28MB, max=17.75MB, minor=4810.43MB, major=58.63MB, promoted=55.79MB
    minor collections=2690  major collections=166 compactions=0


runtime: 00:04:41.425
vars: 395, evals: 750

|rho|=519
|called|=0
|stable|=519
|infl|=391
|wpoint|=0
|side_dep|=126
|side_infl|=124
|var_messages|=3
|rho_write|=124
|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=4913.11MB, max=17.75MB, minor=4910.25MB, major=59.67MB, promoted=56.81MB
    minor collections=2759  major collections=178 compactions=0


runtime: 00:04:51.489
vars: 395, evals: 750

|rho|=533
|called|=0
|stable|=533
|infl|=391
|wpoint|=0
|side_dep|=140
|side_infl|=138
|var_messages|=3
|rho_write|=138
|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=5021.05MB, max=17.75MB, minor=5018.19MB, major=60.78MB, promoted=57.92MB
    minor collections=2830  major collections=193 compactions=0


runtime: 00:05:01.547
vars: 395, evals: 750

|rho|=547
|called|=0
|stable|=547
|infl|=391
|wpoint|=0
|side_dep|=154
|side_infl|=152
|var_messages|=3
|rho_write|=152
|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=5140.55MB, max=17.75MB, minor=5137.70MB, major=62.00MB, promoted=59.14MB
    minor collections=2912  major collections=207 compactions=0


runtime: 00:05:11.704
vars: 395, evals: 750

|rho|=561
|called|=0
|stable|=561
|infl|=391
|wpoint|=0
|side_dep|=168
|side_infl|=166
|var_messages|=3
|rho_write|=166
|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=5273.25MB, max=17.75MB, minor=5270.40MB, major=63.29MB, promoted=60.43MB
    minor collections=2996  major collections=221 compactions=0


runtime: 00:05:21.883
vars: 395, evals: 750

|rho|=574
|called|=0
|stable|=574
|infl|=391
|wpoint|=0
|side_dep|=182
|side_infl|=179
|var_messages|=3
|rho_write|=179
|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=5388.81MB, max=17.75MB, minor=5385.95MB, major=64.39MB, promoted=61.54MB
    minor collections=3074  major collections=234 compactions=0


runtime: 00:05:31.771
vars: 395, evals: 750

|rho|=595
|called|=0
|stable|=595
|infl|=391
|wpoint|=0
|side_dep|=211
|side_infl|=200
|var_messages|=3
|rho_write|=200
|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=5516.30MB, max=17.75MB, minor=5513.44MB, major=65.65MB, promoted=62.79MB
    minor collections=3155  major collections=247 compactions=0

[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/aiob_4.c.v+lhb-reducer.c:443:2-443:53)
[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:423:6-423: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-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: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: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___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 '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)
SV-COMP result: unknown

runtime: 00:05:41.887
vars: 395, evals: 750

|rho|=737
|called|=0
|stable|=737
|infl|=391
|wpoint|=0
|side_dep|=391
|side_infl|=344
|var_messages|=4
|rho_write|=343
|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=6552.01MB, max=17.75MB, minor=6549.12MB, major=74.38MB, promoted=71.49MB
    minor collections=3668  major collections=255 compactions=0


runtime: 00:05:51.900
vars: 395, evals: 750

|rho|=737
|called|=0
|stable|=737
|infl|=391
|wpoint|=0
|side_dep|=391
|side_infl|=344
|var_messages|=4
|rho_write|=343
|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=7880.33MB, max=17.75MB, minor=7877.44MB, major=82.22MB, promoted=79.32MB
    minor collections=4302  major collections=257 compactions=0

[Info][Witness] witness generation summary:
  total generation entries: 628

vars = 395    evals = 750    narrow_reuses = 1

Timings:
                                  cputime   walltime   allocated   count
Default                          354.645s   354.687s   8939.14MB      1×
  preprocess                         0.027s     0.047s      0.01MB      1×
  FrontC                             0.009s     0.009s      5.55MB      4×
  Cabs2cil                           0.007s     0.007s      7.28MB      4×
  mergeCIL                           0.003s     0.003s      3.66MB      1×
  analysis                         354.594s   354.615s   8917.29MB      1×
    createCFG                          0.005s     0.005s      1.55MB      1×
      handle                             0.003s     0.003s      0.36MB     32×
      iter_connect                       0.002s     0.002s      1.02MB     32×
        computeSCCs                        0.001s     0.001s      0.74MB     33×
    global_inits                       0.001s     0.001s      0.57MB      1×
    solving                          341.234s   341.255s   6454.21MB      1×
      S.Dom.equal                        0.003s     0.006s      0.26MB    751×
      cheap_full_reach                   0.001s     0.001s      0.19MB      1×
      postsolver                       169.470s   169.478s   2073.13MB      1×
        postsolver_iter                  169.461s   169.469s   2071.97MB      1×
    warn_global                        0.008s     0.008s      7.29MB      1×
    witness                           12.308s    12.309s   2096.18MB      1×
      determine                          0.001s     0.001s      0.96MB      1×
      write                             12.308s    12.309s   2095.23MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
