./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.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.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/cohencu-ll.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.077
vars: 43, evals: 1520

|rho|=43
|called|=13
|stable|=43
|infl|=37
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=34
Found 4 contexts for 4 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/cohencu-ll.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 reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/cohencu-ll.c:8:1-8:76
1	contexts for entry state of main (2012) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/cohencu-ll.c:22:1-55:1

Memory statistics: total=759.70MB, max=12.37MB, minor=756.82MB, major=14.13MB, promoted=11.24MB
    minor collections=364  major collections=6 compactions=0


runtime: 00:00:20.102
vars: 43, evals: 1928

|rho|=43
|called|=18
|stable|=42
|infl|=37
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=34
Found 4 contexts for 4 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/cohencu-ll.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 reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/cohencu-ll.c:8:1-8:76
1	contexts for entry state of main (2012) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/cohencu-ll.c:22:1-55:1

Memory statistics: total=958.78MB, max=12.37MB, minor=955.88MB, major=15.88MB, promoted=12.98MB
    minor collections=459  major collections=6 compactions=0


runtime: 00:00:30.115
vars: 43, evals: 2183

|rho|=43
|called|=10
|stable|=42
|infl|=37
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=34
Found 4 contexts for 4 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/cohencu-ll.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 reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/cohencu-ll.c:8:1-8:76
1	contexts for entry state of main (2012) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/cohencu-ll.c:22:1-55:1

Memory statistics: total=1089.82MB, max=12.37MB, minor=1086.92MB, major=17.08MB, promoted=14.18MB
    minor collections=522  major collections=7 compactions=0


runtime: 00:00:40.129
vars: 43, evals: 2407

|rho|=43
|called|=17
|stable|=41
|infl|=37
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=34
Found 4 contexts for 4 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/cohencu-ll.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 reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/cohencu-ll.c:8:1-8:76
1	contexts for entry state of main (2012) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/cohencu-ll.c:22:1-55:1

Memory statistics: total=1196.09MB, max=12.37MB, minor=1193.18MB, major=17.96MB, promoted=15.05MB
    minor collections=572  major collections=7 compactions=0


runtime: 00:00:50.289
vars: 43, evals: 2577

|rho|=43
|called|=17
|stable|=41
|infl|=37
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=34
Found 4 contexts for 4 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/cohencu-ll.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 reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/cohencu-ll.c:8:1-8:76
1	contexts for entry state of main (2012) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/cohencu-ll.c:22:1-55:1

Memory statistics: total=1281.16MB, max=12.37MB, minor=1278.24MB, major=18.73MB, promoted=15.81MB
    minor collections=613  major collections=7 compactions=0


runtime: 00:01:00.144
vars: 43, evals: 2710

|rho|=43
|called|=15
|stable|=43
|infl|=37
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=34
Found 4 contexts for 4 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_assert (2009) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/cohencu-ll.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 reach_error (1999) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/cohencu-ll.c:8:1-8:76
1	contexts for entry state of main (2012) on /mnt/thread-witnesses/replication/sv-benchmarks/c/nla-digbench/cohencu-ll.c:22:1-55:1

Memory statistics: total=1351.24MB, max=12.37MB, minor=1348.33MB, major=19.38MB, promoted=16.47MB
    minor collections=646  major collections=7 compactions=0

