/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_valuebound50.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_valuebound50.yml/witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/cohencu-ll_valuebound50.c


--------------------------------------------------------------------------------


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Warning][Witness] couldn't locate invariant: 0LL <= n (../plain/cohencu-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: n <= 32768LL (../plain/cohencu-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound50.c:34:9)
[Warning][Witness] couldn't locate invariant: 0LL <= n (../plain/cohencu-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: n <= 32768LL (../plain/cohencu-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound50.c:35:9)
[Warning][Witness] couldn't locate invariant: 0LL <= n (../plain/cohencu-ll_valuebound50.c:36:9)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/cohencu-ll_valuebound50.c:36:9)
[Warning][Witness] couldn't locate invariant: n <= 32768LL (../plain/cohencu-ll_valuebound50.c:36:9)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound50.c:36:9)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/cohencu-ll_valuebound50.c:37:2)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound50.c:37:2)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:37:2)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:37:2)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound50.c:37:2)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound50.c:38:2)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:38:2)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:38:2)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound50.c:38:2)
[Warning][Witness] couldn't locate invariant: (short)0 <= a (../plain/cohencu-ll_valuebound50.c:39:13)
[Warning][Witness] couldn't locate invariant: 0LL <= n (../plain/cohencu-ll_valuebound50.c:39:13)
[Warning][Witness] couldn't locate invariant: n <= 32768LL (../plain/cohencu-ll_valuebound50.c:39:13)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound50.c:39:13)
[Warning][Witness] couldn't locate invariant: 0LL <= n (../plain/cohencu-ll_valuebound50.c:42:9)
[Warning][Witness] couldn't locate invariant: n <= 32767LL (../plain/cohencu-ll_valuebound50.c:42:9)
[Warning][Witness] couldn't locate invariant: (long long )a - n >= 0LL (../plain/cohencu-ll_valuebound50.c:42:9)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/cohencu-ll_valuebound50.c:43:9)
[Warning][Witness] couldn't locate invariant: 1LL <= n (../plain/cohencu-ll_valuebound50.c:43:9)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound50.c:43:9)
[Warning][Witness] couldn't locate invariant: n <= 32768LL (../plain/cohencu-ll_valuebound50.c:43:9)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound50.c:43:9)
[Warning][Witness] couldn't locate invariant: 1LL <= x (../plain/cohencu-ll_valuebound50.c:44:9)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound50.c:44:9)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:44:9)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:44:9)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound50.c:44:9)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:45:9)
[Warning][Witness] couldn't locate invariant: 7LL <= y (../plain/cohencu-ll_valuebound50.c:45:9)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:45:9)
[Warning][Witness] couldn't locate invariant: (1LL + (long long )a) - n >= 0LL (../plain/cohencu-ll_valuebound50.c:45:9)
[Warning][Witness] couldn't locate invariant: 1LL <= n (../plain/cohencu-ll_valuebound50.c:48:5)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:48:5)
[Warning][Witness] couldn't locate invariant: n <= 32768LL (../plain/cohencu-ll_valuebound50.c:48:5)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:48:5)
[Warning][Witness] couldn't locate invariant: n != 0LL (../plain/cohencu-ll_valuebound50.c:48:5)
[Warning][Witness] couldn't locate invariant: (short)0 <= a (../plain/cohencu-ll_valuebound50.c:49:5)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/cohencu-ll_valuebound50.c:49:5)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:49:5)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:49:5)
[Warning][Witness] couldn't locate invariant: (short)0 <= a (../plain/cohencu-ll_valuebound50.c:50:5)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound50.c:50:5)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:50:5)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:50:5)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/cohencu-ll_valuebound50.c:51:5)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound50.c:51:5)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:51:5)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:51:5)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound50.c:52:5)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:52:5)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:52:5)
[Warning][Witness] couldn't locate invariant: 0LL <= x (../plain/cohencu-ll_valuebound50.c:53:5)
[Warning][Witness] couldn't locate invariant: 1LL <= y (../plain/cohencu-ll_valuebound50.c:53:5)
[Warning][Witness] couldn't locate invariant: 6LL <= z (../plain/cohencu-ll_valuebound50.c:53:5)
[Warning][Witness] couldn't locate invariant: z <= 393222LL (../plain/cohencu-ll_valuebound50.c:53:5)

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

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

Memory statistics: total=802.35MB, max=12.37MB, minor=799.35MB, major=16.35MB, promoted=13.35MB
    minor collections=383  major collections=6 compactions=0


