/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_valuebound2.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_valuebound2.yml/witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/cohencu-ll_valuebound2.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_valuebound2.c:34:9)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound2.c:34:9)
[Warning][Witness] couldn't locate invariant: n <= 32768LL (../plain/cohencu-ll_valuebound2.c:34:9)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound2.c:34:9)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound2.c:34:9)
[Warning][Witness] couldn't locate invariant: 0LL <= n (../plain/cohencu-ll_valuebound2.c:35:9)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound2.c:35:9)
[Warning][Witness] couldn't locate invariant: n <= 32768LL (../plain/cohencu-ll_valuebound2.c:35:9)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound2.c:35:9)
[Warning][Witness] couldn't locate invariant: 0LL <= n (../plain/cohencu-ll_valuebound2.c:36:9)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/cohencu-ll_valuebound2.c:36:9)
[Warning][Witness] couldn't locate invariant: n <= 32768LL (../plain/cohencu-ll_valuebound2.c:36:9)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound2.c:36:9)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/cohencu-ll_valuebound2.c:37:2)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound2.c:37:2)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound2.c:37:2)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound2.c:37:2)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound2.c:37:2)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound2.c:38:2)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound2.c:38:2)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound2.c:38:2)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound2.c:38:2)
[Warning][Witness] couldn't locate invariant: (short)0 <= a (../plain/cohencu-ll_valuebound2.c:39:13)
[Warning][Witness] couldn't locate invariant: 0LL <= n (../plain/cohencu-ll_valuebound2.c:39:13)
[Warning][Witness] couldn't locate invariant: n <= 32768LL (../plain/cohencu-ll_valuebound2.c:39:13)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound2.c:39:13)
[Warning][Witness] couldn't locate invariant: 0LL <= n (../plain/cohencu-ll_valuebound2.c:42:9)
[Warning][Witness] couldn't locate invariant: n <= 32767LL (../plain/cohencu-ll_valuebound2.c:42:9)
[Warning][Witness] couldn't locate invariant: (long long )a - n >= 0LL (../plain/cohencu-ll_valuebound2.c:42:9)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/cohencu-ll_valuebound2.c:43:9)
[Warning][Witness] couldn't locate invariant: 1LL <= n (../plain/cohencu-ll_valuebound2.c:43:9)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound2.c:43:9)
[Warning][Witness] couldn't locate invariant: n <= 32768LL (../plain/cohencu-ll_valuebound2.c:43:9)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound2.c:43:9)
[Warning][Witness] couldn't locate invariant: 1LL <= x (../plain/cohencu-ll_valuebound2.c:44:9)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound2.c:44:9)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound2.c:44:9)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound2.c:44:9)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound2.c:44:9)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound2.c:45:9)
[Warning][Witness] couldn't locate invariant: 7LL <= y (../plain/cohencu-ll_valuebound2.c:45:9)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound2.c:45:9)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound2.c:45:9)
[Warning][Witness] couldn't locate invariant: 1LL <= n (../plain/cohencu-ll_valuebound2.c:48:5)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound2.c:48:5)
[Warning][Witness] couldn't locate invariant: n <= 32768LL (../plain/cohencu-ll_valuebound2.c:48:5)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound2.c:48:5)
[Warning][Witness] couldn't locate invariant: n != 0LL (../plain/cohencu-ll_valuebound2.c:48:5)
[Warning][Witness] couldn't locate invariant: (short)0 <= a (../plain/cohencu-ll_valuebound2.c:49:5)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/cohencu-ll_valuebound2.c:49:5)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound2.c:49:5)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound2.c:49:5)
[Warning][Witness] couldn't locate invariant: (short)0 <= a (../plain/cohencu-ll_valuebound2.c:50:5)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound2.c:50:5)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound2.c:50:5)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound2.c:50:5)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/cohencu-ll_valuebound2.c:51:5)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound2.c:51:5)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound2.c:51:5)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound2.c:51:5)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound2.c:52:5)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound2.c:52:5)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound2.c:52:5)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/cohencu-ll_valuebound2.c:53:5)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound2.c:53:5)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound2.c:53:5)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound2.c:53:5)

runtime: 00:00:10.099
vars: 57, evals: 1502

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=793.86MB, max=12.37MB, minor=790.86MB, major=15.83MB, promoted=12.83MB
    minor collections=379  major collections=6 compactions=0


runtime: 00:00:20.139
vars: 57, evals: 1892

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=993.46MB, max=12.37MB, minor=990.45MB, major=17.89MB, promoted=14.88MB
    minor collections=475  major collections=7 compactions=0


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

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1127.36MB, max=12.37MB, minor=1124.34MB, major=19.10MB, promoted=16.08MB
    minor collections=539  major collections=7 compactions=0


