/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-self/ourtool.2023-02-03_08-10-40.files/ourtool/cohencu-ll_valuebound50.yml/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../results/st-cross-self/ourtool.2023-02-03_08-10-40.files/ourtool/cohencu-ll_valuebound50.yml/witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/cohencu-ll_valuebound50.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: 0LL <= n (../plain/cohencu-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: n <= 32768LL (../plain/cohencu-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: 0LL <= n (../plain/cohencu-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: n <= 32768LL (../plain/cohencu-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: 0LL <= n (../plain/cohencu-ll_valuebound50.c:36:9)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/cohencu-ll_valuebound50.c:36:9)
[Warning][Witness] couldn't locate invariant: n <= 32768LL (../plain/cohencu-ll_valuebound50.c:36:9)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound50.c:36:9)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/cohencu-ll_valuebound50.c:37:2)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound50.c:37:2)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:37:2)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:37:2)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound50.c:37:2)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound50.c:38:2)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:38:2)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:38:2)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound50.c:38:2)
[Warning][Witness] couldn't locate invariant: (short)0 <= a (../plain/cohencu-ll_valuebound50.c:39:13)
[Warning][Witness] couldn't locate invariant: 0LL <= n (../plain/cohencu-ll_valuebound50.c:39:13)
[Warning][Witness] couldn't locate invariant: n <= 32768LL (../plain/cohencu-ll_valuebound50.c:39:13)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound50.c:39:13)
[Warning][Witness] couldn't locate invariant: 0LL <= n (../plain/cohencu-ll_valuebound50.c:42:9)
[Warning][Witness] couldn't locate invariant: n <= 32767LL (../plain/cohencu-ll_valuebound50.c:42:9)
[Warning][Witness] couldn't locate invariant: (long long )a - n >= 0LL (../plain/cohencu-ll_valuebound50.c:42:9)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/cohencu-ll_valuebound50.c:43:9)
[Warning][Witness] couldn't locate invariant: 1LL <= n (../plain/cohencu-ll_valuebound50.c:43:9)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound50.c:43:9)
[Warning][Witness] couldn't locate invariant: n <= 32768LL (../plain/cohencu-ll_valuebound50.c:43:9)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound50.c:43:9)
[Warning][Witness] couldn't locate invariant: 1LL <= x (../plain/cohencu-ll_valuebound50.c:44:9)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound50.c:44:9)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:44:9)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:44:9)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound50.c:44:9)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:45:9)
[Warning][Witness] couldn't locate invariant: 7LL <= y (../plain/cohencu-ll_valuebound50.c:45:9)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:45:9)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound50.c:45:9)
[Warning][Witness] couldn't locate invariant: 1LL <= n (../plain/cohencu-ll_valuebound50.c:48:5)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:48:5)
[Warning][Witness] couldn't locate invariant: n <= 32768LL (../plain/cohencu-ll_valuebound50.c:48:5)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:48:5)
[Warning][Witness] couldn't locate invariant: n != 0LL (../plain/cohencu-ll_valuebound50.c:48:5)
[Warning][Witness] couldn't locate invariant: (short)0 <= a (../plain/cohencu-ll_valuebound50.c:49:5)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/cohencu-ll_valuebound50.c:49:5)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:49:5)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:49:5)
[Warning][Witness] couldn't locate invariant: (short)0 <= a (../plain/cohencu-ll_valuebound50.c:50:5)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound50.c:50:5)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:50:5)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:50:5)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/cohencu-ll_valuebound50.c:51:5)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound50.c:51:5)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:51:5)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:51:5)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound50.c:52:5)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:52:5)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:52:5)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/cohencu-ll_valuebound50.c:53:5)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound50.c:53:5)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:53:5)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:53:5)

runtime: 00:00:10.089
vars: 57, evals: 1513

|rho|=57
|called|=14
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=803.02MB, max=12.37MB, minor=800.01MB, major=16.44MB, promoted=13.44MB
    minor collections=384  major collections=6 compactions=0


runtime: 00:00:20.170
vars: 57, evals: 1899

|rho|=57
|called|=17
|stable|=54
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=997.10MB, max=12.37MB, minor=994.09MB, major=18.32MB, promoted=15.31MB
    minor collections=477  major collections=7 compactions=0


runtime: 00:00:30.118
vars: 57, evals: 2154

|rho|=57
|called|=16
|stable|=54
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1128.86MB, max=12.37MB, minor=1125.84MB, major=19.50MB, promoted=16.49MB
    minor collections=539  major collections=7 compactions=0


runtime: 00:00:40.182
vars: 57, evals: 2352

|rho|=57
|called|=18
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1230.23MB, max=12.37MB, minor=1227.20MB, major=20.52MB, promoted=17.50MB
    minor collections=588  major collections=7 compactions=0


runtime: 00:00:50.142
vars: 57, evals: 2511

|rho|=57
|called|=12
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1314.76MB, max=12.37MB, minor=1311.74MB, major=21.33MB, promoted=18.31MB
    minor collections=629  major collections=8 compactions=0


runtime: 00:01:00.168
vars: 57, evals: 2657

|rho|=57
|called|=18
|stable|=53
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1388.47MB, max=12.37MB, minor=1385.44MB, major=22.02MB, promoted=18.99MB
    minor collections=664  major collections=8 compactions=0


runtime: 00:01:10.221
vars: 57, evals: 2777

|rho|=57
|called|=17
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1450.91MB, max=12.37MB, minor=1447.87MB, major=22.56MB, promoted=19.52MB
    minor collections=693  major collections=8 compactions=0


runtime: 00:01:20.171
vars: 57, evals: 2890

|rho|=57
|called|=17
|stable|=57
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1510.89MB, max=12.37MB, minor=1507.85MB, major=23.08MB, promoted=20.05MB
    minor collections=722  major collections=8 compactions=0


runtime: 00:01:30.475
vars: 57, evals: 2991

|rho|=57
|called|=17
|stable|=52
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1563.43MB, max=12.37MB, minor=1560.39MB, major=23.58MB, promoted=20.54MB
    minor collections=747  major collections=8 compactions=0


runtime: 00:01:40.516
vars: 57, evals: 3082

|rho|=57
|called|=17
|stable|=53
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1609.88MB, max=12.37MB, minor=1606.84MB, major=23.95MB, promoted=20.91MB
    minor collections=769  major collections=8 compactions=0


runtime: 00:01:50.269
vars: 57, evals: 3167

|rho|=57
|called|=18
|stable|=53
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1653.51MB, max=12.37MB, minor=1650.47MB, major=24.33MB, promoted=21.29MB
    minor collections=790  major collections=8 compactions=0


runtime: 00:02:00.244
vars: 57, evals: 3241

|rho|=57
|called|=18
|stable|=57
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1694.08MB, max=12.37MB, minor=1691.04MB, major=24.71MB, promoted=21.66MB
    minor collections=810  major collections=9 compactions=0


runtime: 00:02:10.221
vars: 57, evals: 3315

|rho|=57
|called|=18
|stable|=57
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1731.68MB, max=12.37MB, minor=1728.63MB, major=25.05MB, promoted=22.00MB
    minor collections=828  major collections=9 compactions=0


runtime: 00:02:20.660
vars: 57, evals: 3390

|rho|=57
|called|=17
|stable|=54
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1767.30MB, max=12.37MB, minor=1764.25MB, major=25.32MB, promoted=22.27MB
    minor collections=845  major collections=9 compactions=0


runtime: 00:02:30.252
vars: 57, evals: 3453

|rho|=57
|called|=18
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1796.48MB, max=12.37MB, minor=1793.43MB, major=25.60MB, promoted=22.55MB
    minor collections=859  major collections=9 compactions=0


runtime: 00:02:40.362
vars: 57, evals: 3499

|rho|=57
|called|=8
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1823.65MB, max=12.37MB, minor=1820.60MB, major=25.82MB, promoted=22.77MB
    minor collections=872  major collections=9 compactions=0


runtime: 00:02:50.373
vars: 57, evals: 3554

|rho|=57
|called|=17
|stable|=52
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1850.22MB, max=12.37MB, minor=1847.16MB, major=26.01MB, promoted=22.96MB
    minor collections=884  major collections=9 compactions=0


runtime: 00:03:00.269
vars: 57, evals: 3606

|rho|=57
|called|=18
|stable|=53
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1873.83MB, max=12.37MB, minor=1870.77MB, major=26.21MB, promoted=23.16MB
    minor collections=896  major collections=9 compactions=0


runtime: 00:03:12.213
vars: 57, evals: 3630

|rho|=57
|called|=13
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1887.95MB, max=12.37MB, minor=1884.89MB, major=26.32MB, promoted=23.26MB
    minor collections=902  major collections=9 compactions=0


runtime: 00:03:23.210
vars: 57, evals: 3630

|rho|=57
|called|=8
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1889.92MB, max=12.37MB, minor=1886.86MB, major=26.34MB, promoted=23.28MB
    minor collections=903  major collections=9 compactions=0


runtime: 00:03:30.570
vars: 57, evals: 3667

|rho|=57
|called|=14
|stable|=55
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1904.55MB, max=12.37MB, minor=1901.49MB, major=26.46MB, promoted=23.40MB
    minor collections=910  major collections=9 compactions=0


runtime: 00:03:40.619
vars: 57, evals: 3705

|rho|=57
|called|=17
|stable|=54
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1920.63MB, max=14.22MB, minor=1917.57MB, major=26.63MB, promoted=23.57MB
    minor collections=918  major collections=9 compactions=0


runtime: 00:03:50.676
vars: 57, evals: 3744

|rho|=57
|called|=17
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1943.32MB, max=14.22MB, minor=1940.26MB, major=26.85MB, promoted=23.78MB
    minor collections=929  major collections=9 compactions=0


runtime: 00:04:00.852
vars: 57, evals: 3790

|rho|=57
|called|=18
|stable|=54
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1965.30MB, max=14.22MB, minor=1962.24MB, major=26.98MB, promoted=23.92MB
    minor collections=939  major collections=9 compactions=0


runtime: 00:04:10.337
vars: 57, evals: 3818

|rho|=57
|called|=18
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1980.72MB, max=14.22MB, minor=1977.65MB, major=27.17MB, promoted=24.10MB
    minor collections=947  major collections=9 compactions=0


runtime: 00:04:22.373
vars: 57, evals: 3829

|rho|=57
|called|=18
|stable|=53
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1984.52MB, max=14.22MB, minor=1981.46MB, major=27.18MB, promoted=24.11MB
    minor collections=948  major collections=9 compactions=0


runtime: 00:04:33.175
vars: 57, evals: 3844

|rho|=57
|called|=18
|stable|=55
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1991.08MB, max=14.22MB, minor=1988.01MB, major=27.21MB, promoted=24.14MB
    minor collections=951  major collections=9 compactions=0


runtime: 00:04:40.416
vars: 57, evals: 3853

|rho|=57
|called|=17
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1996.37MB, max=14.22MB, minor=1993.31MB, major=27.26MB, promoted=24.20MB
    minor collections=954  major collections=9 compactions=0


runtime: 00:04:57.875
vars: 57, evals: 3853

|rho|=57
|called|=13
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1999.14MB, max=14.22MB, minor=1996.07MB, major=27.29MB, promoted=24.22MB
    minor collections=955  major collections=9 compactions=0


runtime: 00:05:01.061
vars: 57, evals: 3853

|rho|=57
|called|=12
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1999.52MB, max=14.22MB, minor=1996.46MB, major=27.31MB, promoted=24.24MB
    minor collections=956  major collections=9 compactions=0


runtime: 00:05:36.732
vars: 57, evals: 3853

|rho|=57
|called|=8
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2001.11MB, max=14.22MB, minor=1998.05MB, major=27.31MB, promoted=24.24MB
    minor collections=956  major collections=9 compactions=0


runtime: 00:06:03.601
vars: 57, evals: 3853

|rho|=57
|called|=8
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2001.19MB, max=14.22MB, minor=1998.12MB, major=27.31MB, promoted=24.24MB
    minor collections=956  major collections=9 compactions=0


runtime: 00:06:12.187
vars: 57, evals: 3853

|rho|=57
|called|=8
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2001.31MB, max=14.22MB, minor=1998.24MB, major=27.31MB, promoted=24.24MB
    minor collections=956  major collections=9 compactions=0


runtime: 00:06:21.736
vars: 57, evals: 3875

|rho|=57
|called|=18
|stable|=53
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2006.62MB, max=14.22MB, minor=2003.56MB, major=27.38MB, promoted=24.32MB
    minor collections=959  major collections=9 compactions=0


runtime: 00:06:31.108
vars: 57, evals: 3890

|rho|=57
|called|=15
|stable|=55
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2015.27MB, max=14.22MB, minor=2012.21MB, major=27.45MB, promoted=24.39MB
    minor collections=963  major collections=9 compactions=0


runtime: 00:06:40.574
vars: 57, evals: 3899

|rho|=57
|called|=13
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2021.22MB, max=14.22MB, minor=2018.15MB, major=27.50MB, promoted=24.44MB
    minor collections=966  major collections=9 compactions=0


runtime: 00:06:51.525
vars: 57, evals: 3899

|rho|=57
|called|=8
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2023.15MB, max=14.22MB, minor=2020.08MB, major=27.56MB, promoted=24.49MB
    minor collections=967  major collections=9 compactions=0


runtime: 00:07:00.714
vars: 57, evals: 3928

|rho|=57
|called|=17
|stable|=54
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2032.05MB, max=14.22MB, minor=2028.99MB, major=27.63MB, promoted=24.56MB
    minor collections=971  major collections=9 compactions=0


runtime: 00:07:12.208
vars: 57, evals: 3945

|rho|=57
|called|=8
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2045.10MB, max=14.22MB, minor=2042.03MB, major=27.73MB, promoted=24.66MB
    minor collections=977  major collections=9 compactions=0


runtime: 00:07:20.601
vars: 57, evals: 3956

|rho|=57
|called|=8
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2052.24MB, max=14.22MB, minor=2049.17MB, major=27.82MB, promoted=24.75MB
    minor collections=981  major collections=9 compactions=0


runtime: 00:07:31.252
vars: 57, evals: 3995

|rho|=57
|called|=18
|stable|=57
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2069.69MB, max=14.22MB, minor=2066.62MB, major=27.96MB, promoted=24.89MB
    minor collections=989  major collections=9 compactions=0


runtime: 00:07:40.820
vars: 57, evals: 4021

|rho|=57
|called|=18
|stable|=55
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2080.04MB, max=14.22MB, minor=2076.97MB, major=28.03MB, promoted=24.96MB
    minor collections=994  major collections=9 compactions=0


runtime: 00:07:50.700
vars: 57, evals: 4030

|rho|=57
|called|=11
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2088.66MB, max=14.22MB, minor=2085.59MB, major=28.08MB, promoted=25.01MB
    minor collections=998  major collections=9 compactions=0


runtime: 00:08:00.778
vars: 57, evals: 4041

|rho|=57
|called|=18
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2091.67MB, max=14.22MB, minor=2088.60MB, major=28.17MB, promoted=25.10MB
    minor collections=1000  major collections=10 compactions=0


runtime: 00:08:14.784
vars: 57, evals: 4052

|rho|=57
|called|=18
|stable|=53
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2095.48MB, max=14.22MB, minor=2092.41MB, major=28.21MB, promoted=25.13MB
    minor collections=1002  major collections=10 compactions=0


runtime: 00:08:23.959
vars: 57, evals: 4059

|rho|=57
|called|=18
|stable|=54
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2098.33MB, max=14.22MB, minor=2095.26MB, major=28.22MB, promoted=25.15MB
    minor collections=1003  major collections=10 compactions=0


runtime: 00:08:30.639
vars: 57, evals: 4059

|rho|=57
|called|=15
|stable|=54
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2100.34MB, max=14.22MB, minor=2097.27MB, major=28.22MB, promoted=25.15MB
    minor collections=1004  major collections=10 compactions=0


runtime: 00:08:40.787
vars: 57, evals: 4067

|rho|=57
|called|=16
|stable|=55
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2103.39MB, max=14.22MB, minor=2100.32MB, major=28.26MB, promoted=25.18MB
    minor collections=1006  major collections=10 compactions=0


runtime: 00:08:52.874
vars: 57, evals: 4076

|rho|=57
|called|=18
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2106.69MB, max=14.22MB, minor=2103.62MB, major=28.28MB, promoted=25.21MB
    minor collections=1007  major collections=10 compactions=0


runtime: 00:09:00.797
vars: 57, evals: 4076

|rho|=57
|called|=15
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2108.99MB, max=14.22MB, minor=2105.92MB, major=28.32MB, promoted=25.24MB
    minor collections=1009  major collections=10 compactions=0

