./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/mine-tutorial-ex4.10.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/mine-tutorial-ex4.10.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/mine-tutorial-ex4.10.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: v == (51) (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.10.i:21:3)
[Warning][Witness] couldn't locate invariant: v == (39) || (!(v == (39)) && v == (13)) || (!(v == (39)) && !(v == (13)) && v == (7)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && v == (19)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && v == (3)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && v == (25)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && !(v == (25)) && v == (31)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && !(v == (25)) && !(v == (31)) && v == (21)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && !(v == (25)) && !(v == (31)) && !(v == (21)) && v == (29)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && !(v == (25)) && !(v == (31)) && !(v == (21)) && !(v == (29)) && v == (41)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && !(v == (25)) && !(v == (31)) && !(v == (21)) && !(v == (29)) && !(v == (41)) && v == (47)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && !(v == (25)) && !(v == (31)) && !(v == (21)) && !(v == (29)) && !(v == (41)) && !(v == (47)) && v == (15)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && !(v == (25)) && !(v == (31)) && !(v == (21)) && !(v == (29)) && !(v == (41)) && !(v == (47)) && !(v == (15)) && v == (17)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && !(v == (25)) && !(v == (31)) && !(v == (21)) && !(v == (29)) && !(v == (41)) && !(v == (47)) && !(v == (15)) && !(v == (17)) && v == (43)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && !(v == (25)) && !(v == (31)) && !(v == (21)) && !(v == (29)) && !(v == (41)) && !(v == (47)) && !(v == (15)) && !(v == (17)) && !(v == (43)) && v == (35)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && !(v == (25)) && !(v == (31)) && !(v == (21)) && !(v == (29)) && !(v == (41)) && !(v == (47)) && !(v == (15)) && !(v == (17)) && !(v == (43)) && !(v == (35)) && v == (49)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && !(v == (25)) && !(v == (31)) && !(v == (21)) && !(v == (29)) && !(v == (41)) && !(v == (47)) && !(v == (15)) && !(v == (17)) && !(v == (43)) && !(v == (35)) && !(v == (49)) && v == (11)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && !(v == (25)) && !(v == (31)) && !(v == (21)) && !(v == (29)) && !(v == (41)) && !(v == (47)) && !(v == (15)) && !(v == (17)) && !(v == (43)) && !(v == (35)) && !(v == (49)) && !(v == (11)) && v == (9)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && !(v == (25)) && !(v == (31)) && !(v == (21)) && !(v == (29)) && !(v == (41)) && !(v == (47)) && !(v == (15)) && !(v == (17)) && !(v == (43)) && !(v == (35)) && !(v == (49)) && !(v == (11)) && !(v == (9)) && v == (37)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && !(v == (25)) && !(v == (31)) && !(v == (21)) && !(v == (29)) && !(v == (41)) && !(v == (47)) && !(v == (15)) && !(v == (17)) && !(v == (43)) && !(v == (35)) && !(v == (49)) && !(v == (11)) && !(v == (9)) && !(v == (37)) && v == (33)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && !(v == (25)) && !(v == (31)) && !(v == (21)) && !(v == (29)) && !(v == (41)) && !(v == (47)) && !(v == (15)) && !(v == (17)) && !(v == (43)) && !(v == (35)) && !(v == (49)) && !(v == (11)) && !(v == (9)) && !(v == (37)) && !(v == (33)) && v == (1)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && !(v == (25)) && !(v == (31)) && !(v == (21)) && !(v == (29)) && !(v == (41)) && !(v == (47)) && !(v == (15)) && !(v == (17)) && !(v == (43)) && !(v == (35)) && !(v == (49)) && !(v == (11)) && !(v == (9)) && !(v == (37)) && !(v == (33)) && !(v == (1)) && v == (5)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && !(v == (25)) && !(v == (31)) && !(v == (21)) && !(v == (29)) && !(v == (41)) && !(v == (47)) && !(v == (15)) && !(v == (17)) && !(v == (43)) && !(v == (35)) && !(v == (49)) && !(v == (11)) && !(v == (9)) && !(v == (37)) && !(v == (33)) && !(v == (1)) && !(v == (5)) && v == (23)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && !(v == (25)) && !(v == (31)) && !(v == (21)) && !(v == (29)) && !(v == (41)) && !(v == (47)) && !(v == (15)) && !(v == (17)) && !(v == (43)) && !(v == (35)) && !(v == (49)) && !(v == (11)) && !(v == (9)) && !(v == (37)) && !(v == (33)) && !(v == (1)) && !(v == (5)) && !(v == (23)) && v == (27)) || (!(v == (39)) && !(v == (13)) && !(v == (7)) && !(v == (19)) && !(v == (3)) && !(v == (25)) && !(v == (31)) && !(v == (21)) && !(v == (29)) && !(v == (41)) && !(v == (47)) && !(v == (15)) && !(v == (17)) && !(v == (43)) && !(v == (35)) && !(v == (49)) && !(v == (11)) && !(v == (9)) && !(v == (37)) && !(v == (33)) && !(v == (1)) && !(v == (5)) && !(v == (23)) && !(v == (27)) && v == (45)) (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.10.i:17:5)
[Info][Witness] unassume invariant: ((((((((((((((((((((((((v == 21 || (! (v == 21) && v == 33)) || ((! (v == 21) && ! (v == 33)) && v == 43)) || (((! (v == 21) && ! (v == 33)) && ! (v == 43)) && v == 39)) || ((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && v == 13)) || (((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && v == 19)) || ((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && v == 51)) || (((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && v == 25)) || ((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && v == 15)) || (((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && v == 23)) || ((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && v == 37)) || (((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && v == 3)) || ((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && v == 27)) || (((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && v == 17)) || ((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && v == 49)) || (((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && v == 9)) || ((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && v == 31)) || (((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && ! (v == 31)) && v == 29)) || ((((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && ! (v == 31)) && ! (v == 29)) && v == 41)) || (((((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && ! (v == 31)) && ! (v == 29)) && ! (v == 41)) && v == 11)) || ((((((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && ! (v == 31)) && ! (v == 29)) && ! (v == 41)) && ! (v == 11)) && v == 5)) || (((((((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && ! (v == 31)) && ! (v == 29)) && ! (v == 41)) && ! (v == 11)) && ! (v == 5)) && v == 45)) || ((((((((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && ! (v == 31)) && ! (v == 29)) && ! (v == 41)) && ! (v == 11)) && ! (v == 5)) && ! (v == 45)) && v == 47)) || (((((((((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && ! (v == 31)) && ! (v == 29)) && ! (v == 41)) && ! (v == 11)) && ! (v == 5)) && ! (v == 45)) && ! (v == 47)) && v == 7)) || ((((((((((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && ! (v == 31)) && ! (v == 29)) && ! (v == 41)) && ! (v == 11)) && ! (v == 5)) && ! (v == 45)) && ! (v == 47)) && ! (v == 7)) && v == 1)) || (((((((((((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && ! (v == 31)) && ! (v == 29)) && ! (v == 41)) && ! (v == 11)) && ! (v == 5)) && ! (v == 45)) && ! (v == 47)) && ! (v == 7)) && ! (v == 1)) && v == 35) (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.10.i:15:7-15:12)
[Info][Witness] unassume invariant: ((((((((((((((((((((((((v == 21 || (! (v == 21) && v == 33)) || ((! (v == 21) && ! (v == 33)) && v == 43)) || (((! (v == 21) && ! (v == 33)) && ! (v == 43)) && v == 39)) || ((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && v == 13)) || (((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && v == 19)) || ((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && v == 51)) || (((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && v == 25)) || ((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && v == 15)) || (((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && v == 23)) || ((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && v == 37)) || (((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && v == 3)) || ((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && v == 27)) || (((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && v == 17)) || ((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && v == 49)) || (((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && v == 9)) || ((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && v == 31)) || (((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && ! (v == 31)) && v == 29)) || ((((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && ! (v == 31)) && ! (v == 29)) && v == 41)) || (((((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && ! (v == 31)) && ! (v == 29)) && ! (v == 41)) && v == 11)) || ((((((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && ! (v == 31)) && ! (v == 29)) && ! (v == 41)) && ! (v == 11)) && v == 5)) || (((((((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && ! (v == 31)) && ! (v == 29)) && ! (v == 41)) && ! (v == 11)) && ! (v == 5)) && v == 45)) || ((((((((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && ! (v == 31)) && ! (v == 29)) && ! (v == 41)) && ! (v == 11)) && ! (v == 5)) && ! (v == 45)) && v == 47)) || (((((((((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && ! (v == 31)) && ! (v == 29)) && ! (v == 41)) && ! (v == 11)) && ! (v == 5)) && ! (v == 45)) && ! (v == 47)) && v == 7)) || ((((((((((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && ! (v == 31)) && ! (v == 29)) && ! (v == 41)) && ! (v == 11)) && ! (v == 5)) && ! (v == 45)) && ! (v == 47)) && ! (v == 7)) && v == 1)) || (((((((((((((((((((((((((! (v == 21) && ! (v == 33)) && ! (v == 43)) && ! (v == 39)) && ! (v == 13)) && ! (v == 19)) && ! (v == 51)) && ! (v == 25)) && ! (v == 15)) && ! (v == 23)) && ! (v == 37)) && ! (v == 3)) && ! (v == 27)) && ! (v == 17)) && ! (v == 49)) && ! (v == 9)) && ! (v == 31)) && ! (v == 29)) && ! (v == 41)) && ! (v == 11)) && ! (v == 5)) && ! (v == 45)) && ! (v == 47)) && ! (v == 7)) && ! (v == 1)) && v == 35) (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.10.i:19:5-19:31)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.10.i:12:1-12:173)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 10
  dead: 1 (1 in uncalled functions)
  total lines: 11
[Warning][Deadcode][CWE-570] condition '! cond' is always false (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.10.i:13:39-13:46)
[Warning][Witness] invariant unconfirmed: v == (21) || (!(v == (21)) && v == (33)) || (!(v == (21)) && !(v == (33)) && v == (43)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && v == (39)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && v == (13)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && v == (19)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && v == (51)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && !(v == (51)) && v == (25)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && !(v == (51)) && !(v == (25)) && v == (15)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && !(v == (51)) && !(v == (25)) && !(v == (15)) && v == (23)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && !(v == (51)) && !(v == (25)) && !(v == (15)) && !(v == (23)) && v == (37)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && !(v == (51)) && !(v == (25)) && !(v == (15)) && !(v == (23)) && !(v == (37)) && v == (3)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && !(v == (51)) && !(v == (25)) && !(v == (15)) && !(v == (23)) && !(v == (37)) && !(v == (3)) && v == (27)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && !(v == (51)) && !(v == (25)) && !(v == (15)) && !(v == (23)) && !(v == (37)) && !(v == (3)) && !(v == (27)) && v == (17)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && !(v == (51)) && !(v == (25)) && !(v == (15)) && !(v == (23)) && !(v == (37)) && !(v == (3)) && !(v == (27)) && !(v == (17)) && v == (49)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && !(v == (51)) && !(v == (25)) && !(v == (15)) && !(v == (23)) && !(v == (37)) && !(v == (3)) && !(v == (27)) && !(v == (17)) && !(v == (49)) && v == (9)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && !(v == (51)) && !(v == (25)) && !(v == (15)) && !(v == (23)) && !(v == (37)) && !(v == (3)) && !(v == (27)) && !(v == (17)) && !(v == (49)) && !(v == (9)) && v == (31)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && !(v == (51)) && !(v == (25)) && !(v == (15)) && !(v == (23)) && !(v == (37)) && !(v == (3)) && !(v == (27)) && !(v == (17)) && !(v == (49)) && !(v == (9)) && !(v == (31)) && v == (29)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && !(v == (51)) && !(v == (25)) && !(v == (15)) && !(v == (23)) && !(v == (37)) && !(v == (3)) && !(v == (27)) && !(v == (17)) && !(v == (49)) && !(v == (9)) && !(v == (31)) && !(v == (29)) && v == (41)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && !(v == (51)) && !(v == (25)) && !(v == (15)) && !(v == (23)) && !(v == (37)) && !(v == (3)) && !(v == (27)) && !(v == (17)) && !(v == (49)) && !(v == (9)) && !(v == (31)) && !(v == (29)) && !(v == (41)) && v == (11)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && !(v == (51)) && !(v == (25)) && !(v == (15)) && !(v == (23)) && !(v == (37)) && !(v == (3)) && !(v == (27)) && !(v == (17)) && !(v == (49)) && !(v == (9)) && !(v == (31)) && !(v == (29)) && !(v == (41)) && !(v == (11)) && v == (5)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && !(v == (51)) && !(v == (25)) && !(v == (15)) && !(v == (23)) && !(v == (37)) && !(v == (3)) && !(v == (27)) && !(v == (17)) && !(v == (49)) && !(v == (9)) && !(v == (31)) && !(v == (29)) && !(v == (41)) && !(v == (11)) && !(v == (5)) && v == (45)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && !(v == (51)) && !(v == (25)) && !(v == (15)) && !(v == (23)) && !(v == (37)) && !(v == (3)) && !(v == (27)) && !(v == (17)) && !(v == (49)) && !(v == (9)) && !(v == (31)) && !(v == (29)) && !(v == (41)) && !(v == (11)) && !(v == (5)) && !(v == (45)) && v == (47)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && !(v == (51)) && !(v == (25)) && !(v == (15)) && !(v == (23)) && !(v == (37)) && !(v == (3)) && !(v == (27)) && !(v == (17)) && !(v == (49)) && !(v == (9)) && !(v == (31)) && !(v == (29)) && !(v == (41)) && !(v == (11)) && !(v == (5)) && !(v == (45)) && !(v == (47)) && v == (7)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && !(v == (51)) && !(v == (25)) && !(v == (15)) && !(v == (23)) && !(v == (37)) && !(v == (3)) && !(v == (27)) && !(v == (17)) && !(v == (49)) && !(v == (9)) && !(v == (31)) && !(v == (29)) && !(v == (41)) && !(v == (11)) && !(v == (5)) && !(v == (45)) && !(v == (47)) && !(v == (7)) && v == (1)) || (!(v == (21)) && !(v == (33)) && !(v == (43)) && !(v == (39)) && !(v == (13)) && !(v == (19)) && !(v == (51)) && !(v == (25)) && !(v == (15)) && !(v == (23)) && !(v == (37)) && !(v == (3)) && !(v == (27)) && !(v == (17)) && !(v == (49)) && !(v == (9)) && !(v == (31)) && !(v == (29)) && !(v == (41)) && !(v == (11)) && !(v == (5)) && !(v == (45)) && !(v == (47)) && !(v == (7)) && !(v == (1)) && v == (35)) (/mnt/thread-witnesses/replication/bench/thread-witnesses/st-lit/prec/mine-tutorial-ex4.10.i:16:3)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 1
  refuted: 0
  error: 2
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 3
SV-COMP result: unknown

vars = 20    evals = 92    narrow_reuses = 4

Timings:
                                  cputime   walltime   allocated   count
Default                            1.024s     1.055s    336.97MB      1×
  preprocess                         0.026s     0.025s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.11MB      4×
  Cabs2cil                           0.005s     0.006s      4.70MB      4×
  mergeCIL                           0.003s     0.003s      3.33MB      1×
  analysis                           0.981s     1.005s    319.89MB      1×
    createCFG                          0.001s     0.001s      0.59MB      1×
      handle                             0.001s     0.001s      0.08MB     33×
      iter_connect                       0.001s     0.001s      0.40MB     33×
        computeSCCs                        0.001s     0.001s      0.23MB     34×
    FrontC                             0.007s     0.007s      2.71MB      2×
    Cabs2cil                           0.002s     0.002s      2.10MB      2×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            0.538s     0.562s    278.42MB      1×
      S.Dom.equal                        0.001s     0.001s      0.04MB     96×
      base unassume                      0.152s     0.154s    222.51MB     17×
      cheap_full_reach                   0.001s     0.001s      0.01MB      1×
      postsolver                         0.005s     0.005s      5.15MB      1×
        postsolver_iter                    0.005s     0.005s      5.12MB      1×
    warn_global                        0.001s     0.001s      0.07MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
