./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-same/../../../results/st-same/ourtool.2023-01-27_15-24-18.files/loop-head/cohencu-ll_valuebound20.yml/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-same/../../../results/st-same/ourtool.2023-01-27_15-24-18.files/loop-head/cohencu-ll_valuebound20.yml/witness.yml --enable witness.invariant.loop-head --disable witness.invariant.other --disable witness.invariant.accessed --sets ana.specification /mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/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())) )

runtime: 00:00:10.116
vars: 57, evals: 6007

|rho|=57
|called|=10
|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 __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:14:1-20: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 /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:22:1-56:1
1	contexts for entry state of reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:11:1-13:1

Memory statistics: total=3013.61MB, max=14.22MB, minor=3010.61MB, major=34.17MB, promoted=31.17MB
    minor collections=1441  major collections=11 compactions=0


runtime: 00:00:20.137
vars: 57, evals: 9047

|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 __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:14:1-20: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 /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:22:1-56:1
1	contexts for entry state of reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:11:1-13:1

Memory statistics: total=4611.28MB, max=14.22MB, minor=4608.21MB, major=47.46MB, promoted=44.38MB
    minor collections=2204  major collections=14 compactions=0


runtime: 00:00:30.153
vars: 57, evals: 11107

|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 __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:14:1-20: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 /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:22:1-56:1
1	contexts for entry state of reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:11:1-13:1

Memory statistics: total=5726.79MB, max=16.36MB, minor=5723.67MB, major=56.87MB, promoted=53.76MB
    minor collections=2738  major collections=17 compactions=0


runtime: 00:00:40.174
vars: 57, evals: 12711

|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 __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:14:1-20: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 /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:22:1-56:1
1	contexts for entry state of reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:11:1-13:1

Memory statistics: total=6608.49MB, max=16.36MB, minor=6605.34MB, major=64.05MB, promoted=60.90MB
    minor collections=3158  major collections=18 compactions=0


runtime: 00:00:50.194
vars: 57, evals: 14041

|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 __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:14:1-20: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 /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:22:1-56:1
1	contexts for entry state of reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:11:1-13:1

Memory statistics: total=7354.86MB, max=16.36MB, minor=7351.67MB, major=70.00MB, promoted=66.82MB
    minor collections=3515  major collections=20 compactions=0


runtime: 00:01:00.201
vars: 57, evals: 15215

|rho|=57
|called|=16
|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 __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:14:1-20: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 /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:22:1-56:1
1	contexts for entry state of reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:8:1-8:76
1	contexts for entry state of assume_abort_if_not (2006) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound20.c:11:1-13:1

Memory statistics: total=8022.59MB, max=16.36MB, minor=8019.38MB, major=74.89MB, promoted=71.69MB
    minor collections=3834  major collections=21 compactions=0

