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

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

Memory statistics: total=798.65MB, max=12.37MB, minor=795.65MB, major=16.32MB, promoted=13.32MB
    minor collections=381  major collections=6 compactions=0


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

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

Memory statistics: total=996.31MB, max=12.37MB, minor=993.30MB, major=18.27MB, promoted=15.25MB
    minor collections=476  major collections=7 compactions=0


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

Memory statistics: total=1127.51MB, max=12.37MB, minor=1124.49MB, major=19.52MB, promoted=16.50MB
    minor collections=539  major collections=7 compactions=0


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

Memory statistics: total=1228.56MB, max=12.37MB, minor=1225.54MB, major=20.51MB, promoted=17.48MB
    minor collections=587  major collections=7 compactions=0


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

Memory statistics: total=1314.73MB, max=12.37MB, minor=1311.70MB, major=21.33MB, promoted=18.31MB
    minor collections=629  major collections=8 compactions=0


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

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

Memory statistics: total=1388.30MB, max=12.37MB, minor=1385.27MB, major=22.11MB, promoted=19.08MB
    minor collections=664  major collections=8 compactions=0


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

Memory statistics: total=1450.73MB, max=12.37MB, minor=1447.69MB, major=22.64MB, promoted=19.60MB
    minor collections=693  major collections=8 compactions=0


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

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

Memory statistics: total=1506.90MB, max=14.22MB, minor=1503.86MB, major=23.14MB, promoted=20.11MB
    minor collections=720  major collections=8 compactions=0


runtime: 00:01:30.331
vars: 57, evals: 2986

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

Memory statistics: total=1561.03MB, max=14.22MB, minor=1557.99MB, major=23.68MB, promoted=20.64MB
    minor collections=746  major collections=8 compactions=0


runtime: 00:01:40.532
vars: 57, evals: 3076

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

Memory statistics: total=1607.47MB, max=14.22MB, minor=1604.43MB, major=24.12MB, promoted=21.08MB
    minor collections=768  major collections=8 compactions=0


runtime: 00:01:50.372
vars: 57, evals: 3161

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

Memory statistics: total=1651.12MB, max=14.22MB, minor=1648.07MB, major=24.48MB, promoted=21.43MB
    minor collections=789  major collections=8 compactions=0


runtime: 00:02:00.249
vars: 57, evals: 3230

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

Memory statistics: total=1689.81MB, max=14.22MB, minor=1686.76MB, major=24.88MB, promoted=21.84MB
    minor collections=808  major collections=9 compactions=0


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

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

Memory statistics: total=1726.42MB, max=14.22MB, minor=1723.37MB, major=25.22MB, promoted=22.17MB
    minor collections=825  major collections=9 compactions=0


runtime: 00:02:20.615
vars: 57, evals: 3383

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

Memory statistics: total=1764.35MB, max=14.22MB, minor=1761.30MB, major=25.51MB, promoted=22.46MB
    minor collections=843  major collections=9 compactions=0


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

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

Memory statistics: total=1792.47MB, max=14.22MB, minor=1789.42MB, major=25.73MB, promoted=22.68MB
    minor collections=857  major collections=9 compactions=0


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

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

Memory statistics: total=1821.45MB, max=14.22MB, minor=1818.39MB, major=25.99MB, promoted=22.93MB
    minor collections=871  major collections=9 compactions=0


runtime: 00:02:50.429
vars: 57, evals: 3549

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

Memory statistics: total=1847.83MB, max=14.22MB, minor=1844.78MB, major=26.22MB, promoted=23.16MB
    minor collections=883  major collections=9 compactions=0


runtime: 00:03:00.605
vars: 57, evals: 3600

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

Memory statistics: total=1871.76MB, max=14.22MB, minor=1868.70MB, major=26.46MB, promoted=23.40MB
    minor collections=895  major collections=9 compactions=0


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

Memory statistics: total=1887.05MB, max=14.22MB, minor=1884.00MB, major=26.59MB, promoted=23.53MB
    minor collections=902  major collections=9 compactions=0


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

Memory statistics: total=1889.75MB, max=14.22MB, minor=1886.69MB, major=26.61MB, promoted=23.55MB
    minor collections=903  major collections=9 compactions=0


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

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

Memory statistics: total=1902.29MB, max=14.22MB, minor=1899.23MB, major=26.73MB, promoted=23.67MB
    minor collections=909  major collections=9 compactions=0


runtime: 00:03:40.570
vars: 57, evals: 3698

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

Memory statistics: total=1917.64MB, max=14.22MB, minor=1914.58MB, major=26.82MB, promoted=23.76MB
    minor collections=916  major collections=9 compactions=0


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

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

Memory statistics: total=1940.86MB, max=14.22MB, minor=1937.79MB, major=27.04MB, promoted=23.98MB
    minor collections=928  major collections=9 compactions=0


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

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

Memory statistics: total=1962.31MB, max=14.22MB, minor=1959.25MB, major=27.23MB, promoted=24.17MB
    minor collections=938  major collections=9 compactions=0


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

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

Memory statistics: total=1979.07MB, max=14.22MB, minor=1976.00MB, major=27.38MB, promoted=24.32MB
    minor collections=946  major collections=9 compactions=0


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

