/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint --conf conf/svcomp-yaml-validate.json --enable dbg.timing.enabled --set 'ana.activated[+]' apron --set ana.apron.domain polyhedra --witness.yaml.unassume /mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../results/st-cross-self/ourtool.2023-02-03_08-10-40.files/ourtool/cohencu-ll_valuebound5.yml/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../results/st-cross-self/ourtool.2023-02-03_08-10-40.files/ourtool/cohencu-ll_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.114
vars: 57, evals: 1502

|rho|=57
|called|=9
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of 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.39MB, max=12.37MB, minor=795.38MB, major=16.17MB, promoted=13.16MB
    minor collections=381  major collections=6 compactions=0


runtime: 00:00:20.139
vars: 57, evals: 1892

|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=993.55MB, max=12.37MB, minor=990.54MB, major=18.18MB, promoted=15.17MB
    minor collections=475  major collections=7 compactions=0


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

|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=1127.46MB, max=12.37MB, minor=1124.44MB, major=19.46MB, promoted=16.45MB
    minor collections=539  major collections=7 compactions=0


runtime: 00:00:40.223
vars: 57, evals: 2341

|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=1228.52MB, max=12.37MB, minor=1225.50MB, major=20.52MB, promoted=17.50MB
    minor collections=587  major collections=7 compactions=0


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

|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=1314.58MB, max=12.37MB, minor=1311.55MB, major=21.35MB, promoted=18.32MB
    minor collections=628  major collections=8 compactions=0


runtime: 00:01:00.354
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 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=1388.88MB, max=12.37MB, minor=1385.85MB, major=22.09MB, promoted=19.06MB
    minor collections=664  major collections=8 compactions=0


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

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


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

|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 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=1510.01MB, max=14.22MB, minor=1506.98MB, major=23.22MB, promoted=20.19MB
    minor collections=722  major collections=8 compactions=0


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

|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=1562.51MB, max=14.22MB, minor=1559.47MB, major=23.72MB, promoted=20.68MB
    minor collections=747  major collections=8 compactions=0


runtime: 00:01:40.217
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 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=1609.58MB, max=14.22MB, minor=1606.53MB, major=24.11MB, promoted=21.07MB
    minor collections=769  major collections=8 compactions=0


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

|rho|=57
|called|=18
|stable|=53
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of 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=1653.23MB, max=14.22MB, minor=1650.19MB, major=24.52MB, promoted=21.48MB
    minor collections=790  major collections=9 compactions=0


runtime: 00:02:00.261
vars: 57, evals: 3241

|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 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=1693.82MB, max=14.22MB, minor=1690.77MB, major=24.92MB, promoted=21.88MB
    minor collections=810  major collections=9 compactions=0


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

|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 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=1731.40MB, max=14.22MB, minor=1728.36MB, major=25.25MB, promoted=22.20MB
    minor collections=828  major collections=9 compactions=0


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

|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=1766.39MB, max=14.22MB, minor=1763.34MB, major=25.53MB, promoted=22.48MB
    minor collections=844  major collections=9 compactions=0


runtime: 00:02:30.272
vars: 57, evals: 3444

|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=1794.48MB, max=14.22MB, minor=1791.43MB, major=25.80MB, promoted=22.75MB
    minor collections=858  major collections=9 compactions=0


runtime: 00:02:40.540
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=1823.38MB, max=14.22MB, minor=1820.33MB, major=26.04MB, promoted=22.99MB
    minor collections=872  major collections=9 compactions=0


runtime: 00:02:50.659
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 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=1849.96MB, max=14.22MB, minor=1846.91MB, major=26.35MB, promoted=23.29MB
    minor collections=884  major collections=9 compactions=0


runtime: 00:03:00.610
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 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=1873.22MB, max=14.22MB, minor=1870.17MB, major=26.58MB, promoted=23.52MB
    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 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=1887.12MB, max=14.22MB, minor=1884.07MB, major=26.70MB, promoted=23.64MB
    minor collections=902  major collections=9 compactions=0


runtime: 00:03:23.518
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=1889.66MB, max=14.22MB, minor=1886.60MB, major=26.72MB, promoted=23.66MB
    minor collections=903  major collections=9 compactions=0


runtime: 00:03:30.466
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 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.68MB, max=14.22MB, minor=1900.62MB, major=26.85MB, promoted=23.79MB
    minor collections=910  major collections=9 compactions=0


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

|rho|=57
|called|=17
|stable|=54
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of 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=1920.38MB, max=14.22MB, minor=1917.32MB, major=26.98MB, promoted=23.92MB
    minor collections=918  major collections=9 compactions=0


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

|rho|=57
|called|=17
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of 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=1942.90MB, max=14.22MB, minor=1939.84MB, major=27.18MB, promoted=24.12MB
    minor collections=929  major collections=9 compactions=0


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

|rho|=57
|called|=18
|stable|=54
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of 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=1965.05MB, max=14.22MB, minor=1961.99MB, major=27.41MB, promoted=24.35MB
    minor collections=939  major collections=9 compactions=0


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

|rho|=57
|called|=19
|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=1980.26MB, max=14.22MB, minor=1977.20MB, major=27.54MB, promoted=24.47MB
    minor collections=946  major collections=9 compactions=0


