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

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

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

Memory statistics: total=801.63MB, max=12.37MB, minor=798.63MB, major=15.89MB, promoted=12.89MB
    minor collections=383  major collections=6 compactions=0


runtime: 00:00:20.141
vars: 57, evals: 1907

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

Memory statistics: total=1000.85MB, max=12.37MB, minor=997.84MB, major=17.82MB, promoted=14.81MB
    minor collections=478  major collections=7 compactions=0


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

Memory statistics: total=1130.57MB, max=12.37MB, minor=1127.56MB, major=19.07MB, promoted=16.05MB
    minor collections=540  major collections=7 compactions=0


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

Memory statistics: total=1231.83MB, max=12.37MB, minor=1228.80MB, major=19.94MB, promoted=16.92MB
    minor collections=588  major collections=7 compactions=0


runtime: 00:00:50.134
vars: 57, evals: 2522

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

Memory statistics: total=1318.96MB, max=12.37MB, minor=1315.93MB, major=20.83MB, promoted=17.80MB
    minor collections=631  major collections=8 compactions=0


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

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

Memory statistics: total=1392.97MB, max=12.37MB, minor=1389.94MB, major=21.54MB, promoted=18.51MB
    minor collections=666  major collections=8 compactions=0


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

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

Memory statistics: total=1454.82MB, max=12.37MB, minor=1451.79MB, major=22.19MB, promoted=19.16MB
    minor collections=695  major collections=8 compactions=0


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

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

Memory statistics: total=1513.28MB, max=12.37MB, minor=1510.24MB, major=22.78MB, promoted=19.74MB
    minor collections=723  major collections=8 compactions=0


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

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

Memory statistics: total=1564.65MB, max=14.22MB, minor=1561.61MB, major=23.29MB, promoted=20.25MB
    minor collections=748  major collections=8 compactions=0


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

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

Memory statistics: total=1611.13MB, max=14.22MB, minor=1608.09MB, major=23.72MB, promoted=20.67MB
    minor collections=770  major collections=8 compactions=0


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

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

Memory statistics: total=1654.79MB, max=14.22MB, minor=1651.75MB, major=24.11MB, promoted=21.06MB
    minor collections=791  major collections=8 compactions=0


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

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

Memory statistics: total=1696.95MB, max=14.22MB, minor=1693.90MB, major=24.52MB, promoted=21.47MB
    minor collections=811  major collections=9 compactions=0


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

Memory statistics: total=1733.68MB, max=14.22MB, minor=1730.63MB, major=24.89MB, promoted=21.84MB
    minor collections=829  major collections=9 compactions=0


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

Memory statistics: total=1768.71MB, max=14.22MB, minor=1765.66MB, major=25.17MB, promoted=22.12MB
    minor collections=845  major collections=9 compactions=0


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

Memory statistics: total=1798.55MB, max=14.22MB, minor=1795.50MB, major=25.42MB, promoted=22.37MB
    minor collections=860  major collections=9 compactions=0


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

Memory statistics: total=1825.13MB, max=14.22MB, minor=1822.08MB, major=25.59MB, promoted=22.53MB
    minor collections=872  major collections=9 compactions=0


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

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

Memory statistics: total=1853.88MB, max=14.22MB, minor=1850.82MB, major=25.90MB, promoted=22.84MB
    minor collections=886  major collections=9 compactions=0


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

Memory statistics: total=1875.63MB, max=14.22MB, minor=1872.57MB, major=26.04MB, promoted=22.98MB
    minor collections=896  major collections=9 compactions=0


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

Memory statistics: total=1889.46MB, max=14.22MB, minor=1886.40MB, major=26.15MB, promoted=23.09MB
    minor collections=903  major collections=9 compactions=0


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

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

Memory statistics: total=1891.43MB, max=14.22MB, minor=1888.37MB, major=26.17MB, promoted=23.11MB
    minor collections=904  major collections=9 compactions=0


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

Memory statistics: total=1906.35MB, max=14.22MB, minor=1903.29MB, major=26.30MB, promoted=23.24MB
    minor collections=911  major collections=9 compactions=0


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

Memory statistics: total=1922.12MB, max=14.22MB, minor=1919.06MB, major=26.44MB, promoted=23.38MB
    minor collections=919  major collections=9 compactions=0


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

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

Memory statistics: total=1944.21MB, max=14.22MB, minor=1941.15MB, major=26.61MB, promoted=23.55MB
    minor collections=929  major collections=9 compactions=0


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

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

Memory statistics: total=1964.61MB, max=14.22MB, minor=1961.55MB, major=26.83MB, promoted=23.77MB
    minor collections=939  major collections=9 compactions=0


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

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

Memory statistics: total=1980.53MB, max=14.22MB, minor=1977.46MB, major=26.94MB, promoted=23.88MB
    minor collections=946  major collections=9 compactions=0


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

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

