/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 cpachecker/large_const.yml.witness.yml --witness.yaml.validate cpachecker/large_const.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/large_const.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 == (1) && c3 == (10000) && c1 == (4000) && i == (1) && c2 == (2000) && k == (3999)) || (c3 == (10000) && c1 == (4000) && c2 == (2000) && i == (1) && j == (1) && k == (1999)) || (c3 == (10000) && c1 == (4000) && c2 == (2000) && j == (0) && i == (0) && k == (0)) || (c3 == (10000) && c1 == (4000) && c2 == (2000) && (!(i == (0)) || (i == (0) && !(j == (0))) || (j == (0) && i == (0) && !(k == (0)))) && i == (1) && j == (1) && k == (9999)) (../plain/large_const.i:51:3)
[Warning][Witness] couldn't locate invariant: c3 == (10000) && c1 == (4000) && i == (1) && j == (0) && c2 == (2000) && (k == (10000) || (!(k == (10000)) && k == (4000)) || (!(k == (10000)) && !(k == (4000)) && k == (2000))) (../plain/large_const.i:47:5)
[Info][Witness] unassume invariant: (((((((((c1 == 4000 && c2 == 2000) && c3 == 10000) && i == 1) && k == 10000) || (((((c1 == 4000 && c2 == 2000) && c3 == 10000) && i == 1) && ! (k == 10000)) && k == 4000)) || ((((((c1 == 4000 && c2 == 2000) && c3 == 10000) && i == 1) && ! (k == 10000)) && ! (k == 4000)) && k == 2000)) || ((((c3 == 10000 && c1 == 4000) && c2 == 2000) && i == 0) && k == 0)) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && (! (i == 0) || (i == 0 && ! (k == 0)))) && i == 1) && k == 4000)) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && i == 1) && k == 2000)) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && i == 1) && k == 10000) (../plain/large_const.i:33:3-33:8)
[Info][Witness] unassume invariant: (((((((((c1 == 4000 && c2 == 2000) && c3 == 10000) && i == 1) && k == 10000) || (((((c1 == 4000 && c2 == 2000) && c3 == 10000) && i == 1) && ! (k == 10000)) && k == 4000)) || ((((((c1 == 4000 && c2 == 2000) && c3 == 10000) && i == 1) && ! (k == 10000)) && ! (k == 4000)) && k == 2000)) || ((((c3 == 10000 && c1 == 4000) && c2 == 2000) && i == 0) && k == 0)) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && (! (i == 0) || (i == 0 && ! (k == 0)))) && i == 1) && k == 4000)) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && i == 1) && k == 2000)) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && i == 1) && k == 10000) (../plain/large_const.i:43:7-43:14)
[Info][Witness] unassume invariant: (((((((((c1 == 4000 && c2 == 2000) && c3 == 10000) && i == 1) && k == 10000) || (((((c1 == 4000 && c2 == 2000) && c3 == 10000) && i == 1) && ! (k == 10000)) && k == 4000)) || ((((((c1 == 4000 && c2 == 2000) && c3 == 10000) && i == 1) && ! (k == 10000)) && ! (k == 4000)) && k == 2000)) || ((((c3 == 10000 && c1 == 4000) && c2 == 2000) && i == 0) && k == 0)) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && (! (i == 0) || (i == 0 && ! (k == 0)))) && i == 1) && k == 4000)) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && i == 1) && k == 2000)) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && i == 1) && k == 10000) (../plain/large_const.i:41:7-41:14)
[Info][Witness] unassume invariant: (((((((((c1 == 4000 && c2 == 2000) && c3 == 10000) && i == 1) && k == 10000) || (((((c1 == 4000 && c2 == 2000) && c3 == 10000) && i == 1) && ! (k == 10000)) && k == 4000)) || ((((((c1 == 4000 && c2 == 2000) && c3 == 10000) && i == 1) && ! (k == 10000)) && ! (k == 4000)) && k == 2000)) || ((((c3 == 10000 && c1 == 4000) && c2 == 2000) && i == 0) && k == 0)) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && (! (i == 0) || (i == 0 && ! (k == 0)))) && i == 1) && k == 4000)) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && i == 1) && k == 2000)) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && i == 1) && k == 10000) (../plain/large_const.i:39:7-39:14)
[Info][Witness] unassume invariant: (((((((c1 == 4000 && c2 == 2000) && c3 == 10000) && i == 0) && k == 0) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && (! (i == 0) || (i == 0 && ! (k == 0)))) && i == 1) && k == 4000)) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && i == 1) && k == 2000)) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && i == 1) && k == 10000)) && ((((((((((((((((c1 == 4000 && c2 == 2000) && c3 == 10000) && j == 1) && i == 1) && k == 1999) || (((((j == 1 && c3 == 10000) && c1 == 4000) && i == 1) && c2 == 2000) && k == 3999)) || (((((j == 1 && c3 == 10000) && c1 == 4000) && i == 1) && c2 == 2000) && k == 9999)) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && j == 0) && i == 0) && k == 0)) || ((((((c3 == 10000 && c1 == 4000) && c2 == 2000) && j == 0) && (! (i == 0) || (i == 0 && ! (k == 0)))) && i == 1) && k == 4000)) || ((((((c3 == 10000 && c1 == 4000) && j == 0) && c2 == 2000) && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && i == 1) && k == 10000)) || ((((((c3 == 10000 && c1 == 4000) && c2 == 2000) && (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && i == 0) && ! (k == 0))) || ((j == 0 && (! (i == 0) || (i == 0 && ! (k == 0)))) && ! (k == 4000))) || ((j == 0 && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && ! (k == 2000))) || ((j == 0 && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && ! (k == 10000)))) && i == 1) && j == 1) && k == 1999)) || ((((((c3 == 10000 && c1 == 4000) && c2 == 2000) && (((((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000))) && ! (j == 1))) || (((((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000))) && j == 1) && ! (k == 1999)))) && i == 1) && j == 0) && k == 10000)) || ((((((c3 == 10000 && c1 == 4000) && c2 == 2000) && (((((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && i == 0) && ! (k == 0))) || ((j == 0 && (! (i == 0) || (i == 0 && ! (k == 0)))) && ! (k == 4000))) || ((j == 0 && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && ! (k == 2000))) || ((j == 0 && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && ! (k == 10000))) || ((((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && i == 0) && ! (k == 0))) || ((j == 0 && (! (i == 0) || (i == 0 && ! (k == 0)))) && ! (k == 4000))) || ((j == 0 && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && ! (k == 2000))) || ((j == 0 && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && ! (k == 10000))) && ! (k == 1999))) || ((((((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000))) && ! (k == 1999))) && j == 0) && ! (k == 10000)))) && i == 1) && j == 1) && k == 3999)) || ((((((c3 == 10000 && c1 == 4000) && c2 == 2000) && ((((((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && i == 0) && ! (k == 0))) || ((j == 0 && (! (i == 0) || (i == 0 && ! (k == 0)))) && ! (k == 4000))) || ((j == 0 && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && ! (k == 2000))) || ((j == 0 && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && ! (k == 10000))) || ((((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && i == 0) && ! (k == 0))) || ((j == 0 && (! (i == 0) || (i == 0 && ! (k == 0)))) && ! (k == 4000))) || ((j == 0 && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && ! (k == 2000))) || ((j == 0 && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && ! (k == 10000))) && ! (k == 1999))) || ((((((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000))) && ! (k == 1999))) && j == 0) && ! (k == 10000))) || ((((((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && i == 0) && ! (k == 0))) || ((j == 0 && (! (i == 0) || (i == 0 && ! (k == 0)))) && ! (k == 4000))) || ((j == 0 && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && ! (k == 2000))) || ((j == 0 && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && ! (k == 10000))) || ((((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && i == 0) && ! (k == 0))) || ((j == 0 && (! (i == 0) || (i == 0 && ! (k == 0)))) && ! (k == 4000))) || ((j == 0 && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && ! (k == 2000))) || ((j == 0 && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && ! (k == 10000))) && ! (k == 1999))) || ((((((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000))) && ! (k == 1999))) && j == 0) && ! (k == 10000))) && ! (k == 3999)))) && i == 1) && j == 1) && k == 9999)) || (((((((c3 == 10000 && c1 == 4000) && c2 == 2000) && ((((((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 10000))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 10000))) && ! (j == 1))) || (((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 10000))) && j == 1) && ! (k == 1999))) || (((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (j == 1))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && j == 1) && ! (k == 1999))) && ! (k == 10000))) || (((((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 10000))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 10000))) && ! (k == 1999))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 1999))) && ! (k == 10000))) && j == 1) && ! (k == 3999))) || ((((((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 10000))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 10000))) && ! (k == 1999))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 1999))) && ! (k == 10000))) || ((((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 10000))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 10000))) && ! (k == 1999))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 1999))) && ! (k == 10000))) && ! (k == 3999))) && j == 1) && ! (k == 9999)))) && (! (i == 0) || (i == 0 && ! (k == 0)))) && i == 1) && j == 0) && k == 4000)) || ((((((c3 == 10000 && c1 == 4000) && c2 == 2000) && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && i == 1) && j == 0) && k == 2000)) (../plain/large_const.i:45:3-45:8)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (../plain/large_const.i:49:5-49:8)
[Info][Witness] unassume invariant: (((((((c1 == 4000 && c2 == 2000) && c3 == 10000) && i == 0) && k == 0) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && (! (i == 0) || (i == 0 && ! (k == 0)))) && i == 1) && k == 4000)) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && i == 1) && k == 2000)) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && i == 1) && k == 10000)) && ((((((((((((((((c1 == 4000 && c2 == 2000) && c3 == 10000) && j == 1) && i == 1) && k == 1999) || (((((j == 1 && c3 == 10000) && c1 == 4000) && i == 1) && c2 == 2000) && k == 3999)) || (((((j == 1 && c3 == 10000) && c1 == 4000) && i == 1) && c2 == 2000) && k == 9999)) || (((((c3 == 10000 && c1 == 4000) && c2 == 2000) && j == 0) && i == 0) && k == 0)) || ((((((c3 == 10000 && c1 == 4000) && c2 == 2000) && j == 0) && (! (i == 0) || (i == 0 && ! (k == 0)))) && i == 1) && k == 4000)) || ((((((c3 == 10000 && c1 == 4000) && j == 0) && c2 == 2000) && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && i == 1) && k == 10000)) || ((((((c3 == 10000 && c1 == 4000) && c2 == 2000) && (((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && i == 0) && ! (k == 0))) || ((j == 0 && (! (i == 0) || (i == 0 && ! (k == 0)))) && ! (k == 4000))) || ((j == 0 && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && ! (k == 2000))) || ((j == 0 && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && ! (k == 10000)))) && i == 1) && j == 1) && k == 1999)) || ((((((c3 == 10000 && c1 == 4000) && c2 == 2000) && (((((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000))) && ! (j == 1))) || (((((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000))) && j == 1) && ! (k == 1999)))) && i == 1) && j == 0) && k == 10000)) || ((((((c3 == 10000 && c1 == 4000) && c2 == 2000) && (((((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && i == 0) && ! (k == 0))) || ((j == 0 && (! (i == 0) || (i == 0 && ! (k == 0)))) && ! (k == 4000))) || ((j == 0 && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && ! (k == 2000))) || ((j == 0 && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && ! (k == 10000))) || ((((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && i == 0) && ! (k == 0))) || ((j == 0 && (! (i == 0) || (i == 0 && ! (k == 0)))) && ! (k == 4000))) || ((j == 0 && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && ! (k == 2000))) || ((j == 0 && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && ! (k == 10000))) && ! (k == 1999))) || ((((((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000))) && ! (k == 1999))) && j == 0) && ! (k == 10000)))) && i == 1) && j == 1) && k == 3999)) || ((((((c3 == 10000 && c1 == 4000) && c2 == 2000) && ((((((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && i == 0) && ! (k == 0))) || ((j == 0 && (! (i == 0) || (i == 0 && ! (k == 0)))) && ! (k == 4000))) || ((j == 0 && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && ! (k == 2000))) || ((j == 0 && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && ! (k == 10000))) || ((((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && i == 0) && ! (k == 0))) || ((j == 0 && (! (i == 0) || (i == 0 && ! (k == 0)))) && ! (k == 4000))) || ((j == 0 && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && ! (k == 2000))) || ((j == 0 && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && ! (k == 10000))) && ! (k == 1999))) || ((((((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000))) && ! (k == 1999))) && j == 0) && ! (k == 10000))) || ((((((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && i == 0) && ! (k == 0))) || ((j == 0 && (! (i == 0) || (i == 0 && ! (k == 0)))) && ! (k == 4000))) || ((j == 0 && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && ! (k == 2000))) || ((j == 0 && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && ! (k == 10000))) || ((((((! (j == 0) || (j == 0 && ! (i == 0))) || ((j == 0 && i == 0) && ! (k == 0))) || ((j == 0 && (! (i == 0) || (i == 0 && ! (k == 0)))) && ! (k == 4000))) || ((j == 0 && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && ! (k == 2000))) || ((j == 0 && (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000)))) && ! (k == 10000))) && ! (k == 1999))) || ((((((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000))) && ! (k == 2000))) && ! (k == 1999))) && j == 0) && ! (k == 10000))) && ! (k == 3999)))) && i == 1) && j == 1) && k == 9999)) || (((((((c3 == 10000 && c1 == 4000) && c2 == 2000) && ((((((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 10000))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 10000))) && ! (j == 1))) || (((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 10000))) && j == 1) && ! (k == 1999))) || (((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (j == 1))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && j == 1) && ! (k == 1999))) && ! (k == 10000))) || (((((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 10000))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 10000))) && ! (k == 1999))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 1999))) && ! (k == 10000))) && j == 1) && ! (k == 3999))) || ((((((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 10000))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 10000))) && ! (k == 1999))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 1999))) && ! (k == 10000))) || ((((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 10000))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 10000))) && ! (k == 1999))) || ((((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) || (((! (i == 0) || (i == 0 && ! (k == 0))) || ! (k == 2000)) && ! (k == 1999))) && ! (k == 10000))) && ! (k == 3999))) && j == 1) && ! (k == 9999)))) && (! (i == 0) || (i == 0 && ! (k == 0)))) && i == 1) && j == 0) && k == 4000)) || ((((((c3 == 10000 && c1 == 4000) && c2 == 2000) && ((! (i == 0) || (i == 0 && ! (k == 0))) || ((! (i == 0) || (i == 0 && ! (k == 0))) && ! (k == 4000)))) && i == 1) && j == 0) && k == 2000)) (../plain/large_const.i:49:5-49:8)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (../plain/large_const.i:14:1-16:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 29
  dead: 2 (2 in uncalled functions)
  total lines: 31
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (../plain/large_const.i:12:73-12:74)
[Warning][Witness] invariant unconfirmed: (c1 == (4000) && c2 == (2000) && c3 == (10000) && j == (1) && i == (1) && k == (1999)) || (j == (1) && c3 == (10000) && c1 == (4000) && i == (1) && c2 == (2000) && k == (3999)) || (j == (1) && c3 == (10000) && c1 == (4000) && i == (1) && c2 == (2000) && k == (9999)) || (c3 == (10000) && c1 == (4000) && c2 == (2000) && j == (0) && i == (0) && k == (0)) || (c3 == (10000) && c1 == (4000) && c2 == (2000) && j == (0) && (!(i == (0)) || (i == (0) && !(k == (0)))) && i == (1) && k == (4000)) || (c3 == (10000) && c1 == (4000) && j == (0) && c2 == (2000) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000)))) && i == (1) && k == (10000)) || (c3 == (10000) && c1 == (4000) && c2 == (2000) && (!(j == (0)) || (j == (0) && !(i == (0))) || (j == (0) && i == (0) && !(k == (0))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000)))) && !(k == (10000)))) && i == (1) && j == (1) && k == (1999)) || (c3 == (10000) && c1 == (4000) && c2 == (2000) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000)))) && !(j == (1))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000)))) && j == (1) && !(k == (1999)))) && i == (1) && j == (0) && k == (10000)) || (c3 == (10000) && c1 == (4000) && c2 == (2000) && (!(j == (0)) || (j == (0) && !(i == (0))) || (j == (0) && i == (0) && !(k == (0))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000)))) && !(k == (10000))) || ((!(j == (0)) || (j == (0) && !(i == (0))) || (j == (0) && i == (0) && !(k == (0))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000)))) && !(k == (10000)))) && !(k == (1999))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000)))) && !(k == (1999)))) && j == (0) && !(k == (10000)))) && i == (1) && j == (1) && k == (3999)) || (c3 == (10000) && c1 == (4000) && c2 == (2000) && (!(j == (0)) || (j == (0) && !(i == (0))) || (j == (0) && i == (0) && !(k == (0))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000)))) && !(k == (10000))) || ((!(j == (0)) || (j == (0) && !(i == (0))) || (j == (0) && i == (0) && !(k == (0))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000)))) && !(k == (10000)))) && !(k == (1999))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000)))) && !(k == (1999)))) && j == (0) && !(k == (10000))) || ((!(j == (0)) || (j == (0) && !(i == (0))) || (j == (0) && i == (0) && !(k == (0))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000)))) && !(k == (10000))) || ((!(j == (0)) || (j == (0) && !(i == (0))) || (j == (0) && i == (0) && !(k == (0))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000))) || (j == (0) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000)))) && !(k == (10000)))) && !(k == (1999))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000)))) && !(k == (1999)))) && j == (0) && !(k == (10000)))) && !(k == (3999)))) && i == (1) && j == (1) && k == (9999)) || (c3 == (10000) && c1 == (4000) && c2 == (2000) && (!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000)) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000))) && !(k == (10000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000)) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000))) && !(k == (10000)))) && !(j == (1))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000)) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000))) && !(k == (10000)))) && j == (1) && !(k == (1999))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000)) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000))) && !(j == (1))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000))) && j == (1) && !(k == (1999)))) && !(k == (10000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000)) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000))) && !(k == (10000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000)) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000))) && !(k == (10000)))) && !(k == (1999))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000)) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000))) && !(k == (1999)))) && !(k == (10000)))) && j == (1) && !(k == (3999))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000)) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000))) && !(k == (10000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000)) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000))) && !(k == (10000)))) && !(k == (1999))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000)) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000))) && !(k == (1999)))) && !(k == (10000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000)) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000))) && !(k == (10000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000)) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000))) && !(k == (10000)))) && !(k == (1999))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000)) || ((!(i == (0)) || (i == (0) && !(k == (0))) || !(k == (2000))) && !(k == (1999)))) && !(k == (10000)))) && !(k == (3999)))) && j == (1) && !(k == (9999)))) && (!(i == (0)) || (i == (0) && !(k == (0)))) && i == (1) && j == (0) && k == (4000)) || (c3 == (10000) && c1 == (4000) && c2 == (2000) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && i == (1) && j == (0) && k == (2000)) (../plain/large_const.i:46:3)
[Warning][Witness] invariant unconfirmed: (c1 == (4000) && c2 == (2000) && c3 == (10000) && i == (0) && k == (0)) || (c3 == (10000) && c1 == (4000) && c2 == (2000) && (!(i == (0)) || (i == (0) && !(k == (0)))) && i == (1) && k == (4000)) || (c3 == (10000) && c1 == (4000) && c2 == (2000) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && i == (1) && k == (2000)) || (c3 == (10000) && c1 == (4000) && c2 == (2000) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000)))) && i == (1) && k == (10000)) (../plain/large_const.i:45:3)
[Warning][Witness] invariant unconfirmed: (c1 == (4000) && c2 == (2000) && c3 == (10000) && i == (1) && k == (10000)) || (c1 == (4000) && c2 == (2000) && c3 == (10000) && i == (1) && !(k == (10000)) && k == (4000)) || (c1 == (4000) && c2 == (2000) && c3 == (10000) && i == (1) && !(k == (10000)) && !(k == (4000)) && k == (2000)) || (c3 == (10000) && c1 == (4000) && c2 == (2000) && i == (0) && k == (0)) || (c3 == (10000) && c1 == (4000) && c2 == (2000) && (!(i == (0)) || (i == (0) && !(k == (0)))) && i == (1) && k == (4000)) || (c3 == (10000) && c1 == (4000) && c2 == (2000) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && i == (1) && k == (2000)) || (c3 == (10000) && c1 == (4000) && c2 == (2000) && (!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000))) || ((!(i == (0)) || (i == (0) && !(k == (0))) || ((!(i == (0)) || (i == (0) && !(k == (0)))) && !(k == (4000)))) && !(k == (2000)))) && i == (1) && k == (10000)) (../plain/large_const.i:34:3)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 3
  refuted: 0
  error: 2
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 5
SV-COMP result: unknown

