/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint --conf conf/svcomp-yaml-validate.json --enable dbg.timing.enabled --set 'ana.activated[+]' apron --set ana.apron.domain polyhedra --witness.yaml.unassume graves-cpa/hard-ll_valuebound20.yml.witness.yml --witness.yaml.validate graves-cpa/hard-ll_valuebound20.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/hard-ll_valuebound20.c


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


--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: (p == (2LL) && q == (6LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (6LL)))) && p == (1LL) && q == (12LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (6LL)))) && !(q == (12LL)) && p == (1LL) && q == (20LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (6LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (12LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && p == (16LL) && q == (16LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (6LL)))) && !(q == (12LL)) && !(q == (20LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && p == (1LL) && q == (7LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (6LL)))) && !(p == (1LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && p == (4LL) && q == (20LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (6LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (12LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (7LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (20LL)))) && p == (8LL) && q == (8LL)) || (!(p == (2LL)) && !(q == (12LL)) && !(q == (20LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (7LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (8LL)))) && p == (1LL) && q == (6LL)) || (!(q == (12LL)) && !(q == (20LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (7LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (8LL)))) && !(q == (6LL)) && p == (1LL) && q == (11LL)) || (!(q == (12LL)) && !(q == (20LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (7LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (8LL)))) && !(q == (6LL)) && !(q == (11LL)) && p == (1LL) && q == (18LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (6LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (12LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && !(q == (16LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (7LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (20LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (8LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (11LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && p == (16LL) && q == (0LL)) || (!(q == (12LL)) && !(q == (20LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (7LL)) && !(p == (8LL)) && !(q == (6LL)) && !(q == (11LL)) && !(q == (18LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && p == (1LL) && q == (8LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (6LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (12LL)))) && !(p == (16LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (7LL)))) && !(q == (20LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (8LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (11LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (8LL)))) && p == (4LL) && q == (16LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (6LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (12LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (7LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (20LL)))) && !(q == (8LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (11LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && !(p == (16LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && p == (8LL) && q == (0LL)) || (!(q == (6LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (12LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (7LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (20LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (8LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (11LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (8LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (0LL)))) && p == (2LL) && q == (4LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (6LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (12LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (7LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (20LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (11LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && !(p == (16LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (8LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && !(p == (8LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (4LL)))) && p == (32LL) && q == (0LL)) || (!(q == (12LL)) && !(q == (20LL)) && !(q == (7LL)) && !(q == (6LL)) && !(q == (11LL)) && !(q == (18LL)) && !(p == (16LL)) && !(q == (8LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && !(p == (8LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (4LL)))) && !(p == (32LL)) && p == (1LL) && q == (0LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (6LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (12LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && !(p == (16LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (7LL)))) && !(q == (8LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (11LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && !(p == (4LL)) && !(q == (0LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (4LL)))) && p == (8LL) && q == (16LL)) || (!(q == (12LL)) && !(q == (20LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (7LL)) && !(q == (6LL)) && !(q == (11LL)) && !(q == (18LL)) && !(q == (8LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (4LL)))) && !(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && p == (1LL) && q == (17LL)) || (!(q == (12LL)) && !(q == (20LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (7LL)) && !(q == (6LL)) && !(q == (11LL)) && !(q == (18LL)) && !(q == (8LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (4LL)))) && !(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && !(q == (17LL)) && p == (1LL) && q == (9LL)) || (!(q == (6LL)) && !(p == (1LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (20LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (8LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (0LL)))) && !(q == (4LL)) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && p == (2LL) && q == (12LL)) || (!(q == (6LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (7LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (20LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (8LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (11LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (8LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (0LL)))) && !(q == (4LL)) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (17LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (9LL)))) && !(q == (12LL)) && p == (2LL) && q == (10LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (6LL)))) && !(q == (20LL)) && !(p == (8LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && !(p == (1LL)) && !(q == (16LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (4LL)))) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (12LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (10LL)))) && p == (4LL) && q == (8LL)) || (!(p == (1LL)) && !(q == (20LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && !(q == (16LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (0LL)))) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && !(p == (2LL)) && !(q == (8LL)) && p == (4LL) && q == (12LL)) || ((!(p == (1LL)) || (p == (1LL) && !(q == (7LL)))) && !(q == (20LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (6LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (11LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (18LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && !(q == (16LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (0LL)))) && !(p == (2LL)) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (17LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (9LL)))) && !(q == (8LL)) && !(q == (12LL)) && p == (4LL) && q == (4LL)) || (!(q == (12LL)) && !(q == (20LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (7LL)) && !(q == (6LL)) && !(q == (11LL)) && !(q == (18LL)) && !(q == (8LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (4LL)))) && !(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (9LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (10LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (4LL)))) && p == (1LL) && q == (13LL)) || (!(q == (12LL)) && !(q == (20LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (7LL)) && !(q == (6LL)) && !(q == (11LL)) && !(q == (18LL)) && !(q == (8LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (4LL)))) && !(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (9LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (10LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (4LL)))) && !(q == (13LL)) && p == (1LL) && q == (14LL)) || (!(q == (12LL)) && !(q == (20LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (7LL)) && !(q == (6LL)) && !(q == (11LL)) && !(q == (18LL)) && !(q == (8LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (4LL)))) && !(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (9LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (10LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (4LL)))) && !(q == (13LL)) && !(q == (14LL)) && p == (1LL) && q == (2LL)) || (!(q == (12LL)) && !(q == (20LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (7LL)) && !(q == (6LL)) && !(q == (11LL)) && !(q == (18LL)) && !(q == (8LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (4LL)))) && !(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (9LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (10LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (4LL)))) && !(q == (13LL)) && !(q == (14LL)) && !(q == (2LL)) && p == (1LL) && q == (3LL)) || (!(q == (6LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (20LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (8LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (0LL)))) && !(q == (4LL)) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && !(q == (12LL)) && !(q == (10LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (8LL)))) && !(p == (1LL)) && p == (2LL) && q == (2LL)) || (!(q == (6LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (20LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (8LL)))) && !(p == (1LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (0LL)))) && !(q == (4LL)) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && !(q == (12LL)) && !(q == (10LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (8LL)))) && !(q == (2LL)) && p == (2LL) && q == (18LL)) || (!(q == (12LL)) && !(q == (20LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (7LL)) && !(q == (6LL)) && !(q == (11LL)) && !(q == (18LL)) && !(q == (8LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (4LL)))) && !(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (9LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (10LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (4LL)))) && !(q == (13LL)) && !(q == (14LL)) && !(q == (2LL)) && !(q == (3LL)) && p == (1LL) && q == (5LL)) || (!(q == (6LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (20LL)))) && !(p == (16LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (7LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (11LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (8LL)))) && !(p == (4LL)) && !(q == (4LL)) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (0LL)))) && !(p == (8LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (17LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (9LL)))) && !(q == (12LL)) && !(q == (10LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (13LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (14LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (3LL)))) && !(q == (2LL)) && !(q == (18LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (5LL)))) && p == (2LL) && q == (16LL)) || (!(q == (6LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (20LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (8LL)))) && (!(p == (16LL)) || (p == (16LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (0LL)))) && !(q == (4LL)) && (!(p == (32LL)) || (p == (32LL) && !(q == (0LL)))) && !(q == (12LL)) && !(q == (10LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (8LL)))) && !(p == (1LL)) && !(q == (2LL)) && !(q == (18LL)) && !(q == (16LL)) && p == (2LL) && q == (14LL)) || (!(q == (12LL)) && !(q == (20LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (7LL)) && !(q == (6LL)) && !(q == (11LL)) && !(q == (18LL)) && !(q == (8LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (2LL)) || (p == (2LL) && !(q == (4LL)))) && !(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (9LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (10LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (4LL)))) && !(q == (13LL)) && !(q == (14LL)) && !(q == (2LL)) && !(q == (3LL)) && !(q == (5LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (16LL)))) && p == (1LL) && q == (19LL)) || (!(q == (12LL)) && !(q == (20LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (7LL)) && !(q == (6LL)) && !(q == (11LL)) && !(q == (18LL)) && !(q == (8LL)) && !(p == (2LL)) && !(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (9LL)) && !(p == (4LL)) && !(q == (13LL)) && !(q == (14LL)) && !(q == (2LL)) && !(q == (3LL)) && !(q == (5LL)) && !(q == (19LL)) && p == (1LL) && q == (4LL)) || (!(q == (12LL)) && !(q == (20LL)) && (!(p == (16LL)) || (p == (16LL) && !(q == (16LL)))) && !(q == (7LL)) && !(q == (6LL)) && !(q == (11LL)) && !(q == (18LL)) && !(q == (8LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && !(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && !(q == (17LL)) && !(q == (9LL)) && !(p == (2LL)) && !(q == (13LL)) && !(q == (14LL)) && !(q == (2LL)) && !(q == (3LL)) && !(q == (5LL)) && !(q == (19LL)) && !(q == (4LL)) && p == (1LL) && q == (10LL)) || (!(q == (12LL)) && !(q == (20LL)) && !(p == (16LL)) && !(q == (7LL)) && !(q == (6LL)) && !(q == (11LL)) && !(q == (18LL)) && !(q == (8LL)) && !(p == (4LL)) && !(q == (0LL)) && !(p == (8LL)) && !(q == (17LL)) && !(q == (9LL)) && !(q == (13LL)) && !(q == (14LL)) && !(q == (2LL)) && !(q == (3LL)) && !(q == (5LL)) && !(p == (2LL)) && !(q == (19LL)) && !(q == (4LL)) && !(q == (10LL)) && p == (1LL) && q == (16LL)) || (!(q == (12LL)) && !(q == (20LL)) && !(q == (7LL)) && !(q == (6LL)) && !(q == (11LL)) && !(q == (18LL)) && !(q == (8LL)) && !(q == (0LL)) && !(q == (17LL)) && !(q == (9LL)) && !(q == (13LL)) && !(q == (14LL)) && !(q == (2LL)) && !(q == (3LL)) && !(q == (5LL)) && !(q == (19LL)) && !(q == (4LL)) && !(q == (10LL)) && !(q == (16LL)) && p == (1LL) && q == (15LL)) || (!(q == (12LL)) && !(q == (20LL)) && !(q == (7LL)) && !(q == (6LL)) && !(q == (11LL)) && !(q == (18LL)) && !(q == (8LL)) && !(q == (0LL)) && !(q == (17LL)) && !(q == (9LL)) && !(q == (13LL)) && !(q == (14LL)) && !(q == (2LL)) && !(q == (3LL)) && !(q == (5LL)) && !(q == (19LL)) && !(q == (4LL)) && !(q == (10LL)) && !(q == (16LL)) && !(q == (15LL)) && p == (1LL) && q == (1LL)) || (!(q == (6LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (20LL)))) && !(p == (16LL)) && !(p == (8LL)) && !(q == (4LL)) && !(p == (32LL)) && !(p == (1LL)) && !(q == (12LL)) && !(q == (10LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (8LL)))) && !(q == (2LL)) && !(q == (18LL)) && !(q == (16LL)) && !(q == (14LL)) && p == (2LL) && q == (0LL)) || (!(q == (6LL)) && !(p == (8LL)) && !(p == (1LL)) && !(q == (4LL)) && !(q == (12LL)) && !(q == (10LL)) && !(p == (4LL)) && !(q == (2LL)) && !(q == (18LL)) && !(q == (16LL)) && !(q == (14LL)) && !(q == (0LL)) && p == (2LL) && q == (8LL)) || (!(q == (6LL)) && !(p == (1LL)) && !(p == (4LL)) && !(q == (4LL)) && !(q == (12LL)) && !(q == (10LL)) && !(q == (2LL)) && !(q == (18LL)) && !(q == (16LL)) && !(q == (14LL)) && !(q == (0LL)) && !(q == (8LL)) && p == (2LL) && q == (20LL)) || (!(q == (20LL)) && !(p == (16LL)) && !(q == (16LL)) && !(p == (8LL)) && !(p == (32LL)) && !(p == (1LL)) && !(q == (8LL)) && !(q == (12LL)) && !(q == (4LL)) && !(p == (2LL)) && p == (4LL) && q == (0LL)) (../plain/hard-ll_valuebound20.c:48:9)
[Warning][Witness] couldn't locate invariant: p == (1LL) && (q == (20LL) || (!(q == (20LL)) && q == (11LL)) || (!(q == (20LL)) && !(q == (11LL)) && q == (8LL)) || (!(q == (20LL)) && !(q == (11LL)) && !(q == (8LL)) && q == (0LL)) || (!(q == (20LL)) && !(q == (11LL)) && !(q == (8LL)) && !(q == (0LL)) && q == (15LL)) || (!(q == (20LL)) && !(q == (11LL)) && !(q == (8LL)) && !(q == (0LL)) && !(q == (15LL)) && q == (17LL)) || (!(q == (20LL)) && !(q == (11LL)) && !(q == (8LL)) && !(q == (0LL)) && !(q == (15LL)) && !(q == (17LL)) && q == (5LL)) || (!(q == (20LL)) && !(q == (11LL)) && !(q == (8LL)) && !(q == (0LL)) && !(q == (15LL)) && !(q == (17LL)) && !(q == (5LL)) && q == (7LL)) || (!(q == (20LL)) && !(q == (11LL)) && !(q == (8LL)) && !(q == (0LL)) && !(q == (15LL)) && !(q == (17LL)) && !(q == (5LL)) && !(q == (7LL)) && q == (1LL)) || (!(q == (20LL)) && !(q == (11LL)) && !(q == (8LL)) && !(q == (0LL)) && !(q == (15LL)) && !(q == (17LL)) && !(q == (5LL)) && !(q == (7LL)) && !(q == (1LL)) && q == (14LL)) || (!(q == (20LL)) && !(q == (11LL)) && !(q == (8LL)) && !(q == (0LL)) && !(q == (15LL)) && !(q == (17LL)) && !(q == (5LL)) && !(q == (7LL)) && !(q == (1LL)) && !(q == (14LL)) && q == (18LL)) || (!(q == (20LL)) && !(q == (11LL)) && !(q == (8LL)) && !(q == (0LL)) && !(q == (15LL)) && !(q == (17LL)) && !(q == (5LL)) && !(q == (7LL)) && !(q == (1LL)) && !(q == (14LL)) && !(q == (18LL)) && q == (9LL)) || (!(q == (20LL)) && !(q == (11LL)) && !(q == (8LL)) && !(q == (0LL)) && !(q == (15LL)) && !(q == (17LL)) && !(q == (5LL)) && !(q == (7LL)) && !(q == (1LL)) && !(q == (14LL)) && !(q == (18LL)) && !(q == (9LL)) && q == (19LL)) || (!(q == (20LL)) && !(q == (11LL)) && !(q == (8LL)) && !(q == (0LL)) && !(q == (15LL)) && !(q == (17LL)) && !(q == (5LL)) && !(q == (7LL)) && !(q == (1LL)) && !(q == (14LL)) && !(q == (18LL)) && !(q == (9LL)) && !(q == (19LL)) && q == (6LL)) || (!(q == (20LL)) && !(q == (11LL)) && !(q == (8LL)) && !(q == (0LL)) && !(q == (15LL)) && !(q == (17LL)) && !(q == (5LL)) && !(q == (7LL)) && !(q == (1LL)) && !(q == (14LL)) && !(q == (18LL)) && !(q == (9LL)) && !(q == (19LL)) && !(q == (6LL)) && q == (2LL)) || (!(q == (20LL)) && !(q == (11LL)) && !(q == (8LL)) && !(q == (0LL)) && !(q == (15LL)) && !(q == (17LL)) && !(q == (5LL)) && !(q == (7LL)) && !(q == (1LL)) && !(q == (14LL)) && !(q == (18LL)) && !(q == (9LL)) && !(q == (19LL)) && !(q == (6LL)) && !(q == (2LL)) && q == (3LL)) || (!(q == (20LL)) && !(q == (11LL)) && !(q == (8LL)) && !(q == (0LL)) && !(q == (15LL)) && !(q == (17LL)) && !(q == (5LL)) && !(q == (7LL)) && !(q == (1LL)) && !(q == (14LL)) && !(q == (18LL)) && !(q == (9LL)) && !(q == (19LL)) && !(q == (6LL)) && !(q == (2LL)) && !(q == (3LL)) && q == (13LL)) || (!(q == (20LL)) && !(q == (11LL)) && !(q == (8LL)) && !(q == (0LL)) && !(q == (15LL)) && !(q == (17LL)) && !(q == (5LL)) && !(q == (7LL)) && !(q == (1LL)) && !(q == (14LL)) && !(q == (18LL)) && !(q == (9LL)) && !(q == (19LL)) && !(q == (6LL)) && !(q == (2LL)) && !(q == (3LL)) && !(q == (13LL)) && q == (4LL)) || (!(q == (20LL)) && !(q == (11LL)) && !(q == (8LL)) && !(q == (0LL)) && !(q == (15LL)) && !(q == (17LL)) && !(q == (5LL)) && !(q == (7LL)) && !(q == (1LL)) && !(q == (14LL)) && !(q == (18LL)) && !(q == (9LL)) && !(q == (19LL)) && !(q == (6LL)) && !(q == (2LL)) && !(q == (3LL)) && !(q == (13LL)) && !(q == (4LL)) && q == (16LL)) || (!(q == (20LL)) && !(q == (11LL)) && !(q == (8LL)) && !(q == (0LL)) && !(q == (15LL)) && !(q == (17LL)) && !(q == (5LL)) && !(q == (7LL)) && !(q == (1LL)) && !(q == (14LL)) && !(q == (18LL)) && !(q == (9LL)) && !(q == (19LL)) && !(q == (6LL)) && !(q == (2LL)) && !(q == (3LL)) && !(q == (13LL)) && !(q == (4LL)) && !(q == (16LL)) && q == (12LL)) || (!(q == (20LL)) && !(q == (11LL)) && !(q == (8LL)) && !(q == (0LL)) && !(q == (15LL)) && !(q == (17LL)) && !(q == (5LL)) && !(q == (7LL)) && !(q == (1LL)) && !(q == (14LL)) && !(q == (18LL)) && !(q == (9LL)) && !(q == (19LL)) && !(q == (6LL)) && !(q == (2LL)) && !(q == (3LL)) && !(q == (13LL)) && !(q == (4LL)) && !(q == (16LL)) && !(q == (12LL)) && q == (10LL))) (../plain/hard-ll_valuebound20.c:50:24)
[Warning][Witness] couldn't locate invariant: (p == (8LL) && q == (0LL)) || ((!(p == (8LL)) || (p == (8LL) && !(q == (0LL)))) && p == (2LL) && q == (8LL)) || (!(p == (8LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (8LL)))) && p == (1LL) && q == (0LL)) || (!(q == (0LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (8LL)))) && p == (8LL) && q == (16LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (8LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (0LL)))) && !(p == (8LL)) && p == (4LL) && q == (16LL)) || ((!(p == (8LL)) || (p == (8LL) && !(q == (0LL)))) && !(p == (2LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (0LL)))) && !(q == (16LL)) && p == (4LL) && q == (8LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (8LL)))) && !(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (8LL)))) && p == (1LL) && q == (12LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (8LL)))) && !(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (8LL)))) && !(q == (12LL)) && p == (1LL) && q == (14LL)) || ((!(p == (8LL)) || (p == (8LL) && !(q == (0LL)))) && !(q == (8LL)) && (!(p == (1LL)) || (p == (1LL) && !(q == (0LL)))) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (12LL)))) && (!(p == (1LL)) || (p == (1LL) && !(q == (14LL)))) && p == (2LL) && q == (20LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (8LL)))) && !(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (8LL)))) && !(q == (12LL)) && !(q == (14LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (20LL)))) && p == (1LL) && q == (4LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (8LL)))) && !(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (8LL)))) && !(q == (12LL)) && !(q == (14LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (20LL)))) && !(q == (4LL)) && p == (1LL) && q == (18LL)) || (!(p == (8LL)) && !(q == (8LL)) && !(p == (1LL)) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && !(q == (20LL)) && p == (2LL) && q == (0LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (8LL)))) && !(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (8LL)))) && !(q == (12LL)) && !(q == (14LL)) && (!(p == (2LL)) || (p == (2LL) && !(q == (20LL)))) && !(q == (4LL)) && !(q == (18LL)) && p == (1LL) && q == (10LL)) || (!(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (8LL)))) && !(q == (12LL)) && !(q == (14LL)) && !(p == (2LL)) && !(q == (4LL)) && !(q == (18LL)) && !(q == (10LL)) && p == (1LL) && q == (20LL)) || (!(q == (8LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && !(q == (20LL)) && !(p == (1LL)) && !(q == (0LL)) && p == (2LL) && q == (4LL)) || (!(p == (8LL)) && !(p == (1LL)) && !(q == (16LL)) && !(q == (8LL)) && !(p == (2LL)) && p == (4LL) && q == (0LL)) || ((!(p == (2LL)) || (p == (2LL) && !(q == (8LL)))) && !(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (8LL)))) && !(q == (12LL)) && !(q == (14LL)) && !(q == (4LL)) && !(q == (18LL)) && !(q == (10LL)) && !(q == (20LL)) && p == (1LL) && q == (6LL)) || (!(p == (2LL)) && !(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && !(p == (4LL)) && !(q == (12LL)) && !(q == (14LL)) && !(q == (4LL)) && !(q == (18LL)) && !(q == (10LL)) && !(q == (20LL)) && !(q == (6LL)) && p == (1LL) && q == (8LL)) || (!(q == (0LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && !(q == (12LL)) && !(q == (14LL)) && !(q == (4LL)) && !(q == (18LL)) && !(q == (10LL)) && !(q == (20LL)) && !(q == (6LL)) && !(q == (8LL)) && p == (1LL) && q == (2LL)) || (!(q == (0LL)) && !(p == (8LL)) && !(p == (4LL)) && !(q == (12LL)) && !(q == (14LL)) && !(q == (4LL)) && !(q == (18LL)) && !(q == (10LL)) && !(q == (20LL)) && !(q == (6LL)) && !(q == (8LL)) && !(q == (2LL)) && p == (1LL) && q == (16LL)) || (!(q == (8LL)) && (!(p == (8LL)) || (p == (8LL) && !(q == (16LL)))) && (!(p == (4LL)) || (p == (4LL) && !(q == (16LL)))) && !(p == (1LL)) && !(q == (20LL)) && !(q == (0LL)) && !(q == (4LL)) && p == (2LL) && q == (12LL)) || (!(q == (8LL)) && !(p == (8LL)) && !(p == (4LL)) && !(q == (20LL)) && !(q == (0LL)) && !(q == (4LL)) && !(p == (1LL)) && !(q == (12LL)) && p == (2LL) && q == (16LL)) || (!(p == (8LL)) && !(p == (1LL)) && !(p == (2LL)) && !(p == (4LL)) && p == (16LL) && q == (0LL)) (../plain/hard-ll_valuebound20.c:52:9)

runtime: 00:00:10.111
vars: 111, evals: 433

|rho|=111
|called|=5
|stable|=110
|infl|=109
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=84
Found 14 contexts for 5 functions. Top 5 functions:
5	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll_valuebound20.c:14:1-20:1
3	contexts for entry state of reach_error (1999) on ../plain/hard-ll_valuebound20.c:8:1-8:73
3	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll_valuebound20.c:11:1-13:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
1	contexts for entry state of main (2012) on ../plain/hard-ll_valuebound20.c:22:1-63:1

Memory statistics: total=2543.21MB, max=21.63MB, minor=2540.17MB, major=226.30MB, promoted=223.26MB
    minor collections=1229  major collections=38 compactions=0


runtime: 00:00:20.141
vars: 111, evals: 707

|rho|=111
|called|=5
|stable|=110
|infl|=109
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=84
Found 14 contexts for 5 functions. Top 5 functions:
5	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll_valuebound20.c:14:1-20:1
3	contexts for entry state of reach_error (1999) on ../plain/hard-ll_valuebound20.c:8:1-8:73
3	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll_valuebound20.c:11:1-13:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
1	contexts for entry state of main (2012) on ../plain/hard-ll_valuebound20.c:22:1-63:1

Memory statistics: total=5014.81MB, max=21.63MB, minor=5011.76MB, major=450.25MB, promoted=447.20MB
    minor collections=2424  major collections=70 compactions=0


runtime: 00:00:30.198
vars: 111, evals: 981

|rho|=111
|called|=5
|stable|=110
|infl|=109
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=84
Found 14 contexts for 5 functions. Top 5 functions:
5	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll_valuebound20.c:14:1-20:1
3	contexts for entry state of reach_error (1999) on ../plain/hard-ll_valuebound20.c:8:1-8:73
3	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll_valuebound20.c:11:1-13:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
1	contexts for entry state of main (2012) on ../plain/hard-ll_valuebound20.c:22:1-63:1

Memory statistics: total=7498.08MB, max=21.63MB, minor=7495.02MB, major=671.28MB, promoted=668.22MB
    minor collections=3624  major collections=101 compactions=0


runtime: 00:00:40.224
vars: 111, evals: 1238

|rho|=111
|called|=5
|stable|=102
|infl|=109
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=84
Found 14 contexts for 5 functions. Top 5 functions:
5	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll_valuebound20.c:14:1-20:1
3	contexts for entry state of reach_error (1999) on ../plain/hard-ll_valuebound20.c:8:1-8:73
3	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll_valuebound20.c:11:1-13:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
1	contexts for entry state of main (2012) on ../plain/hard-ll_valuebound20.c:22:1-63:1

Memory statistics: total=9858.70MB, max=21.63MB, minor=9855.62MB, major=881.44MB, promoted=878.36MB
    minor collections=4764  major collections=130 compactions=0


runtime: 00:00:50.248
vars: 111, evals: 1502

|rho|=111
|called|=5
|stable|=110
|infl|=109
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=84
Found 14 contexts for 5 functions. Top 5 functions:
5	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll_valuebound20.c:14:1-20:1
3	contexts for entry state of reach_error (1999) on ../plain/hard-ll_valuebound20.c:8:1-8:73
3	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll_valuebound20.c:11:1-13:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
1	contexts for entry state of main (2012) on ../plain/hard-ll_valuebound20.c:22:1-63:1

Memory statistics: total=12192.29MB, max=21.63MB, minor=12189.21MB, major=1091.39MB, promoted=1088.31MB
    minor collections=5891  major collections=160 compactions=0


runtime: 00:01:00.279
vars: 111, evals: 1767

|rho|=111
|called|=5
|stable|=110
|infl|=109
|wpoint|=4
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=84
Found 14 contexts for 5 functions. Top 5 functions:
5	contexts for entry state of __VERIFIER_assert (2009) on ../plain/hard-ll_valuebound20.c:14:1-20:1
3	contexts for entry state of reach_error (1999) on ../plain/hard-ll_valuebound20.c:8:1-8:73
3	contexts for entry state of assume_abort_if_not (2006) on ../plain/hard-ll_valuebound20.c:11:1-13:1
2	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140
1	contexts for entry state of main (2012) on ../plain/hard-ll_valuebound20.c:22:1-63:1

Memory statistics: total=14574.46MB, max=21.63MB, minor=14571.36MB, major=1305.04MB, promoted=1301.94MB
    minor collections=7042  major collections=190 compactions=0

