./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-lit/../../../results/st-lit-location/convert-tmp.2023-02-16_10-47-42.files/cpachecker/hh-ex3.yml/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/../../../results/st-lit-location/convert-tmp.2023-02-16_10-47-42.files/cpachecker/hh-ex3.yml/witness.yml --sets ana.specification /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/properties/unreach-call.prp --sets exp.architecture 64bit /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex3.i


--------------------------------------------------------------------------------


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Warning][Witness] couldn't locate invariant: j == (4) && i == (4) (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex3.i:32:3)
[Warning][Witness] couldn't locate invariant: (i == (7) && j == (4)) || (i == (6) && j == (4)) || (j == (4) && i == (4)) || (i == (5) && j == (4)) (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex3.i:26:5)

runtime: 00:00:11.920
vars: 20, evals: 38

|rho|=20
|called|=9
|stable|=20
|infl|=18
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=17
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2020) on /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex3.i:14:1-33:1

Memory statistics: total=11118.95MB, max=693.18MB, minor=11105.15MB, major=788.49MB, promoted=774.69MB
    minor collections=5305  major collections=18 compactions=1


runtime: 00:00:21.933
vars: 20, evals: 38

|rho|=20
|called|=9
|stable|=20
|infl|=18
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=17
Found 1 contexts for 1 functions. Top 5 functions:
1	contexts for entry state of main (2020) on /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex3.i:14:1-33:1

Memory statistics: total=11607.04MB, max=693.18MB, minor=11593.24MB, major=788.63MB, promoted=774.83MB
    minor collections=5537  major collections=18 compactions=1


runtime: 00:00:32.036
vars: 29, evals: 70

|rho|=29
|called|=9
|stable|=25
|infl|=27
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=22
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_assert (2017) on /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex3.i:13:1-13:84
1	contexts for entry state of main (2020) on /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex3.i:14:1-33:1

Memory statistics: total=13871.02MB, max=693.18MB, minor=13857.16MB, major=1425.87MB, promoted=1412.01MB
    minor collections=6620  major collections=25 compactions=2


runtime: 00:00:42.103
vars: 29, evals: 70

|rho|=29
|called|=9
|stable|=25
|infl|=27
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=22
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_assert (2017) on /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex3.i:13:1-13:84
1	contexts for entry state of main (2020) on /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex3.i:14:1-33:1

Memory statistics: total=15350.42MB, max=693.18MB, minor=15336.54MB, major=1797.60MB, promoted=1783.72MB
    minor collections=7327  major collections=29 compactions=2


runtime: 00:00:52.170
vars: 29, evals: 70

|rho|=29
|called|=9
|stable|=25
|infl|=27
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=22
Found 2 contexts for 2 functions. Top 5 functions:
1	contexts for entry state of __VERIFIER_assert (2017) on /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex3.i:13:1-13:84
1	contexts for entry state of main (2020) on /mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/hh-ex3.i:14:1-33:1

Memory statistics: total=22868.96MB, max=693.18MB, minor=22855.04MB, major=2075.83MB, promoted=2061.91MB
    minor collections=10914  major collections=33 compactions=3

