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

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

|rho|=57
|called|=8
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound5.c:8:1-8:76
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound5.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 __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound5.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound5.c:11:1-13:1

Memory statistics: total=798.20MB, max=12.37MB, minor=795.20MB, major=15.79MB, promoted=12.78MB
    minor collections=381  major collections=6 compactions=0


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

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

Memory statistics: total=996.36MB, max=12.37MB, minor=993.35MB, major=17.54MB, promoted=14.53MB
    minor collections=476  major collections=7 compactions=0


runtime: 00:00:30.140
vars: 57, evals: 2162

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

Memory statistics: total=1130.42MB, max=12.37MB, minor=1127.41MB, major=18.81MB, promoted=15.80MB
    minor collections=540  major collections=7 compactions=0


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

|rho|=57
|called|=16
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound5.c:8:1-8:76
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound5.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 __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound5.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound5.c:11:1-13:1

Memory statistics: total=1230.48MB, max=12.37MB, minor=1227.46MB, major=19.74MB, promoted=16.72MB
    minor collections=588  major collections=7 compactions=0


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

Memory statistics: total=1315.65MB, max=12.37MB, minor=1312.62MB, major=20.50MB, promoted=17.48MB
    minor collections=628  major collections=7 compactions=0


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

Memory statistics: total=1390.81MB, max=12.37MB, minor=1387.78MB, major=21.26MB, promoted=18.23MB
    minor collections=665  major collections=8 compactions=0


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

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

Memory statistics: total=1453.14MB, max=12.37MB, minor=1450.11MB, major=21.83MB, promoted=18.80MB
    minor collections=695  major collections=8 compactions=0


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

|rho|=57
|called|=14
|stable|=57
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound5.c:8:1-8:76
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound5.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 __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound5.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound5.c:11:1-13:1

Memory statistics: total=1512.00MB, max=12.37MB, minor=1508.97MB, major=22.43MB, promoted=19.40MB
    minor collections=723  major collections=8 compactions=0


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

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

Memory statistics: total=1564.46MB, max=14.22MB, minor=1561.42MB, major=23.03MB, promoted=19.99MB
    minor collections=748  major collections=8 compactions=0


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

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

Memory statistics: total=1611.43MB, max=14.22MB, minor=1608.38MB, major=23.41MB, promoted=20.37MB
    minor collections=770  major collections=8 compactions=0


runtime: 00:01:50.176
vars: 57, evals: 3174

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

Memory statistics: total=1655.02MB, max=14.22MB, minor=1651.98MB, major=23.81MB, promoted=20.77MB
    minor collections=791  major collections=8 compactions=0


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

|rho|=57
|called|=17
|stable|=52
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound5.c:8:1-8:76
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound5.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 __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound5.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound5.c:11:1-13:1

Memory statistics: total=1695.01MB, max=14.22MB, minor=1691.97MB, major=24.20MB, promoted=21.16MB
    minor collections=810  major collections=8 compactions=0


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

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

Memory statistics: total=1732.23MB, max=14.22MB, minor=1729.18MB, major=24.53MB, promoted=21.48MB
    minor collections=828  major collections=8 compactions=0


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

Memory statistics: total=1766.00MB, max=14.22MB, minor=1762.95MB, major=24.84MB, promoted=21.79MB
    minor collections=844  major collections=9 compactions=0


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

Memory statistics: total=1795.81MB, max=14.22MB, minor=1792.76MB, major=25.09MB, promoted=22.04MB
    minor collections=858  major collections=9 compactions=0


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

Memory statistics: total=1822.35MB, max=14.22MB, minor=1819.30MB, major=25.33MB, promoted=22.27MB
    minor collections=871  major collections=9 compactions=0


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

|rho|=57
|called|=18
|stable|=53
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound5.c:8:1-8:76
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound5.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 __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound5.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound5.c:11:1-13:1

Memory statistics: total=1850.41MB, max=14.22MB, minor=1847.35MB, major=25.58MB, promoted=22.52MB
    minor collections=884  major collections=9 compactions=0


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

Memory statistics: total=1872.77MB, max=14.22MB, minor=1869.71MB, major=25.80MB, promoted=22.74MB
    minor collections=895  major collections=9 compactions=0


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

Memory statistics: total=1886.57MB, max=14.22MB, minor=1883.51MB, major=25.87MB, promoted=22.82MB
    minor collections=902  major collections=9 compactions=0


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

Memory statistics: total=1888.54MB, max=14.22MB, minor=1885.49MB, major=25.90MB, promoted=22.84MB
    minor collections=903  major collections=9 compactions=0


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

Memory statistics: total=1903.14MB, max=14.22MB, minor=1900.08MB, major=26.03MB, promoted=22.98MB
    minor collections=910  major collections=9 compactions=0


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

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

Memory statistics: total=1919.82MB, max=14.22MB, minor=1916.76MB, major=26.17MB, promoted=23.11MB
    minor collections=918  major collections=9 compactions=0


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

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

Memory statistics: total=1943.15MB, max=14.22MB, minor=1940.09MB, major=26.36MB, promoted=23.30MB
    minor collections=929  major collections=9 compactions=0


runtime: 00:04:00.295
vars: 57, evals: 3790

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

Memory statistics: total=1964.53MB, max=14.22MB, minor=1961.47MB, major=26.55MB, promoted=23.49MB
    minor collections=939  major collections=9 compactions=0


runtime: 00:04:13.126
vars: 57, evals: 3818

|rho|=57
|called|=18
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound5.c:8:1-8:76
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound5.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 __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound5.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound5.c:11:1-13:1

Memory statistics: total=1979.29MB, max=14.22MB, minor=1976.22MB, major=26.70MB, promoted=23.64MB
    minor collections=946  major collections=9 compactions=0


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