runtime: 00:04:22.702
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=1984.30MB, max=14.22MB, minor=1981.23MB, major=27.57MB, promoted=24.51MB
    minor collections=948  major collections=9 compactions=0


runtime: 00:04:33.586
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=1990.85MB, max=14.22MB, minor=1987.78MB, major=27.62MB, promoted=24.56MB
    minor collections=951  major collections=9 compactions=0


runtime: 00:04:40.369
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 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=1995.98MB, max=14.22MB, minor=1992.91MB, major=27.67MB, promoted=24.60MB
    minor collections=954  major collections=9 compactions=0


runtime: 00:04:58.345
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=1998.91MB, max=14.22MB, minor=1995.84MB, major=27.69MB, promoted=24.63MB
    minor collections=955  major collections=9 compactions=0


runtime: 00:05:01.463
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=1999.29MB, max=14.22MB, minor=1996.23MB, major=27.69MB, promoted=24.63MB
    minor collections=955  major collections=9 compactions=0


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

|rho|=57
|called|=9
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of 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=2000.75MB, max=14.22MB, minor=1997.69MB, major=27.71MB, promoted=24.65MB
    minor collections=956  major collections=9 compactions=0


runtime: 00:05:37.324
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=2000.92MB, max=14.22MB, minor=1997.86MB, major=27.71MB, promoted=24.65MB
    minor collections=956  major collections=9 compactions=0


runtime: 00:06:04.235
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=2000.99MB, max=14.22MB, minor=1997.93MB, major=27.71MB, promoted=24.65MB
    minor collections=956  major collections=9 compactions=0


runtime: 00:06:12.939
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=2001.12MB, max=14.22MB, minor=1998.05MB, major=27.71MB, promoted=24.65MB
    minor collections=956  major collections=9 compactions=0


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

|rho|=57
|called|=17
|stable|=52
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of 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=2004.87MB, max=14.22MB, minor=2001.81MB, major=27.78MB, promoted=24.72MB
    minor collections=958  major collections=9 compactions=0


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

|rho|=57
|called|=17
|stable|=55
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of 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.75MB, max=14.22MB, minor=2010.68MB, major=27.82MB, promoted=24.76MB
    minor collections=962  major collections=9 compactions=0


runtime: 00:06:41.154
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 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.02MB, max=14.22MB, minor=2017.96MB, major=27.89MB, promoted=24.83MB
    minor collections=966  major collections=9 compactions=0


runtime: 00:06:52.012
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=2022.96MB, max=14.22MB, minor=2019.89MB, major=27.94MB, promoted=24.88MB
    minor collections=967  major collections=9 compactions=0


runtime: 00:07:00.789
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 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=2031.20MB, max=14.22MB, minor=2028.13MB, major=28.03MB, promoted=24.96MB
    minor collections=971  major collections=10 compactions=0


runtime: 00:07:10.818
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=2044.86MB, max=14.22MB, minor=2041.79MB, major=28.14MB, promoted=25.07MB
    minor collections=978  major collections=10 compactions=0


runtime: 00:07:20.869
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 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=2051.99MB, max=14.22MB, minor=2048.92MB, major=28.17MB, promoted=25.10MB
    minor collections=981  major collections=10 compactions=0


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

|rho|=57
|called|=19
|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=2069.26MB, max=14.22MB, minor=2066.19MB, major=28.34MB, promoted=25.27MB
    minor collections=989  major collections=10 compactions=0


runtime: 00:07:41.457
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 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.84MB, max=14.22MB, minor=2076.77MB, major=28.44MB, promoted=25.37MB
    minor collections=994  major collections=10 compactions=0


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

|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=2087.93MB, max=14.22MB, minor=2084.86MB, major=28.50MB, promoted=25.43MB
    minor collections=998  major collections=10 compactions=0


runtime: 00:08:01.362
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 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.47MB, max=14.22MB, minor=2088.40MB, major=28.57MB, promoted=25.50MB
    minor collections=1000  major collections=10 compactions=0


runtime: 00:08:15.511
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=2095.28MB, max=14.22MB, minor=2092.21MB, major=28.60MB, promoted=25.53MB
    minor collections=1002  major collections=10 compactions=0


runtime: 00:08:24.590
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=2098.13MB, max=14.22MB, minor=2095.06MB, major=28.62MB, promoted=25.55MB
    minor collections=1003  major collections=10 compactions=0


runtime: 00:08:30.679
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 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.06MB, max=14.22MB, minor=2096.99MB, major=28.63MB, promoted=25.55MB
    minor collections=1004  major collections=10 compactions=0


runtime: 00:08:40.621
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 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=2103.12MB, max=14.22MB, minor=2100.04MB, major=28.64MB, promoted=25.56MB
    minor collections=1005  major collections=10 compactions=0


runtime: 00:08:53.330
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=2106.49MB, max=14.22MB, minor=2103.42MB, major=28.66MB, promoted=25.59MB
    minor collections=1007  major collections=10 compactions=0


runtime: 00:09:00.722
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 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.68MB, max=14.22MB, minor=2105.61MB, major=28.68MB, promoted=25.61MB
    minor collections=1008  major collections=10 compactions=0

