./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_valuebound1.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_valuebound1.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_valuebound1.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.129
vars: 57, evals: 6397

|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 main (2012) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:11:1-13:1

Memory statistics: total=3209.37MB, max=14.22MB, minor=3206.36MB, major=35.09MB, promoted=32.08MB
    minor collections=1534  major collections=11 compactions=0


runtime: 00:00:20.164
vars: 57, evals: 9311

|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 main (2012) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:11:1-13:1

Memory statistics: total=4753.08MB, max=14.22MB, minor=4750.00MB, major=48.20MB, promoted=45.12MB
    minor collections=2272  major collections=15 compactions=0


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

|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 main (2012) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:11:1-13:1

Memory statistics: total=5861.26MB, max=16.36MB, minor=5858.13MB, major=57.36MB, promoted=54.24MB
    minor collections=2802  major collections=17 compactions=0


runtime: 00:00:40.185
vars: 57, evals: 12966

|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 main (2012) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:11:1-13:1

Memory statistics: total=6749.37MB, max=16.36MB, minor=6746.21MB, major=64.38MB, promoted=61.22MB
    minor collections=3226  major collections=18 compactions=0


runtime: 00:00:50.208
vars: 57, evals: 14317

|rho|=57
|called|=16
|stable|=55
|infl|=51
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=44
Found 5 contexts for 5 functions. Top 5 functions:
1	contexts for entry state of main (2012) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:11:1-13:1

Memory statistics: total=7505.53MB, max=16.36MB, minor=7502.34MB, major=70.40MB, promoted=67.21MB
    minor collections=3587  major collections=19 compactions=0


runtime: 00:01:00.221
vars: 57, evals: 15481

|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 main (2012) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:22:1-56:1
1	contexts for entry state of __VERIFIER_nondet_ushort (383) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:46:74-46:150
1	contexts for entry state of reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:8:1-8:76
1	contexts for entry state of __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:14:1-20:1
1	contexts for entry state of assume_abort_if_not (2006) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound1.c:11:1-13:1

Memory statistics: total=8168.25MB, max=16.36MB, minor=8165.04MB, major=75.52MB, promoted=72.31MB
    minor collections=3904  major collections=21 compactions=0

