/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_valuebound1.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_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.128
vars: 57, evals: 1513

|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=800.23MB, max=12.37MB, minor=797.23MB, major=16.03MB, promoted=13.03MB
    minor collections=382  major collections=6 compactions=0


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

|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=998.00MB, max=12.37MB, minor=994.99MB, major=18.11MB, promoted=15.10MB
    minor collections=477  major collections=7 compactions=0


runtime: 00:00:30.127
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=1129.44MB, max=12.37MB, minor=1126.43MB, major=19.30MB, promoted=16.29MB
    minor collections=540  major collections=7 compactions=0


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

|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=1230.54MB, max=12.37MB, minor=1227.52MB, major=20.33MB, promoted=17.31MB
    minor collections=588  major collections=7 compactions=0


runtime: 00:00:50.155
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=1316.15MB, max=12.37MB, minor=1313.12MB, major=21.17MB, promoted=18.14MB
    minor collections=629  major collections=8 compactions=0


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

|rho|=57
|called|=18
|stable|=53
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of __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=1388.16MB, max=12.37MB, minor=1385.13MB, major=21.91MB, promoted=18.88MB
    minor collections=664  major collections=8 compactions=0


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

|rho|=57
|called|=17
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of __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=1450.60MB, max=12.37MB, minor=1447.57MB, major=22.50MB, promoted=19.47MB
    minor collections=693  major collections=8 compactions=0


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

|rho|=57
|called|=8
|stable|=56
|infl|=51
|wpoint|=1
|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=1506.79MB, max=14.22MB, minor=1503.75MB, major=23.02MB, promoted=19.99MB
    minor collections=720  major collections=8 compactions=0


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

|rho|=57
|called|=13
|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=1557.58MB, max=14.22MB, minor=1554.55MB, major=23.51MB, promoted=20.48MB
    minor collections=744  major collections=8 compactions=0


runtime: 00:01:40.365
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 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=1606.69MB, max=14.22MB, minor=1603.65MB, major=23.97MB, promoted=20.93MB
    minor collections=768  major collections=8 compactions=0


runtime: 00:01:50.224
vars: 57, evals: 3145

|rho|=57
|called|=13
|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=1646.21MB, max=14.22MB, minor=1643.17MB, major=24.33MB, promoted=21.29MB
    minor collections=787  major collections=8 compactions=0


runtime: 00:02:00.241
vars: 57, evals: 3213

|rho|=57
|called|=7
|stable|=56
|infl|=51
|wpoint|=1
|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=1684.17MB, max=14.22MB, minor=1681.12MB, major=24.70MB, promoted=21.66MB
    minor collections=805  major collections=9 compactions=0


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

|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=1723.14MB, max=14.22MB, minor=1720.09MB, major=25.06MB, promoted=22.01MB
    minor collections=824  major collections=9 compactions=0


runtime: 00:02:20.236
vars: 57, evals: 3376

|rho|=57
|called|=18
|stable|=51
|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=1761.14MB, max=14.22MB, minor=1758.09MB, major=25.36MB, promoted=22.31MB
    minor collections=842  major collections=9 compactions=0


runtime: 00:02:30.247
vars: 57, evals: 3429

|rho|=57
|called|=16
|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=1786.57MB, max=14.22MB, minor=1783.52MB, major=25.61MB, promoted=22.56MB
    minor collections=854  major collections=9 compactions=0


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

|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=1817.88MB, max=14.22MB, minor=1814.83MB, major=25.88MB, promoted=22.82MB
    minor collections=869  major collections=9 compactions=0


runtime: 00:02:50.462
vars: 57, evals: 3538

|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=1841.55MB, max=14.22MB, minor=1838.49MB, major=26.16MB, promoted=23.10MB
    minor collections=880  major collections=9 compactions=0


runtime: 00:03:00.395
vars: 57, evals: 3584

|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=1867.93MB, max=14.22MB, minor=1864.88MB, major=26.41MB, promoted=23.35MB
    minor collections=893  major collections=9 compactions=0


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

|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=1884.20MB, max=14.22MB, minor=1881.15MB, major=26.55MB, promoted=23.50MB
    minor collections=901  major collections=9 compactions=0


runtime: 00:03:22.334
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=1889.60MB, max=14.22MB, minor=1886.55MB, major=26.60MB, promoted=23.54MB
    minor collections=903  major collections=9 compactions=0


runtime: 00:03:30.342
vars: 57, evals: 3652

|rho|=57
|called|=16
|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=1896.26MB, max=14.22MB, minor=1893.20MB, major=26.69MB, promoted=23.63MB
    minor collections=906  major collections=9 compactions=0


runtime: 00:03:40.396
vars: 57, evals: 3676

|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=1911.53MB, max=14.22MB, minor=1908.47MB, major=26.80MB, promoted=23.74MB
    minor collections=914  major collections=9 compactions=0


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

|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=1935.15MB, max=14.22MB, minor=1932.09MB, major=27.00MB, promoted=23.94MB
    minor collections=925  major collections=9 compactions=0


runtime: 00:04:00.370
vars: 57, evals: 3761