Memory statistics: total=1985.81MB, max=14.22MB, minor=1982.75MB, major=27.00MB, promoted=23.93MB
    minor collections=949  major collections=9 compactions=0


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

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

Memory statistics: total=1990.90MB, max=14.22MB, minor=1987.84MB, major=27.02MB, promoted=23.95MB
    minor collections=951  major collections=9 compactions=0


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

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

Memory statistics: total=1996.91MB, max=14.22MB, minor=1993.85MB, major=27.05MB, promoted=23.99MB
    minor collections=954  major collections=9 compactions=0


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

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

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


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

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

Memory statistics: total=2000.83MB, max=14.22MB, minor=1997.76MB, major=27.09MB, promoted=24.03MB
    minor collections=956  major collections=9 compactions=0


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

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

Memory statistics: total=2002.29MB, max=14.22MB, minor=1999.22MB, major=27.13MB, promoted=24.07MB
    minor collections=957  major collections=9 compactions=0


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

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

Memory statistics: total=2002.46MB, max=14.22MB, minor=1999.39MB, major=27.13MB, promoted=24.07MB
    minor collections=957  major collections=9 compactions=0


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

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

Memory statistics: total=2002.53MB, max=14.22MB, minor=1999.46MB, major=27.13MB, promoted=24.07MB
    minor collections=957  major collections=9 compactions=0


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

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

Memory statistics: total=2002.65MB, max=14.22MB, minor=1999.58MB, major=27.13MB, promoted=24.07MB
    minor collections=957  major collections=9 compactions=0


runtime: 00:06:20.503
vars: 57, evals: 3869

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

Memory statistics: total=2006.41MB, max=14.22MB, minor=2003.34MB, major=27.19MB, promoted=24.13MB
    minor collections=959  major collections=9 compactions=0


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

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

Memory statistics: total=2015.68MB, max=14.22MB, minor=2012.61MB, major=27.25MB, promoted=24.18MB
    minor collections=963  major collections=9 compactions=0


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

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

Memory statistics: total=2022.57MB, max=14.22MB, minor=2019.51MB, major=27.32MB, promoted=24.25MB
    minor collections=967  major collections=9 compactions=0


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

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

Memory statistics: total=2024.51MB, max=14.22MB, minor=2021.44MB, major=27.32MB, promoted=24.25MB
    minor collections=967  major collections=9 compactions=0


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

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

Memory statistics: total=2032.76MB, max=14.22MB, minor=2029.69MB, major=27.40MB, promoted=24.33MB
    minor collections=971  major collections=9 compactions=0


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

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

Memory statistics: total=2046.44MB, max=14.22MB, minor=2043.37MB, major=27.52MB, promoted=24.45MB
    minor collections=978  major collections=9 compactions=0


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

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

Memory statistics: total=2053.57MB, max=14.22MB, minor=2050.50MB, major=27.59MB, promoted=24.52MB
    minor collections=981  major collections=9 compactions=0


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

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

Memory statistics: total=2071.09MB, max=14.22MB, minor=2068.02MB, major=27.77MB, promoted=24.70MB
    minor collections=990  major collections=9 compactions=0


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

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

Memory statistics: total=2081.45MB, max=14.22MB, minor=2078.38MB, major=27.83MB, promoted=24.76MB
    minor collections=995  major collections=9 compactions=0


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

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

Memory statistics: total=2090.08MB, max=14.22MB, minor=2087.01MB, major=27.90MB, promoted=24.83MB
    minor collections=999  major collections=9 compactions=0


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

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

Memory statistics: total=2093.09MB, max=14.22MB, minor=2090.02MB, major=27.92MB, promoted=24.85MB
    minor collections=1000  major collections=9 compactions=0


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

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

Memory statistics: total=2096.90MB, max=14.22MB, minor=2093.83MB, major=27.96MB, promoted=24.89MB
    minor collections=1002  major collections=9 compactions=0


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

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

Memory statistics: total=2099.76MB, max=14.22MB, minor=2096.68MB, major=27.98MB, promoted=24.91MB
    minor collections=1003  major collections=9 compactions=0


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

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

Memory statistics: total=2101.90MB, max=14.22MB, minor=2098.82MB, major=28.00MB, promoted=24.93MB
    minor collections=1005  major collections=10 compactions=0


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

Memory statistics: total=2105.42MB, max=14.22MB, minor=2102.34MB, major=28.04MB, promoted=24.96MB
    minor collections=1007  major collections=10 compactions=0


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

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

Memory statistics: total=2108.13MB, max=14.22MB, minor=2105.05MB, major=28.06MB, promoted=24.99MB
    minor collections=1008  major collections=10 compactions=0


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

Memory statistics: total=2110.99MB, max=14.22MB, minor=2107.92MB, major=28.07MB, promoted=25.00MB
    minor collections=1009  major collections=10 compactions=0

