/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint --conf conf/svcomp-yaml-validate.json --enable dbg.timing.enabled --set 'ana.activated[+]' apron --set ana.apron.domain polyhedra --witness.yaml.unassume /mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../results/st-cross-self2/ourtool.2023-02-15_09-12-33.files/ourtool/cohencu-ll_valuebound20.yml/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../results/st-cross-self2/ourtool.2023-02-15_09-12-33.files/ourtool/cohencu-ll_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.095
vars: 57, evals: 1513

|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=803.04MB, max=12.37MB, minor=800.04MB, major=16.38MB, promoted=13.38MB
    minor collections=384  major collections=6 compactions=0


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

|rho|=57
|called|=18
|stable|=55
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of 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=1000.08MB, max=12.37MB, minor=997.07MB, major=18.17MB, promoted=15.16MB
    minor collections=478  major collections=7 compactions=0


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

|rho|=57
|called|=18
|stable|=55
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of 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=1131.29MB, max=12.37MB, minor=1128.28MB, major=19.36MB, promoted=16.34MB
    minor collections=541  major collections=7 compactions=0


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

|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=1230.24MB, max=12.37MB, minor=1227.21MB, major=20.32MB, promoted=17.30MB
    minor collections=588  major collections=7 compactions=0


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

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


runtime: 00:01:00.350
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 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=1389.12MB, max=12.37MB, minor=1386.09MB, major=21.93MB, promoted=18.90MB
    minor collections=664  major collections=8 compactions=0


runtime: 00:01:10.240
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.91MB, max=12.37MB, minor=1447.88MB, major=22.46MB, promoted=19.43MB
    minor collections=693  major collections=8 compactions=0


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

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


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

|rho|=57
|called|=17
|stable|=52
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of 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=1563.44MB, max=14.22MB, minor=1560.40MB, major=23.49MB, promoted=20.45MB
    minor collections=747  major collections=8 compactions=0


runtime: 00:01:40.460
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 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=1609.89MB, max=14.22MB, minor=1606.85MB, major=23.87MB, promoted=20.83MB
    minor collections=769  major collections=8 compactions=0


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

|rho|=57
|called|=17
|stable|=53
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of 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=1654.17MB, max=14.22MB, minor=1651.13MB, major=24.25MB, promoted=21.20MB
    minor collections=790  major collections=8 compactions=0


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

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


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

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


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

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


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

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


runtime: 00:02:40.322
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 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=1823.69MB, max=14.22MB, minor=1820.64MB, major=25.76MB, promoted=22.71MB
    minor collections=872  major collections=9 compactions=0


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

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


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

|rho|=57
|called|=17
|stable|=53
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of 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=1874.13MB, max=14.22MB, minor=1871.07MB, major=26.17MB, promoted=23.11MB
    minor collections=896  major collections=9 compactions=0


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

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


runtime: 00:03:22.798
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.91MB, max=14.22MB, minor=1886.85MB, major=26.29MB, promoted=23.24MB
    minor collections=903  major collections=9 compactions=0


runtime: 00:03:30.512
vars: 57, evals: 3676

|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=1906.28MB, max=14.22MB, minor=1903.22MB, major=26.44MB, promoted=23.38MB
    minor collections=911  major collections=9 compactions=0


runtime: 00:03:40.308
vars: 57, evals: 3713

|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=1923.71MB, max=14.22MB, minor=1920.65MB, major=26.61MB, promoted=23.55MB
    minor collections=919  major collections=9 compactions=0


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

|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=1945.42MB, max=14.22MB, minor=1942.36MB, major=26.82MB, promoted=23.76MB
    minor collections=930  major collections=9 compactions=0


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

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


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

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


runtime: 00:04:21.381
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.20MB, max=14.22MB, minor=1981.13MB, major=27.13MB, promoted=24.06MB
    minor collections=948  major collections=9 compactions=0


runtime: 00:04:32.126
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 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=1990.75MB, max=14.22MB, minor=1987.68MB, major=27.19MB, promoted=24.13MB
    minor collections=951  major collections=9 compactions=0


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

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


runtime: 00:04:56.689
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=1998.81MB, max=14.22MB, minor=1995.74MB, major=27.25MB, promoted=24.19MB
    minor collections=955  major collections=9 compactions=0


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

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


runtime: 00:05:35.359
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=2000.78MB, max=14.22MB, minor=1997.72MB, major=27.27MB, promoted=24.20MB
    minor collections=956  major collections=9 compactions=0


runtime: 00:06:02.125
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=2000.86MB, max=14.22MB, minor=1997.79MB, major=27.27MB, promoted=24.20MB
    minor collections=956  major collections=9 compactions=0


runtime: 00:06:10.590
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=2000.98MB, max=14.22MB, minor=1997.91MB, major=27.27MB, promoted=24.20MB
    minor collections=956  major collections=9 compactions=0


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

|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=2006.95MB, max=14.22MB, minor=2003.88MB, major=27.35MB, promoted=24.28MB
    minor collections=959  major collections=9 compactions=0


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

|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 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=2015.58MB, max=14.22MB, minor=2012.51MB, major=27.40MB, promoted=24.33MB
    minor collections=963  major collections=9 compactions=0


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

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


runtime: 00:06:53.499
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=2022.86MB, max=14.22MB, minor=2019.79MB, major=27.48MB, promoted=24.42MB
    minor collections=967  major collections=9 compactions=0


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

|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=2035.27MB, max=14.22MB, minor=2032.20MB, major=27.60MB, promoted=24.53MB
    minor collections=973  major collections=9 compactions=0


runtime: 00:07:10.710
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.77MB, max=14.22MB, minor=2041.70MB, major=27.67MB, promoted=24.60MB
    minor collections=977  major collections=9 compactions=0


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

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


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

|rho|=57
|called|=18
|stable|=52
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of 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=2070.93MB, max=14.22MB, minor=2067.86MB, major=27.99MB, promoted=24.92MB
    minor collections=990  major collections=9 compactions=0


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

|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 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=2081.61MB, max=14.22MB, minor=2078.54MB, major=28.06MB, promoted=24.99MB
    minor collections=995  major collections=9 compactions=0


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

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


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

|rho|=57
|called|=18
|stable|=52
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of 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=2092.90MB, max=14.22MB, minor=2089.83MB, major=28.18MB, promoted=25.11MB
    minor collections=1001  major collections=10 compactions=0


runtime: 00:08:13.709
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 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=2095.17MB, max=14.22MB, minor=2092.09MB, major=28.20MB, promoted=25.13MB
    minor collections=1002  major collections=10 compactions=0


runtime: 00:08:22.847
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.01MB, max=14.22MB, minor=2094.94MB, major=28.22MB, promoted=25.15MB
    minor collections=1003  major collections=10 compactions=0


runtime: 00:08:30.647
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.31MB, max=14.22MB, minor=2097.24MB, major=28.23MB, promoted=25.16MB
    minor collections=1004  major collections=10 compactions=0


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

|rho|=57
|called|=15
|stable|=55
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of 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=2103.71MB, max=14.22MB, minor=2100.64MB, major=28.25MB, promoted=25.18MB
    minor collections=1006  major collections=10 compactions=0


runtime: 00:08:51.597
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.37MB, max=14.22MB, minor=2103.30MB, major=28.27MB, promoted=25.20MB
    minor collections=1007  major collections=10 compactions=0


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

|rho|=57
|called|=14
|stable|=56
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of 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=2109.34MB, max=14.22MB, minor=2106.27MB, major=28.32MB, promoted=25.25MB
    minor collections=1009  major collections=10 compactions=0

