/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:14.403
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.340
vars: 14, evals: 6

|rho|=14
|called|=1
|stable|=14
|infl|=8
|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.16MB, max=8.82MB, minor=32.38MB, major=8.43MB, promoted=5.65MB
    minor collections=29  major collections=4 compactions=0


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

|rho|=193
|called|=149
|stable|=193
|infl|=39
|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=69.03MB, max=8.82MB, minor=66.24MB, major=9.05MB, promoted=6.27MB
    minor collections=58  major collections=8 compactions=0


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

|rho|=193
|called|=111
|stable|=193
|infl|=77
|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=198.96MB, max=8.82MB, minor=196.17MB, major=10.65MB, promoted=7.85MB
    minor collections=135  major collections=19 compactions=0


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

|rho|=193
|called|=76
|stable|=193
|infl|=112
|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=398.07MB, max=8.82MB, minor=395.28MB, major=12.93MB, promoted=10.13MB
    minor collections=248  major collections=30 compactions=0


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

|rho|=193
|called|=40
|stable|=193
|infl|=148
|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=643.52MB, max=8.82MB, minor=640.71MB, major=15.74MB, promoted=12.93MB
    minor collections=384  major collections=38 compactions=0


runtime: 00:01:10.452
vars: 194, evals: 184

|rho|=194
|called|=7
|stable|=194
|infl|=182
|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=927.15MB, max=8.82MB, minor=924.35MB, major=18.79MB, promoted=15.98MB
    minor collections=537  major collections=46 compactions=0


runtime: 00:01:20.461
vars: 257, evals: 232

|rho|=257
|called|=11
|stable|=257
|infl|=241
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=232
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=1150.34MB, max=10.14MB, minor=1147.53MB, major=21.28MB, promoted=18.47MB
    minor collections=659  major collections=51 compactions=0


runtime: 00:01:33.798
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.559
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.77MB, max=13.42MB, minor=1477.95MB, major=25.33MB, promoted=22.51MB
    minor collections=827  major collections=54 compactions=0


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

|rho|=350
|called|=244
|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=1541.22MB, max=13.42MB, minor=1538.40MB, major=25.88MB, promoted=23.06MB
    minor collections=865  major collections=61 compactions=0


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

|rho|=350
|called|=208
|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=1695.58MB, max=13.42MB, minor=1692.76MB, major=27.52MB, promoted=24.70MB
    minor collections=955  major collections=70 compactions=0


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

|rho|=350
|called|=171
|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=1921.23MB, max=13.42MB, minor=1918.41MB, major=29.90MB, promoted=27.08MB
    minor collections=1081  major collections=80 compactions=0


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

|rho|=350
|called|=135
|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=2197.96MB, max=13.42MB, minor=2195.14MB, major=32.83MB, promoted=30.02MB
    minor collections=1231  major collections=90 compactions=0


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

|rho|=350
|called|=110
|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=2407.65MB, max=13.42MB, minor=2404.83MB, major=34.96MB, promoted=32.15MB
    minor collections=1349  major collections=98 compactions=0


runtime: 00:02:40.619
vars: 389, evals: 733

|rho|=389
|called|=2
|stable|=378
|infl|=383
|wpoint|=0
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=338
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=4053.92MB, max=17.75MB, minor=4051.09MB, major=52.23MB, promoted=49.40MB
    minor collections=2149  major collections=105 compactions=0


runtime: 00:03:02.146
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.96MB, max=17.75MB, minor=4411.12MB, major=54.38MB, promoted=51.54MB
    minor collections=2349  major collections=113 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:11.648
vars: 395, evals: 750

|rho|=401
|called|=0
|stable|=401
|infl|=391
|wpoint|=0
|side_dep|=8
|side_infl|=6
|var_messages|=3
|rho_write|=6
|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=4416.79MB, max=17.75MB, minor=4413.95MB, major=54.65MB, promoted=51.81MB
    minor collections=2366  major collections=116 compactions=0


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

|rho|=414
|called|=0
|stable|=414
|infl|=391
|wpoint|=0
|side_dep|=21
|side_infl|=19
|var_messages|=3
|rho_write|=19
|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=4425.23MB, max=17.75MB, minor=4422.39MB, major=54.73MB, promoted=51.89MB
    minor collections=2388  major collections=118 compactions=0


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

|rho|=429
|called|=0
|stable|=429
|infl|=391
|wpoint|=0
|side_dep|=36
|side_infl|=34
|var_messages|=3
|rho_write|=34
|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=4446.92MB, max=17.75MB, minor=4444.08MB, major=54.90MB, promoted=52.06MB
    minor collections=2414  major collections=122 compactions=0


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

|rho|=444
|called|=0
|stable|=444
|infl|=391
|wpoint|=0
|side_dep|=51
|side_infl|=49
|var_messages|=3
|rho_write|=49
|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=4487.50MB, max=17.75MB, minor=4484.66MB, major=55.27MB, promoted=52.42MB
    minor collections=2444  major collections=126 compactions=0


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

