./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_valuebound50.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_valuebound50.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_valuebound50.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.097
vars: 57, evals: 6103

|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 __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound50.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_valuebound50.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_valuebound50.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_valuebound50.c:22:1-56:1

Memory statistics: total=3058.86MB, max=14.22MB, minor=3055.86MB, major=34.16MB, promoted=31.15MB
    minor collections=1462  major collections=11 compactions=0


runtime: 00:00:20.146
vars: 57, evals: 8962

|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 __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 __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound50.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_valuebound50.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_valuebound50.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_valuebound50.c:22:1-56:1

Memory statistics: total=4560.14MB, max=14.22MB, minor=4557.07MB, major=46.70MB, promoted=43.63MB
    minor collections=2180  major collections=14 compactions=0


runtime: 00:00:30.164
vars: 57, evals: 11096

|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 __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 __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound50.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_valuebound50.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_valuebound50.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_valuebound50.c:22:1-56:1

Memory statistics: total=5711.62MB, max=16.36MB, minor=5708.51MB, major=56.12MB, promoted=53.00MB
    minor collections=2730  major collections=16 compactions=0


runtime: 00:00:40.190
vars: 57, evals: 12779

|rho|=57
|called|=16
|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 __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 __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound50.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_valuebound50.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_valuebound50.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_valuebound50.c:22:1-56:1

Memory statistics: total=6640.68MB, max=16.36MB, minor=6637.52MB, major=63.85MB, promoted=60.69MB
    minor collections=3174  major collections=18 compactions=0


runtime: 00:00:50.225
vars: 57, evals: 14156

|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_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 __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound50.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_valuebound50.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_valuebound50.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_valuebound50.c:22:1-56:1

Memory statistics: total=7411.78MB, max=16.36MB, minor=7408.59MB, major=70.07MB, promoted=66.88MB
    minor collections=3542  major collections=19 compactions=0


runtime: 00:01:00.237
vars: 57, evals: 15357

|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 __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 __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound50.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_valuebound50.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_valuebound50.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_valuebound50.c:22:1-56:1

Memory statistics: total=8093.51MB, max=16.36MB, minor=8090.30MB, major=74.90MB, promoted=71.69MB
    minor collections=3868  major collections=20 compactions=0