vars = 62    evals = 109    narrow_reuses = 2

Timings:
                                  cputime   walltime   allocated   count
Default                            3.759s     3.760s    441.32MB      1×
  preprocess                         0.024s     0.022s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.17MB      4×
  Cabs2cil                           0.005s     0.005s      4.81MB      4×
  mergeCIL                           0.003s     0.003s      3.35MB      1×
  analysis                           3.718s     3.719s    423.99MB      1×
    createCFG                          0.001s     0.001s      0.66MB      1×
      handle                             0.001s     0.001s      0.11MB     34×
      iter_connect                       0.001s     0.001s      0.44MB     34×
        computeSCCs                        0.001s     0.001s      0.26MB     35×
    FrontC                             0.011s     0.011s      5.76MB      6×
    Cabs2cil                           0.004s     0.004s      4.50MB      6×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            1.357s     1.357s    343.23MB      1×
      S.Dom.equal                        0.001s     0.001s      0.04MB    111×
      base unassume                      0.226s     0.227s    240.81MB     26×
      cheap_full_reach                   0.001s     0.001s      0.03MB      1×
      postsolver                         0.023s     0.023s     17.31MB      1×
        postsolver_iter                    0.023s     0.023s     17.26MB      1×
    warn_global                        0.001s     0.001s      0.20MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