|rho|=458
|called|=0
|stable|=458
|infl|=391
|wpoint|=0
|side_dep|=65
|side_infl|=63
|var_messages|=3
|rho_write|=63
|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=4542.96MB, max=17.75MB, minor=4540.12MB, major=55.85MB, promoted=53.01MB
    minor collections=2491  major collections=133 compactions=0


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

|rho|=472
|called|=0
|stable|=472
|infl|=391
|wpoint|=0
|side_dep|=79
|side_infl|=77
|var_messages|=3
|rho_write|=77
|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=4611.14MB, max=17.75MB, minor=4608.30MB, major=56.55MB, promoted=53.71MB
    minor collections=2545  major collections=141 compactions=0


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

|rho|=486
|called|=0
|stable|=486
|infl|=391
|wpoint|=0
|side_dep|=93
|side_infl|=91
|var_messages|=3
|rho_write|=91
|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=4691.14MB, max=17.75MB, minor=4688.30MB, major=57.35MB, promoted=54.50MB
    minor collections=2603  major collections=151 compactions=0


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

|rho|=500
|called|=0
|stable|=500
|infl|=391
|wpoint|=0
|side_dep|=107
|side_infl|=105
|var_messages|=3
|rho_write|=105
|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=4779.78MB, max=17.75MB, minor=4776.94MB, major=58.25MB, promoted=55.41MB
    minor collections=2666  major collections=162 compactions=0


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

|rho|=514
|called|=0
|stable|=514
|infl|=391
|wpoint|=0
|side_dep|=121
|side_infl|=119
|var_messages|=3
|rho_write|=119
|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=4876.46MB, max=17.75MB, minor=4873.60MB, major=59.24MB, promoted=56.38MB
    minor collections=2733  major collections=173 compactions=0


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

|rho|=527
|called|=0
|stable|=527
|infl|=391
|wpoint|=0
|side_dep|=134
|side_infl|=132
|var_messages|=3
|rho_write|=132
|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=4974.45MB, max=17.75MB, minor=4971.59MB, major=60.25MB, promoted=57.40MB
    minor collections=2799  major collections=187 compactions=0


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

|rho|=541
|called|=0
|stable|=541
|infl|=391
|wpoint|=0
|side_dep|=148
|side_infl|=146
|var_messages|=3
|rho_write|=146
|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=5087.90MB, max=17.75MB, minor=5085.04MB, major=61.43MB, promoted=58.57MB
    minor collections=2876  major collections=201 compactions=0


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

|rho|=554
|called|=0
|stable|=554
|infl|=391
|wpoint|=0
|side_dep|=161
|side_infl|=159
|var_messages|=3
|rho_write|=159
|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=5211.16MB, max=17.75MB, minor=5208.31MB, major=62.67MB, promoted=59.82MB
    minor collections=2957  major collections=214 compactions=0


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

|rho|=568
|called|=0
|stable|=568
|infl|=391
|wpoint|=0
|side_dep|=175
|side_infl|=173
|var_messages|=3
|rho_write|=173
|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=5344.84MB, max=17.75MB, minor=5341.98MB, major=63.93MB, promoted=61.07MB
    minor collections=3041  major collections=228 compactions=0


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

|rho|=581
|called|=0
|stable|=581
|infl|=391
|wpoint|=0
|side_dep|=192
|side_infl|=186
|var_messages|=3
|rho_write|=186
|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=5435.91MB, max=17.75MB, minor=5433.05MB, major=64.82MB, promoted=61.97MB
    minor collections=3107  major collections=240 compactions=0

[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (../plain/aiob_4.c.v+lhb-reducer.c:443:2-443:53)

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

|rho|=731
|called|=0
|stable|=731
|infl|=391
|wpoint|=0
|side_dep|=384
|side_infl|=337
|var_messages|=4
|rho_write|=336
|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=6424.46MB, max=17.75MB, minor=6421.60MB, major=73.20MB, promoted=70.34MB
    minor collections=3593  major collections=252 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: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:42.038
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=7191.49MB, max=17.75MB, minor=7188.59MB, major=78.06MB, promoted=75.16MB
    minor collections=3974  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                          349.661s   349.777s   8939.09MB      1×
  preprocess                         0.024s     0.022s      0.01MB      1×
  FrontC                             0.007s     0.007s      5.55MB      4×
  Cabs2cil                           0.007s     0.007s      7.28MB      4×
  mergeCIL                           0.003s     0.003s      3.66MB      1×
  analysis                         349.617s   349.733s   8917.24MB      1×
    createCFG                          0.005s     0.006s      1.55MB      1×
      handle                             0.004s     0.004s      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                          336.684s   336.767s   6454.20MB      1×
      S.Dom.equal                        0.003s     0.006s      0.26MB    751×
      cheap_full_reach                   0.001s     0.001s      0.19MB      1×
      postsolver                       169.523s   169.561s   2073.13MB      1×
        postsolver_iter                  169.517s   169.554s   2071.97MB      1×
    warn_global                        0.020s     0.020s      7.29MB      1×
    witness                           11.878s    11.911s   2096.16MB      1×
      determine                          0.001s     0.001s      0.96MB      1×
      write                             11.877s    11.911s   2095.20MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