runtime: 00:00:20.098
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 main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=998.18MB, max=12.37MB, minor=995.17MB, major=18.17MB, promoted=15.16MB
    minor collections=477  major collections=7 compactions=0


runtime: 00:00:30.104
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 main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1129.39MB, max=12.37MB, minor=1126.37MB, major=19.34MB, promoted=16.33MB
    minor collections=540  major collections=7 compactions=0


runtime: 00:00:40.181
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 main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1230.76MB, max=12.37MB, minor=1227.74MB, major=20.33MB, promoted=17.31MB
    minor collections=588  major collections=7 compactions=0


runtime: 00:00:50.244
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 main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1316.47MB, max=12.37MB, minor=1313.45MB, major=21.13MB, promoted=18.10MB
    minor collections=629  major collections=8 compactions=0


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

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

Memory statistics: total=1389.00MB, max=12.37MB, minor=1385.97MB, major=21.86MB, promoted=18.83MB
    minor collections=664  major collections=8 compactions=0


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

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

Memory statistics: total=1451.97MB, max=12.37MB, minor=1448.94MB, major=22.41MB, promoted=19.38MB
    minor collections=694  major collections=8 compactions=0


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

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

Memory statistics: total=1510.78MB, max=12.37MB, minor=1507.74MB, major=22.94MB, promoted=19.90MB
    minor collections=722  major collections=8 compactions=0


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

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

Memory statistics: total=1563.28MB, max=14.22MB, minor=1560.24MB, major=23.42MB, promoted=20.38MB
    minor collections=747  major collections=8 compactions=0


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

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

Memory statistics: total=1609.73MB, max=14.22MB, minor=1606.69MB, major=23.84MB, promoted=20.80MB
    minor collections=769  major collections=8 compactions=0


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

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

Memory statistics: total=1654.01MB, max=14.22MB, minor=1650.97MB, major=24.23MB, promoted=21.18MB
    minor collections=790  major collections=8 compactions=0


runtime: 00:02:00.253
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 main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1695.48MB, max=14.22MB, minor=1692.43MB, major=24.69MB, promoted=21.65MB
    minor collections=811  major collections=9 compactions=0


runtime: 00:02:10.532
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 main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1732.17MB, max=14.22MB, minor=1729.13MB, major=24.98MB, promoted=21.94MB
    minor collections=828  major collections=9 compactions=0


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

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

Memory statistics: total=1767.16MB, max=14.22MB, minor=1764.11MB, major=25.26MB, promoted=22.21MB
    minor collections=845  major collections=9 compactions=0


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

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

Memory statistics: total=1796.33MB, max=14.22MB, minor=1793.28MB, major=25.49MB, promoted=22.44MB
    minor collections=859  major collections=9 compactions=0


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

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

Memory statistics: total=1823.50MB, max=14.22MB, minor=1820.45MB, major=25.72MB, promoted=22.67MB
    minor collections=872  major collections=9 compactions=0


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

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

Memory statistics: total=1850.09MB, max=14.22MB, minor=1847.03MB, major=25.97MB, promoted=22.91MB
    minor collections=884  major collections=9 compactions=0


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

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

Memory statistics: total=1873.37MB, max=14.22MB, minor=1870.31MB, major=26.19MB, promoted=23.13MB
    minor collections=895  major collections=9 compactions=0


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

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

Memory statistics: total=1887.28MB, max=14.22MB, minor=1884.22MB, major=26.30MB, promoted=23.25MB
    minor collections=902  major collections=9 compactions=0


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

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

Memory statistics: total=1889.80MB, max=14.22MB, minor=1886.75MB, major=26.33MB, promoted=23.27MB
    minor collections=903  major collections=9 compactions=0


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

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

Memory statistics: total=1903.77MB, max=14.22MB, minor=1900.71MB, major=26.45MB, promoted=23.39MB
    minor collections=910  major collections=9 compactions=0


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

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

Memory statistics: total=1919.84MB, max=14.22MB, minor=1916.78MB, major=26.57MB, promoted=23.51MB
    minor collections=918  major collections=9 compactions=0


runtime: 00:03:50.501
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 main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1942.52MB, max=14.22MB, minor=1939.46MB, major=26.78MB, promoted=23.71MB
    minor collections=928  major collections=9 compactions=0


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

|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 main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1963.49MB, max=14.22MB, minor=1960.43MB, major=26.97MB, promoted=23.91MB
    minor collections=938  major collections=9 compactions=0