runtime: 00:00:40.141
vars: 57, evals: 2341

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1228.36MB, max=12.37MB, minor=1225.34MB, major=20.09MB, promoted=17.07MB
    minor collections=587  major collections=7 compactions=0


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

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1312.92MB, max=12.37MB, minor=1309.89MB, major=20.88MB, promoted=17.85MB
    minor collections=628  major collections=8 compactions=0


runtime: 00:01:00.160
vars: 57, evals: 2651

|rho|=57
|called|=18
|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1386.29MB, max=12.37MB, minor=1383.26MB, major=21.59MB, promoted=18.56MB
    minor collections=663  major collections=8 compactions=0


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

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1449.92MB, max=12.37MB, minor=1446.88MB, major=22.22MB, promoted=19.19MB
    minor collections=693  major collections=8 compactions=0


runtime: 00:01:20.186
vars: 57, evals: 2873

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1505.06MB, max=12.37MB, minor=1502.02MB, major=22.72MB, promoted=19.68MB
    minor collections=719  major collections=8 compactions=0


runtime: 00:01:30.185
vars: 57, evals: 2975

|rho|=57
|called|=11
|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1558.09MB, max=14.22MB, minor=1555.05MB, major=23.23MB, promoted=20.19MB
    minor collections=745  major collections=8 compactions=0


runtime: 00:01:40.190
vars: 57, evals: 3076

|rho|=57
|called|=18
|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1606.73MB, max=14.22MB, minor=1603.69MB, major=23.70MB, promoted=20.66MB
    minor collections=768  major collections=8 compactions=0


runtime: 00:01:50.373
vars: 57, evals: 3161

|rho|=57
|called|=18
|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1650.92MB, max=14.22MB, minor=1647.88MB, major=24.14MB, promoted=21.09MB
    minor collections=789  major collections=8 compactions=0


runtime: 00:02:00.216
vars: 57, evals: 3230

|rho|=57
|called|=14
|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1689.58MB, max=14.22MB, minor=1686.54MB, major=24.46MB, promoted=21.42MB
    minor collections=808  major collections=9 compactions=0


runtime: 00:02:10.269
vars: 57, evals: 3298

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1725.81MB, max=14.22MB, minor=1722.77MB, major=24.75MB, promoted=21.70MB
    minor collections=825  major collections=9 compactions=0


runtime: 00:02:20.233
vars: 57, evals: 3383

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1764.12MB, max=14.22MB, minor=1761.07MB, major=25.07MB, promoted=22.02MB
    minor collections=843  major collections=9 compactions=0


runtime: 00:02:30.681
vars: 57, evals: 3444

|rho|=57
|called|=17
|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1792.24MB, max=14.22MB, minor=1789.19MB, major=25.35MB, promoted=22.30MB
    minor collections=857  major collections=9 compactions=0


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

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1821.21MB, max=14.22MB, minor=1818.16MB, major=25.60MB, promoted=22.55MB
    minor collections=871  major collections=9 compactions=0


runtime: 00:02:50.490
vars: 57, evals: 3549

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1847.57MB, max=14.22MB, minor=1844.51MB, major=25.90MB, promoted=22.84MB
    minor collections=883  major collections=9 compactions=0


runtime: 00:03:00.272
vars: 57, evals: 3600

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1871.49MB, max=14.22MB, minor=1868.44MB, major=26.11MB, promoted=23.05MB
    minor collections=894  major collections=9 compactions=0


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

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1886.79MB, max=14.22MB, minor=1883.73MB, major=26.24MB, promoted=23.18MB
    minor collections=902  major collections=9 compactions=0


runtime: 00:03:24.256
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1889.48MB, max=14.22MB, minor=1886.43MB, major=26.25MB, promoted=23.20MB
    minor collections=903  major collections=9 compactions=0


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

|rho|=57
|called|=17
|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1902.02MB, max=14.22MB, minor=1898.96MB, major=26.38MB, promoted=23.33MB
    minor collections=909  major collections=9 compactions=0


runtime: 00:03:40.548
vars: 57, evals: 3698

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1917.37MB, max=14.22MB, minor=1914.31MB, major=26.48MB, promoted=23.42MB
    minor collections=916  major collections=9 compactions=0


runtime: 00:03:50.411
vars: 57, evals: 3733

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1940.55MB, max=14.22MB, minor=1937.49MB, major=26.67MB, promoted=23.60MB
    minor collections=927  major collections=9 compactions=0


runtime: 00:04:00.345
vars: 57, evals: 3783

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1961.91MB, max=14.22MB, minor=1958.85MB, major=26.93MB, promoted=23.86MB
    minor collections=938  major collections=9 compactions=0


runtime: 00:04:11.092
vars: 57, evals: 3807

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1978.47MB, max=14.22MB, minor=1975.40MB, major=27.03MB, promoted=23.97MB
    minor collections=945  major collections=9 compactions=0


runtime: 00:04:23.530
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1983.74MB, max=14.22MB, minor=1980.68MB, major=27.10MB, promoted=24.03MB
    minor collections=948  major collections=9 compactions=0


