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

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

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

Memory statistics: total=798.14MB, max=12.37MB, minor=795.14MB, major=15.79MB, promoted=12.79MB
    minor collections=381  major collections=6 compactions=0


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

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

Memory statistics: total=995.57MB, max=12.37MB, minor=992.56MB, major=17.64MB, promoted=14.63MB
    minor collections=476  major collections=7 compactions=0


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

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

Memory statistics: total=1128.40MB, max=12.37MB, minor=1125.39MB, major=18.92MB, promoted=15.90MB
    minor collections=539  major collections=7 compactions=0


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

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

Memory statistics: total=1230.26MB, max=12.37MB, minor=1227.24MB, major=19.83MB, promoted=16.80MB
    minor collections=588  major collections=7 compactions=0


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

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

Memory statistics: total=1315.34MB, max=12.37MB, minor=1312.31MB, major=20.66MB, promoted=17.63MB
    minor collections=628  major collections=7 compactions=0


runtime: 00:01:00.235
vars: 57, evals: 2664

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

Memory statistics: total=1389.93MB, max=12.37MB, minor=1386.90MB, major=21.35MB, promoted=18.32MB
    minor collections=664  major collections=8 compactions=0


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

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

Memory statistics: total=1451.01MB, max=12.37MB, minor=1447.98MB, major=21.90MB, promoted=18.86MB
    minor collections=693  major collections=8 compactions=0


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

Memory statistics: total=1509.51MB, max=12.37MB, minor=1506.47MB, major=22.44MB, promoted=19.41MB
    minor collections=721  major collections=8 compactions=0


runtime: 00:01:30.173
vars: 57, evals: 2997

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

Memory statistics: total=1563.40MB, max=14.22MB, minor=1560.37MB, major=23.00MB, promoted=19.97MB
    minor collections=747  major collections=8 compactions=0


runtime: 00:01:40.198
vars: 57, evals: 3089

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

Memory statistics: total=1610.48MB, max=14.22MB, minor=1607.44MB, major=23.43MB, promoted=20.39MB
    minor collections=770  major collections=8 compactions=0


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

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

Memory statistics: total=1652.62MB, max=14.22MB, minor=1649.58MB, major=23.92MB, promoted=20.88MB
    minor collections=790  major collections=8 compactions=0


runtime: 00:02:00.336
vars: 57, evals: 3246

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

Memory statistics: total=1694.70MB, max=14.22MB, minor=1691.65MB, major=24.32MB, promoted=21.27MB
    minor collections=810  major collections=8 compactions=0


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

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

Memory statistics: total=1731.06MB, max=14.22MB, minor=1728.01MB, major=24.67MB, promoted=21.62MB
    minor collections=828  major collections=9 compactions=0


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

Memory statistics: total=1765.69MB, max=14.22MB, minor=1762.64MB, major=24.95MB, promoted=21.91MB
    minor collections=844  major collections=9 compactions=0


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

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

Memory statistics: total=1795.48MB, max=14.22MB, minor=1792.43MB, major=25.19MB, promoted=22.14MB
    minor collections=858  major collections=9 compactions=0


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

Memory statistics: total=1822.02MB, max=14.22MB, minor=1818.97MB, major=25.46MB, promoted=22.40MB
    minor collections=871  major collections=9 compactions=0


runtime: 00:02:50.291
vars: 57, evals: 3560

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

Memory statistics: total=1850.08MB, max=14.22MB, minor=1847.03MB, major=25.75MB, promoted=22.70MB
    minor collections=884  major collections=9 compactions=0


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

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

Memory statistics: total=1872.44MB, max=14.22MB, minor=1869.38MB, major=25.98MB, promoted=22.92MB
    minor collections=895  major collections=9 compactions=0


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

Memory statistics: total=1886.23MB, max=14.22MB, minor=1883.18MB, major=26.08MB, promoted=23.02MB
    minor collections=902  major collections=9 compactions=0


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

Memory statistics: total=1888.20MB, max=14.22MB, minor=1885.15MB, major=26.08MB, promoted=23.02MB
    minor collections=902  major collections=9 compactions=0


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

Memory statistics: total=1902.82MB, max=14.22MB, minor=1899.76MB, major=26.19MB, promoted=23.14MB
    minor collections=909  major collections=9 compactions=0


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

Memory statistics: total=1918.90MB, max=14.22MB, minor=1915.84MB, major=26.37MB, promoted=23.31MB
    minor collections=917  major collections=9 compactions=0


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

Memory statistics: total=1941.57MB, max=14.22MB, minor=1938.51MB, major=26.59MB, promoted=23.53MB
    minor collections=928  major collections=9 compactions=0


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

Memory statistics: total=1963.42MB, max=14.22MB, minor=1960.36MB, major=26.79MB, promoted=23.73MB
    minor collections=938  major collections=9 compactions=0


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

Memory statistics: total=1978.64MB, max=14.22MB, minor=1975.58MB, major=26.97MB, promoted=23.91MB
    minor collections=946  major collections=9 compactions=0


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