runtime: 00:04:10.498
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 main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=1978.82MB, max=14.22MB, minor=1975.75MB, major=27.05MB, promoted=23.99MB
    minor collections=946  major collections=9 compactions=0


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

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

Memory statistics: total=1984.10MB, max=14.22MB, minor=1981.03MB, major=27.08MB, promoted=24.02MB
    minor collections=948  major collections=9 compactions=0


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

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

Memory statistics: total=1990.65MB, max=14.22MB, minor=1987.58MB, major=27.14MB, promoted=24.08MB
    minor collections=951  major collections=9 compactions=0


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

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

Memory statistics: total=1995.84MB, max=14.22MB, minor=1992.77MB, major=27.18MB, promoted=24.11MB
    minor collections=954  major collections=9 compactions=0


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

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

Memory statistics: total=1998.71MB, max=14.22MB, minor=1995.64MB, major=27.20MB, promoted=24.13MB
    minor collections=955  major collections=9 compactions=0


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

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

Memory statistics: total=1999.09MB, max=14.22MB, minor=1996.03MB, major=27.20MB, promoted=24.13MB
    minor collections=955  major collections=9 compactions=0


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

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

Memory statistics: total=2000.68MB, max=14.22MB, minor=1997.62MB, major=27.22MB, promoted=24.15MB
    minor collections=956  major collections=9 compactions=0


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

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

Memory statistics: total=2000.76MB, max=14.22MB, minor=1997.69MB, major=27.22MB, promoted=24.15MB
    minor collections=956  major collections=9 compactions=0


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

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

Memory statistics: total=2000.88MB, max=14.22MB, minor=1997.81MB, major=27.22MB, promoted=24.15MB
    minor collections=956  major collections=9 compactions=0


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

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

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


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

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

Memory statistics: total=2014.84MB, max=14.22MB, minor=2011.77MB, major=27.35MB, promoted=24.28MB
    minor collections=963  major collections=9 compactions=0


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

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

Memory statistics: total=2020.78MB, max=14.22MB, minor=2017.72MB, major=27.38MB, promoted=24.32MB
    minor collections=966  major collections=9 compactions=0


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

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

Memory statistics: total=2022.72MB, max=14.22MB, minor=2019.65MB, major=27.41MB, promoted=24.34MB
    minor collections=967  major collections=9 compactions=0


runtime: 00:07:00.506
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 main (2012) on ../plain/cohencu-ll_valuebound50.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound50.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound50.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound50.c:11:1-13:1

Memory statistics: total=2031.04MB, max=14.22MB, minor=2027.97MB, major=27.47MB, promoted=24.40MB
    minor collections=971  major collections=9 compactions=0


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

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

Memory statistics: total=2044.60MB, max=14.22MB, minor=2041.53MB, major=27.57MB, promoted=24.50MB
    minor collections=977  major collections=9 compactions=0


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

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

Memory statistics: total=2051.73MB, max=14.22MB, minor=2048.66MB, major=27.63MB, promoted=24.56MB
    minor collections=980  major collections=9 compactions=0


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

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

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


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

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

Memory statistics: total=2079.59MB, max=14.22MB, minor=2076.52MB, major=27.91MB, promoted=24.84MB
    minor collections=994  major collections=9 compactions=0


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

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

Memory statistics: total=2087.99MB, max=14.22MB, minor=2084.92MB, major=27.95MB, promoted=24.88MB
    minor collections=998  major collections=9 compactions=0


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

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

Memory statistics: total=2091.22MB, max=14.22MB, minor=2088.15MB, major=27.97MB, promoted=24.90MB
    minor collections=999  major collections=9 compactions=0


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

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

Memory statistics: total=2095.04MB, max=14.22MB, minor=2091.96MB, major=28.02MB, promoted=24.95MB
    minor collections=1001  major collections=9 compactions=0


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

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

Memory statistics: total=2097.88MB, max=14.22MB, minor=2094.81MB, major=28.03MB, promoted=24.95MB
    minor collections=1002  major collections=9 compactions=0


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

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

Memory statistics: total=2099.83MB, max=14.22MB, minor=2096.76MB, major=28.04MB, promoted=24.96MB
    minor collections=1003  major collections=9 compactions=0


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

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

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


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

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

Memory statistics: total=2106.25MB, max=14.22MB, minor=2103.17MB, major=28.09MB, promoted=25.01MB
    minor collections=1007  major collections=10 compactions=0


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

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

Memory statistics: total=2108.43MB, max=14.22MB, minor=2105.36MB, major=28.11MB, promoted=25.04MB
    minor collections=1008  major collections=10 compactions=0

