./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_valuebound100.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_valuebound100.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_valuebound100.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.111
vars: 57, evals: 6161

|rho|=57
|called|=16
|stable|=51
|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 main (2012) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound100.c:22:1-56: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_valuebound100.c:11:1-13:1
1	contexts for entry state of reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound100.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_valuebound100.c:14:1-20:1

Memory statistics: total=3090.49MB, max=14.22MB, minor=3087.49MB, major=34.37MB, promoted=31.37MB
    minor collections=1478  major collections=11 compactions=0


runtime: 00:00:20.145
vars: 57, evals: 9163

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

Memory statistics: total=4675.06MB, max=14.22MB, minor=4671.98MB, major=47.50MB, promoted=44.42MB
    minor collections=2235  major collections=14 compactions=0


runtime: 00:00:30.168
vars: 57, evals: 11249

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

Memory statistics: total=5804.22MB, max=16.36MB, minor=5801.09MB, major=56.81MB, promoted=53.68MB
    minor collections=2774  major collections=17 compactions=0


runtime: 00:00:40.195
vars: 57, evals: 12881

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

Memory statistics: total=6705.99MB, max=16.36MB, minor=6702.83MB, major=63.74MB, promoted=60.59MB
    minor collections=3205  major collections=18 compactions=0


runtime: 00:00:50.214
vars: 57, evals: 14224

|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 __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_valuebound100.c:22:1-56: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_valuebound100.c:11:1-13:1
1	contexts for entry state of reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound100.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_valuebound100.c:14:1-20:1

Memory statistics: total=7459.01MB, max=16.36MB, minor=7455.82MB, major=69.75MB, promoted=66.56MB
    minor collections=3565  major collections=19 compactions=0


runtime: 00:01:00.224
vars: 57, evals: 15385

|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_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_valuebound100.c:22:1-56: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_valuebound100.c:11:1-13:1
1	contexts for entry state of reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench-scaling/cohencu-ll_valuebound100.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_valuebound100.c:14:1-20:1

Memory statistics: total=8121.20MB, max=16.36MB, minor=8117.98MB, major=75.66MB, promoted=72.45MB
    minor collections=3881  major collections=21 compactions=0