Memory statistics: total=1984.39MB, max=14.22MB, minor=1981.32MB, major=27.43MB, promoted=24.36MB
    minor collections=948  major collections=9 compactions=0


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

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

Memory statistics: total=1989.10MB, max=14.22MB, minor=1986.03MB, major=27.48MB, promoted=24.41MB
    minor collections=951  major collections=9 compactions=0


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

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

Memory statistics: total=1995.47MB, max=14.22MB, minor=1992.41MB, major=27.52MB, promoted=24.46MB
    minor collections=954  major collections=9 compactions=0


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

Memory statistics: total=1999.00MB, max=14.22MB, minor=1995.93MB, major=27.55MB, promoted=24.48MB
    minor collections=955  major collections=9 compactions=0


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

Memory statistics: total=1999.38MB, max=14.22MB, minor=1996.32MB, major=27.55MB, promoted=24.48MB
    minor collections=955  major collections=9 compactions=0


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

Memory statistics: total=2000.84MB, max=14.22MB, minor=1997.78MB, major=27.57MB, promoted=24.51MB
    minor collections=956  major collections=9 compactions=0


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

Memory statistics: total=2001.01MB, max=14.22MB, minor=1997.94MB, major=27.57MB, promoted=24.51MB
    minor collections=956  major collections=9 compactions=0


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

Memory statistics: total=2001.08MB, max=14.22MB, minor=1998.02MB, major=27.57MB, promoted=24.51MB
    minor collections=956  major collections=9 compactions=0


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

Memory statistics: total=2001.18MB, max=14.22MB, minor=1998.11MB, major=27.57MB, promoted=24.51MB
    minor collections=956  major collections=9 compactions=0


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

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

Memory statistics: total=2004.30MB, max=14.22MB, minor=2001.23MB, major=27.65MB, promoted=24.58MB
    minor collections=958  major collections=9 compactions=0


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

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

Memory statistics: total=2013.07MB, max=14.22MB, minor=2010.01MB, major=27.71MB, promoted=24.64MB
    minor collections=962  major collections=9 compactions=0


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

Memory statistics: total=2021.11MB, max=14.22MB, minor=2018.04MB, major=27.76MB, promoted=24.69MB
    minor collections=966  major collections=9 compactions=0


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

Memory statistics: total=2023.04MB, max=14.22MB, minor=2019.98MB, major=27.81MB, promoted=24.74MB
    minor collections=967  major collections=9 compactions=0


runtime: 00:07:00.644
vars: 57, evals: 3921

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

Memory statistics: total=2028.48MB, max=14.22MB, minor=2025.41MB, major=27.87MB, promoted=24.80MB
    minor collections=969  major collections=9 compactions=0


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

Memory statistics: total=2044.95MB, max=14.22MB, minor=2041.88MB, major=28.01MB, promoted=24.94MB
    minor collections=977  major collections=9 compactions=0


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

Memory statistics: total=2052.07MB, max=14.22MB, minor=2049.00MB, major=28.09MB, promoted=25.02MB
    minor collections=981  major collections=9 compactions=0


runtime: 00:07:30.712
vars: 57, evals: 3984

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

Memory statistics: total=2066.22MB, max=14.22MB, minor=2063.15MB, major=28.22MB, promoted=25.15MB
    minor collections=988  major collections=10 compactions=0


runtime: 00:07:40.809
vars: 57, evals: 4013

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

Memory statistics: total=2078.10MB, max=14.22MB, minor=2075.03MB, major=28.34MB, promoted=25.27MB
    minor collections=993  major collections=10 compactions=0


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

Memory statistics: total=2087.99MB, max=14.22MB, minor=2084.92MB, major=28.43MB, promoted=25.36MB
    minor collections=998  major collections=10 compactions=0


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

Memory statistics: total=2091.57MB, max=14.22MB, minor=2088.49MB, major=28.49MB, promoted=25.42MB
    minor collections=1000  major collections=10 compactions=0


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

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

Memory statistics: total=2093.92MB, max=14.22MB, minor=2090.85MB, major=28.51MB, promoted=25.44MB
    minor collections=1001  major collections=10 compactions=0


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

Memory statistics: total=2098.23MB, max=14.22MB, minor=2095.15MB, major=28.53MB, promoted=25.46MB
    minor collections=1003  major collections=10 compactions=0


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

Memory statistics: total=2100.15MB, max=14.22MB, minor=2097.08MB, major=28.54MB, promoted=25.47MB
    minor collections=1004  major collections=10 compactions=0


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

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

Memory statistics: total=2102.70MB, max=14.22MB, minor=2099.63MB, major=28.55MB, promoted=25.48MB
    minor collections=1005  major collections=10 compactions=0


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

Memory statistics: total=2106.59MB, max=14.22MB, minor=2103.52MB, major=28.59MB, promoted=25.52MB
    minor collections=1007  major collections=10 compactions=0


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

Memory statistics: total=2108.60MB, max=14.22MB, minor=2105.53MB, major=28.61MB, promoted=25.54MB
    minor collections=1008  major collections=10 compactions=0