Memory statistics: total=1982.45MB, max=14.22MB, minor=1979.38MB, major=26.98MB, promoted=23.92MB
    minor collections=947  major collections=9 compactions=0


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

Memory statistics: total=1988.99MB, max=14.22MB, minor=1985.93MB, major=27.04MB, promoted=23.97MB
    minor collections=951  major collections=9 compactions=0


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

Memory statistics: total=1994.28MB, max=14.22MB, minor=1991.22MB, major=27.07MB, promoted=24.01MB
    minor collections=953  major collections=9 compactions=0


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

Memory statistics: total=1997.04MB, max=14.22MB, minor=1993.98MB, major=27.10MB, promoted=24.03MB
    minor collections=954  major collections=9 compactions=0


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

Memory statistics: total=1997.43MB, max=14.22MB, minor=1994.36MB, major=27.12MB, promoted=24.05MB
    minor collections=955  major collections=9 compactions=0


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

Memory statistics: total=1999.02MB, max=14.22MB, minor=1995.95MB, major=27.12MB, promoted=24.05MB
    minor collections=955  major collections=9 compactions=0


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

Memory statistics: total=1999.09MB, max=14.22MB, minor=1996.02MB, major=27.12MB, promoted=24.05MB
    minor collections=955  major collections=9 compactions=0


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

Memory statistics: total=1999.21MB, max=14.22MB, minor=1996.15MB, major=27.12MB, promoted=24.05MB
    minor collections=955  major collections=9 compactions=0


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

Memory statistics: total=2004.52MB, max=14.22MB, minor=2001.46MB, major=27.18MB, promoted=24.11MB
    minor collections=958  major collections=9 compactions=0


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

Memory statistics: total=2013.16MB, max=14.22MB, minor=2010.10MB, major=27.25MB, promoted=24.18MB
    minor collections=962  major collections=9 compactions=0


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

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

Memory statistics: total=2019.42MB, max=14.22MB, minor=2016.36MB, major=27.29MB, promoted=24.23MB
    minor collections=965  major collections=9 compactions=0


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

Memory statistics: total=2021.01MB, max=14.22MB, minor=2017.95MB, major=27.35MB, promoted=24.28MB
    minor collections=966  major collections=9 compactions=0


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

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

Memory statistics: total=2031.40MB, max=14.22MB, minor=2028.33MB, major=27.45MB, promoted=24.38MB
    minor collections=971  major collections=9 compactions=0


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

Memory statistics: total=2042.94MB, max=14.22MB, minor=2039.87MB, major=27.55MB, promoted=24.49MB
    minor collections=976  major collections=9 compactions=0


runtime: 00:07:20.816
vars: 57, evals: 3967

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

Memory statistics: total=2052.35MB, max=14.22MB, minor=2049.28MB, major=27.66MB, promoted=24.59MB
    minor collections=981  major collections=9 compactions=0


runtime: 00:07:30.551
vars: 57, evals: 4000

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

Memory statistics: total=2069.06MB, max=14.22MB, minor=2065.99MB, major=27.82MB, promoted=24.75MB
    minor collections=989  major collections=9 compactions=0


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

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

Memory statistics: total=2078.51MB, max=14.22MB, minor=2075.44MB, major=27.86MB, promoted=24.79MB
    minor collections=993  major collections=9 compactions=0


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

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

Memory statistics: total=2087.66MB, max=14.22MB, minor=2084.59MB, major=27.92MB, promoted=24.85MB
    minor collections=998  major collections=9 compactions=0


runtime: 00:08:00.640
vars: 57, evals: 4046

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

Memory statistics: total=2091.01MB, max=14.22MB, minor=2087.94MB, major=27.95MB, promoted=24.88MB
    minor collections=999  major collections=9 compactions=0


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

Memory statistics: total=2093.28MB, max=14.22MB, minor=2090.21MB, major=27.96MB, promoted=24.89MB
    minor collections=1000  major collections=9 compactions=0


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

Memory statistics: total=2096.12MB, max=14.22MB, minor=2093.05MB, major=28.00MB, promoted=24.93MB
    minor collections=1002  major collections=9 compactions=0


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

Memory statistics: total=2098.32MB, max=14.22MB, minor=2095.25MB, major=28.03MB, promoted=24.96MB
    minor collections=1003  major collections=9 compactions=0


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

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

Memory statistics: total=2101.81MB, max=14.22MB, minor=2098.74MB, major=28.06MB, promoted=24.99MB
    minor collections=1005  major collections=10 compactions=0


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

Memory statistics: total=2104.48MB, max=14.22MB, minor=2101.41MB, major=28.07MB, promoted=25.00MB
    minor collections=1006  major collections=10 compactions=0


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

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

Memory statistics: total=2107.28MB, max=14.22MB, minor=2104.21MB, major=28.12MB, promoted=25.05MB
    minor collections=1008  major collections=10 compactions=0