Memory statistics: total=1983.09MB, max=14.22MB, minor=1980.03MB, major=26.73MB, promoted=23.67MB
    minor collections=948  major collections=9 compactions=0


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

Memory statistics: total=1989.64MB, max=14.22MB, minor=1986.57MB, major=26.77MB, promoted=23.71MB
    minor collections=951  major collections=9 compactions=0


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

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

Memory statistics: total=1996.06MB, max=14.22MB, minor=1992.99MB, major=26.81MB, promoted=23.74MB
    minor collections=954  major collections=9 compactions=0


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

Memory statistics: total=1997.69MB, max=14.22MB, minor=1994.62MB, major=26.82MB, promoted=23.75MB
    minor collections=955  major collections=9 compactions=0


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

Memory statistics: total=1998.07MB, max=14.22MB, minor=1995.01MB, major=26.82MB, promoted=23.75MB
    minor collections=955  major collections=9 compactions=0


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

Memory statistics: total=1999.66MB, max=14.22MB, minor=1996.60MB, major=26.84MB, promoted=23.78MB
    minor collections=956  major collections=9 compactions=0


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

Memory statistics: total=1999.74MB, max=14.22MB, minor=1996.67MB, major=26.84MB, promoted=23.78MB
    minor collections=956  major collections=9 compactions=0


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

Memory statistics: total=1999.86MB, max=14.22MB, minor=1996.79MB, major=26.84MB, promoted=23.78MB
    minor collections=956  major collections=9 compactions=0


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

Memory statistics: total=2005.17MB, max=14.22MB, minor=2002.11MB, major=26.87MB, promoted=23.81MB
    minor collections=958  major collections=9 compactions=0


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

Memory statistics: total=2013.87MB, max=14.22MB, minor=2010.80MB, major=26.96MB, promoted=23.90MB
    minor collections=962  major collections=9 compactions=0


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

|rho|=57
|called|=12
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound5.c:8:1-8:76
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound5.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 __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound5.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound5.c:11:1-13:1

Memory statistics: total=2020.09MB, max=14.22MB, minor=2017.03MB, major=27.00MB, promoted=23.94MB
    minor collections=965  major collections=9 compactions=0


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

Memory statistics: total=2021.72MB, max=14.22MB, minor=2018.65MB, major=27.03MB, promoted=23.96MB
    minor collections=966  major collections=9 compactions=0


runtime: 00:07:00.656
vars: 57, evals: 3936

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

Memory statistics: total=2033.64MB, max=14.22MB, minor=2030.57MB, major=27.13MB, promoted=24.06MB
    minor collections=972  major collections=9 compactions=0


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

Memory statistics: total=2043.62MB, max=14.22MB, minor=2040.55MB, major=27.21MB, promoted=24.14MB
    minor collections=977  major collections=9 compactions=0


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

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

Memory statistics: total=2054.24MB, max=14.22MB, minor=2051.17MB, major=27.31MB, promoted=24.24MB
    minor collections=982  major collections=9 compactions=0


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

|rho|=57
|called|=18
|stable|=52
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound5.c:8:1-8:76
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound5.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 __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound5.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound5.c:11:1-13:1

Memory statistics: total=2069.77MB, max=14.22MB, minor=2066.70MB, major=27.44MB, promoted=24.37MB
    minor collections=989  major collections=9 compactions=0


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

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

Memory statistics: total=2079.80MB, max=14.22MB, minor=2076.73MB, major=27.49MB, promoted=24.42MB
    minor collections=994  major collections=9 compactions=0


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

|rho|=57
|called|=8
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound5.c:8:1-8:76
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound5.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 __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound5.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound5.c:11:1-13:1

Memory statistics: total=2088.62MB, max=14.22MB, minor=2085.55MB, major=27.57MB, promoted=24.50MB
    minor collections=998  major collections=9 compactions=0


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

|rho|=57
|called|=18
|stable|=52
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound5.c:8:1-8:76
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound5.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 __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound5.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound5.c:11:1-13:1

Memory statistics: total=2091.73MB, max=14.22MB, minor=2088.66MB, major=27.61MB, promoted=24.54MB
    minor collections=999  major collections=9 compactions=0


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

Memory statistics: total=2093.99MB, max=14.22MB, minor=2090.92MB, major=27.65MB, promoted=24.58MB
    minor collections=1001  major collections=9 compactions=0


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

Memory statistics: total=2096.83MB, max=14.22MB, minor=2093.76MB, major=27.67MB, promoted=24.60MB
    minor collections=1002  major collections=9 compactions=0


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

|rho|=57
|called|=18
|stable|=55
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of reach_error (1999) on ../plain/cohencu-ll_valuebound5.c:8:1-8:76
1	contexts for entry state of main (2012) on ../plain/cohencu-ll_valuebound5.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 __VERIFIER_assert (2009) on ../plain/cohencu-ll_valuebound5.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on ../plain/cohencu-ll_valuebound5.c:11:1-13:1

Memory statistics: total=2100.52MB, max=14.22MB, minor=2097.45MB, major=27.70MB, promoted=24.62MB
    minor collections=1004  major collections=9 compactions=0


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

Memory statistics: total=2102.52MB, max=14.22MB, minor=2099.45MB, major=27.70MB, promoted=24.63MB
    minor collections=1005  major collections=9 compactions=0


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

Memory statistics: total=2105.19MB, max=14.22MB, minor=2102.11MB, major=27.72MB, promoted=24.64MB
    minor collections=1006  major collections=9 compactions=0


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

Memory statistics: total=2108.17MB, max=14.22MB, minor=2105.09MB, major=27.77MB, promoted=24.69MB
    minor collections=1008  major collections=9 compactions=0