runtime: 00:04:30.389
vars: 57, evals: 3836

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1988.73MB, max=14.22MB, minor=1985.66MB, major=27.11MB, promoted=24.05MB
    minor collections=950  major collections=9 compactions=0


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

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1994.83MB, max=14.22MB, minor=1991.77MB, major=27.15MB, promoted=24.09MB
    minor collections=953  major collections=9 compactions=0


runtime: 00:04:58.731
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1998.36MB, max=14.22MB, minor=1995.29MB, major=27.18MB, promoted=24.12MB
    minor collections=955  major collections=9 compactions=0


runtime: 00:05:01.853
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=1998.74MB, max=14.22MB, minor=1995.68MB, major=27.18MB, promoted=24.12MB
    minor collections=955  major collections=9 compactions=0


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

|rho|=57
|called|=9
|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2000.20MB, max=14.22MB, minor=1997.14MB, major=27.22MB, promoted=24.16MB
    minor collections=956  major collections=9 compactions=0


runtime: 00:05:37.527
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2000.37MB, max=14.22MB, minor=1997.30MB, major=27.22MB, promoted=24.16MB
    minor collections=956  major collections=9 compactions=0


runtime: 00:06:04.415
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2000.44MB, max=14.22MB, minor=1997.38MB, major=27.22MB, promoted=24.16MB
    minor collections=956  major collections=9 compactions=0


runtime: 00:06:12.743
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2000.56MB, max=14.22MB, minor=1997.50MB, major=27.22MB, promoted=24.16MB
    minor collections=956  major collections=9 compactions=0


runtime: 00:06:20.471
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2005.82MB, max=14.22MB, minor=2002.75MB, major=27.30MB, promoted=24.23MB
    minor collections=959  major collections=9 compactions=0


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

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2013.77MB, max=14.22MB, minor=2010.71MB, major=27.34MB, promoted=24.27MB
    minor collections=962  major collections=9 compactions=0


runtime: 00:06:41.166
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2020.46MB, max=14.22MB, minor=2017.40MB, major=27.41MB, promoted=24.35MB
    minor collections=966  major collections=9 compactions=0


runtime: 00:06:52.161
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2022.40MB, max=14.22MB, minor=2019.33MB, major=27.41MB, promoted=24.35MB
    minor collections=966  major collections=9 compactions=0


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

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2030.64MB, max=14.22MB, minor=2027.57MB, major=27.49MB, promoted=24.42MB
    minor collections=970  major collections=9 compactions=0


runtime: 00:07:10.898
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2044.30MB, max=14.22MB, minor=2041.23MB, major=27.62MB, promoted=24.55MB
    minor collections=977  major collections=9 compactions=0


runtime: 00:07:21.015
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2051.43MB, max=14.22MB, minor=2048.36MB, major=27.69MB, promoted=24.62MB
    minor collections=980  major collections=9 compactions=0


runtime: 00:07:30.536
vars: 57, evals: 3984

|rho|=57
|called|=9
|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2067.36MB, max=14.22MB, minor=2064.29MB, major=27.86MB, promoted=24.79MB
    minor collections=988  major collections=9 compactions=0


runtime: 00:07:41.471
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2079.27MB, max=14.22MB, minor=2076.20MB, major=27.96MB, promoted=24.89MB
    minor collections=994  major collections=9 compactions=0


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

|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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2087.60MB, max=14.22MB, minor=2084.53MB, major=28.02MB, promoted=24.96MB
    minor collections=998  major collections=9 compactions=0


runtime: 00:08:01.389
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2090.90MB, max=14.22MB, minor=2087.83MB, major=28.09MB, promoted=25.02MB
    minor collections=1000  major collections=10 compactions=0


runtime: 00:08:15.212
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2094.72MB, max=14.22MB, minor=2091.64MB, major=28.10MB, promoted=25.03MB
    minor collections=1001  major collections=10 compactions=0


runtime: 00:08:24.301
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2097.56MB, max=14.22MB, minor=2094.49MB, major=28.12MB, promoted=25.05MB
    minor collections=1003  major collections=10 compactions=0


runtime: 00:08:30.578
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2099.50MB, max=14.22MB, minor=2096.43MB, major=28.13MB, promoted=25.06MB
    minor collections=1004  major collections=10 compactions=0


runtime: 00:08:40.599
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2102.61MB, max=14.22MB, minor=2099.54MB, major=28.15MB, promoted=25.07MB
    minor collections=1005  major collections=10 compactions=0


runtime: 00:08:53.247
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2105.92MB, max=14.22MB, minor=2102.85MB, major=28.19MB, promoted=25.12MB
    minor collections=1007  major collections=10 compactions=0


runtime: 00:09:00.643
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 __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_valuebound2.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound2.c:11:1-13:1
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound2.c:14:1-20:1
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound2.c:22:1-56:1

Memory statistics: total=2108.12MB, max=14.22MB, minor=2105.04MB, major=28.21MB, promoted=25.13MB
    minor collections=1008  major collections=10 compactions=0