|rho|=57
|called|=10
|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=1955.78MB, max=14.22MB, minor=1952.72MB, major=27.20MB, promoted=24.14MB
    minor collections=935  major collections=9 compactions=0


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

|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=1975.31MB, max=14.22MB, minor=1972.24MB, major=27.35MB, promoted=24.29MB
    minor collections=944  major collections=9 compactions=0


runtime: 00:04:22.464
vars: 57, evals: 3823

|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=1982.06MB, max=14.22MB, minor=1978.99MB, major=27.43MB, promoted=24.37MB
    minor collections=947  major collections=9 compactions=0


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

|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=1987.11MB, max=14.22MB, minor=1984.05MB, major=27.50MB, promoted=24.43MB
    minor collections=950  major collections=9 compactions=0


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

|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=1992.99MB, max=14.22MB, minor=1989.93MB, major=27.54MB, promoted=24.48MB
    minor collections=952  major collections=9 compactions=0


runtime: 00:05:03.564
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=1998.88MB, max=14.22MB, minor=1995.82MB, major=27.60MB, promoted=24.53MB
    minor collections=955  major collections=9 compactions=0


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

|rho|=57
|called|=10
|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.70MB, max=14.22MB, minor=1996.64MB, major=27.62MB, promoted=24.55MB
    minor collections=956  major collections=9 compactions=0


runtime: 00:05:42.676
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=2000.86MB, max=14.22MB, minor=1997.79MB, major=27.62MB, promoted=24.55MB
    minor collections=956  major collections=9 compactions=0


runtime: 00:06:09.391
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=2000.93MB, max=14.22MB, minor=1997.87MB, major=27.62MB, promoted=24.55MB
    minor collections=956  major collections=9 compactions=0


runtime: 00:06:12.116
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=2001.00MB, max=14.22MB, minor=1997.94MB, major=27.62MB, promoted=24.55MB
    minor collections=956  major collections=9 compactions=0


runtime: 00:06:20.783
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=2001.11MB, max=14.22MB, minor=1998.04MB, major=27.62MB, promoted=24.55MB
    minor collections=956  major collections=9 compactions=0


runtime: 00:06:30.609
vars: 57, evals: 3882

|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=2009.21MB, max=14.22MB, minor=2006.14MB, major=27.71MB, promoted=24.65MB
    minor collections=960  major collections=9 compactions=0


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

|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=2018.06MB, max=14.22MB, minor=2014.99MB, major=27.77MB, promoted=24.71MB
    minor collections=964  major collections=9 compactions=0


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

|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 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.57MB, max=14.22MB, minor=2018.50MB, major=27.80MB, promoted=24.73MB
    minor collections=966  major collections=9 compactions=0


runtime: 00:07:01.191
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=2022.97MB, max=14.22MB, minor=2019.90MB, major=27.85MB, promoted=24.78MB
    minor collections=967  major collections=9 compactions=0


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

|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=2039.40MB, max=14.22MB, minor=2036.33MB, major=27.99MB, promoted=24.92MB
    minor collections=975  major collections=9 compactions=0


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

|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=2049.22MB, max=14.22MB, minor=2046.16MB, major=28.10MB, promoted=25.03MB
    minor collections=980  major collections=10 compactions=0


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

|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=2057.46MB, max=14.22MB, minor=2054.39MB, major=28.18MB, promoted=25.11MB
    minor collections=984  major collections=10 compactions=0


runtime: 00:07:41.081
vars: 57, evals: 4006

|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=2073.24MB, max=14.22MB, minor=2070.17MB, major=28.33MB, promoted=25.27MB
    minor collections=991  major collections=10 compactions=0


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

|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=2084.32MB, max=14.22MB, minor=2081.25MB, major=28.42MB, promoted=25.35MB
    minor collections=996  major collections=10 compactions=0


runtime: 00:08:01.268
vars: 57, evals: 4030

|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=2089.92MB, max=14.22MB, minor=2086.85MB, major=28.47MB, promoted=25.40MB
    minor collections=999  major collections=10 compactions=0


runtime: 00:08:13.221
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=2092.99MB, max=14.22MB, minor=2089.92MB, major=28.53MB, promoted=25.46MB
    minor collections=1001  major collections=10 compactions=0


runtime: 00:08:21.353
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=2095.25MB, max=14.22MB, minor=2092.18MB, major=28.54MB, promoted=25.47MB
    minor collections=1002  major collections=10 compactions=0


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

|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=2098.58MB, max=14.22MB, minor=2095.51MB, major=28.56MB, promoted=25.49MB
    minor collections=1003  major collections=10 compactions=0


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

|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=2101.86MB, max=14.22MB, minor=2098.79MB, major=28.58MB, promoted=25.51MB
    minor collections=1005  major collections=10 compactions=0


runtime: 00:08:50.750
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=2103.99MB, max=14.22MB, minor=2100.92MB, major=28.59MB, promoted=25.52MB
    minor collections=1006  major collections=10 compactions=0


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

|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=2107.12MB, max=14.22MB, minor=2104.05MB, major=28.63MB, promoted=25.56MB
    minor collections=1008  major collections=10 compactions=0

