./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_valuebound2.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_valuebound2.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_valuebound2.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.098
vars: 57, evals: 5611

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

Memory statistics: total=2811.73MB, max=14.22MB, minor=2808.74MB, major=32.31MB, promoted=29.32MB
    minor collections=1345  major collections=11 compactions=0


runtime: 00:00:20.148
vars: 57, evals: 8692

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

Memory statistics: total=4421.36MB, max=14.22MB, minor=4418.30MB, major=45.74MB, promoted=42.68MB
    minor collections=2114  major collections=14 compactions=0


runtime: 00:00:30.174
vars: 57, evals: 10767

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

Memory statistics: total=5542.10MB, max=16.36MB, minor=5538.99MB, major=55.33MB, promoted=52.22MB
    minor collections=2649  major collections=16 compactions=0


runtime: 00:00:40.200
vars: 57, evals: 12393

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

Memory statistics: total=6437.48MB, max=16.36MB, minor=6434.34MB, major=62.64MB, promoted=59.50MB
    minor collections=3077  major collections=18 compactions=0


runtime: 00:00:50.223
vars: 57, evals: 13816

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

Memory statistics: total=7229.51MB, max=16.36MB, minor=7226.33MB, major=68.69MB, promoted=65.51MB
    minor collections=3455  major collections=19 compactions=0


runtime: 00:01:00.242
vars: 57, evals: 15028

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

Memory statistics: total=7916.03MB, max=16.36MB, minor=7912.83MB, major=73.49MB, promoted=70.29MB
    minor collections=3783  major collections=20 compactions=0

