/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/eureka_05.yml.witness.yml --witness.yaml.validate cpachecker/eureka_05.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/eureka_05.i


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


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Error][Witness] CIL couldn't parse invariant: (i == (5) && lh == (4) && rh == (4)) || (i == (5) && (!(lh == (4)) || (lh == (4) && !(rh == (4)))) && lh == (2) && rh == (2)) || (i == (5) && (!(lh == (4)) || (lh == (4) && !(rh == (4)))) && (!(lh == (2)) || (lh == (2) && !(rh == (2)))) && lh == (0) && rh == (3)) || (i == (5) && (!(lh == (4)) || (lh == (4) && !(rh == (4)))) && !(lh == (2)) && (!(lh == (0)) || (lh == (0) && !(rh == (3)))) && lh == (1) && rh == (2)) || (i == (5) && (!(lh == (4)) || (lh == (4) && !(rh == (4)))) && !(lh == (2)) && !(rh == (3)) && !(lh == (1)) && lh == (0) && rh == (2)) || (i == (5) && !(lh == (4)) && !(rh == (3)) && !(rh == (2)) && lh == (0) && rh == (4)) || (i == (5) && !(rh == (3)) && !(rh == (2)) && !(rh == (4)) && lh == (0) && rh == (0)) || (i == (5) && (!(lh == (4)) || (lh == (4) && !(rh == (4)))) && (!(lh == (2)) || (lh == (2) && !(rh == (2)))) && !(lh == (0)) && (!(lh == (1)) || (lh == (1) && !(rh == (2)))) && lh == (3) && rh == (3)) || (i == (5) && !(lh == (4)) && !(rh == (2)) && !(lh == (0)) && (!(lh == (3)) || (lh == (3) && !(rh == (3)))) && lh == (2) && rh == (4)) || (i == (5) && !(rh == (2)) && !(lh == (0)) && !(lh == (3)) && !(rh == (4)) && lh == (2) && rh == (3)) || (i == (5) && !(lh == (4)) && (!(lh == (1)) || (lh == (1) && !(rh == (2)))) && !(lh == (0)) && !(rh == (3)) && !(lh == (2)) && lh == (3) && rh == (4)) || (i == (5) && !(rh == (3)) && !(rh == (2)) && !(rh == (4)) && !(rh == (0)) && lh == (0) && rh == (1)) || (i == (5) && !(lh == (4)) && !(rh == (2)) && !(lh == (0)) && !(lh == (2)) && !(lh == (3)) && lh == (1) && rh == (4)) || (i == (5) && !(rh == (2)) && (!(lh == (3)) || (lh == (3) && !(rh == (3)))) && (!(lh == (2)) || (lh == (2) && !(rh == (3)))) && !(lh == (0)) && !(rh == (4)) && lh == (1) && rh == (1)) || (i == (5) && !(lh == (0)) && !(rh == (2)) && !(lh == (3)) && !(lh == (2)) && !(rh == (4)) && !(rh == (1)) && lh == (1) && rh == (3)) (../plain/eureka_05.i:34:7)
[Info][Witness] invariant has undefined variables or side effects: (i == (5) && lh == (4) && rh == (4)) || (i == (5) && (!(lh == (4)) || (lh == (4) && !(rh == (4)))) && lh == (2) && rh == (2)) || (i == (5) && (!(lh == (4)) || (lh == (4) && !(rh == (4)))) && (!(lh == (2)) || (lh == (2) && !(rh == (2)))) && lh == (0) && rh == (3)) || (i == (5) && (!(lh == (4)) || (lh == (4) && !(rh == (4)))) && !(lh == (2)) && (!(lh == (0)) || (lh == (0) && !(rh == (3)))) && lh == (1) && rh == (2)) || (i == (5) && (!(lh == (4)) || (lh == (4) && !(rh == (4)))) && !(lh == (2)) && !(rh == (3)) && !(lh == (1)) && lh == (0) && rh == (2)) || (i == (5) && !(lh == (4)) && !(rh == (3)) && !(rh == (2)) && lh == (0) && rh == (4)) || (i == (5) && !(rh == (3)) && !(rh == (2)) && !(rh == (4)) && lh == (0) && rh == (0)) || (i == (5) && (!(lh == (4)) || (lh == (4) && !(rh == (4)))) && (!(lh == (2)) || (lh == (2) && !(rh == (2)))) && !(lh == (0)) && (!(lh == (1)) || (lh == (1) && !(rh == (2)))) && lh == (3) && rh == (3)) || (i == (5) && !(lh == (4)) && !(rh == (2)) && !(lh == (0)) && (!(lh == (3)) || (lh == (3) && !(rh == (3)))) && lh == (2) && rh == (4)) || (i == (5) && !(rh == (2)) && !(lh == (0)) && !(lh == (3)) && !(rh == (4)) && lh == (2) && rh == (3)) || (i == (5) && !(lh == (4)) && (!(lh == (1)) || (lh == (1) && !(rh == (2)))) && !(lh == (0)) && !(rh == (3)) && !(lh == (2)) && lh == (3) && rh == (4)) || (i == (5) && !(rh == (3)) && !(rh == (2)) && !(rh == (4)) && !(rh == (0)) && lh == (0) && rh == (1)) || (i == (5) && !(lh == (4)) && !(rh == (2)) && !(lh == (0)) && !(lh == (2)) && !(lh == (3)) && lh == (1) && rh == (4)) || (i == (5) && !(rh == (2)) && (!(lh == (3)) || (lh == (3) && !(rh == (3)))) && (!(lh == (2)) || (lh == (2) && !(rh == (3)))) && !(lh == (0)) && !(rh == (4)) && lh == (1) && rh == (1)) || (i == (5) && !(lh == (0)) && !(rh == (2)) && !(lh == (3)) && !(lh == (2)) && !(rh == (4)) && !(rh == (1)) && lh == (1) && rh == (3)) (../plain/eureka_05.i:34:7)
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
[Warning][Witness] couldn't locate invariant: i == (4) || (!(i == (4)) && i == (0)) || (!(i == (0)) && !(i == (4)) && i == (3)) || (!(i == (0)) && !(i == (4)) && !(i == (3)) && i == (1)) || (!(i == (0)) && !(i == (4)) && !(i == (3)) && !(i == (1)) && i == (2)) (../plain/eureka_05.i:50:3)
[Info][Witness] unassume invariant: ((((((((((((((((((((lh == 0 && rh == 0) || ((! (lh == 0) || (lh == 0 && ! (rh == 0))) && rh == 2)) || (((! (lh == 0) || (lh == 0 && ! (rh == 0))) && ! (rh == 2)) && lh == 1)) || (((((! (lh == 0) || (lh == 0 && ! (rh == 0))) && ! (rh == 2)) && ! (lh == 1)) && lh == 3) && rh == 3)) || ((((((! (lh == 0) || (lh == 0 && ! (rh == 0))) && ! (rh == 2)) && ! (lh == 1)) && (! (lh == 3) || (lh == 3 && ! (rh == 3)))) && lh == 4) && rh == 4)) && i == 5) && lh == 2) && rh == 1) || (((((((((lh == 0 && rh == 0) || (((! (lh == 0) || (lh == 0 && ! (rh == 0))) && lh == 2) && rh == 2)) || ((((! (lh == 0) || (lh == 0 && ! (rh == 0))) && (! (lh == 2) || (lh == 2 && ! (rh == 2)))) && lh == 1) && rh == 1)) || ((((! (lh == 0) || (lh == 0 && ! (rh == 0))) && (! (lh == 2) || (lh == 2 && ! (rh == 2)))) && (! (lh == 1) || (lh == 1 && ! (rh == 1)))) && lh == 3)) || (((((! (lh == 0) || (lh == 0 && ! (rh == 0))) && (! (lh == 2) || (lh == 2 && ! (rh == 2)))) && (! (lh == 1) || (lh == 1 && ! (rh == 1)))) && ! (lh == 3)) && rh == 4)) && (! (lh == 2) || (lh == 2 && ! (rh == 1)))) && i == 5) && lh == 4) && rh == 3)) || ((((((((lh == 0 && rh == 0) || ! (lh == 0)) || (lh == 0 && ! (rh == 0))) && ! (lh == 2)) && (! (lh == 4) || (lh == 4 && ! (rh == 3)))) && i == 5) && lh == 1) && rh == 1)) || (((((((((lh == 0 && rh == 0) || ((! (lh == 0) || (lh == 0 && ! (rh == 0))) && rh == 2)) || ((((! (lh == 0) || (lh == 0 && ! (rh == 0))) && ! (rh == 2)) && lh == 3) && rh == 3)) || ((((! (lh == 0) || (lh == 0 && ! (rh == 0))) && ! (rh == 2)) && (! (lh == 3) || (lh == 3 && ! (rh == 3)))) && lh == 4)) && ! (rh == 1)) && (! (lh == 4) || (lh == 4 && ! (rh == 3)))) && i == 5) && lh == 2) && rh == 4)) || (((((((((((lh == 0 && rh == 0) || (((! (lh == 0) || (lh == 0 && ! (rh == 0))) && lh == 2) && rh == 2)) || ((((! (lh == 0) || (lh == 0 && ! (rh == 0))) && (! (lh == 2) || (lh == 2 && ! (rh == 2)))) && lh == 1) && rh == 1)) || ((! (lh == 0) || (lh == 0 && ! (rh == 0))) && (! (lh == 2) || (lh == 2 && ! (rh == 2))))) && (! (lh == 2) || (lh == 2 && ! (rh == 1)))) && ! (lh == 4)) && (! (lh == 1) || (lh == 1 && ! (rh == 1)))) && (! (lh == 2) || (lh == 2 && ! (rh == 4)))) && i == 5) && lh == 3) && rh == 3)) || ((((((((((lh == 0 && rh == 0) || ! (lh == 0)) || (lh == 0 && ! (rh == 0))) && ! (rh == 1)) && (! (lh == 4) || (lh == 4 && ! (rh == 3)))) && ! (rh == 4)) && (! (lh == 3) || (lh == 3 && ! (rh == 3)))) && i == 5) && lh == 2) && rh == 2)) || (((((((((((lh == 0 || ((! (lh == 0) && lh == 2) && rh == 2)) || ((! (lh == 0) && lh == 3) && rh == 3)) || ((! (lh == 0) && lh == 4) && rh == 4)) && (! (lh == 4) || (lh == 4 && ! (rh == 3)))) && ! (rh == 1)) && (! (lh == 2) || (lh == 2 && ! (rh == 4)))) && (! (lh == 3) || (lh == 3 && ! (rh == 3)))) && (! (lh == 2) || (lh == 2 && ! (rh == 2)))) && i == 5) && lh == 1) && rh == 0)) || ((((((((((lh == 3 && rh == 3) || lh == 4) && (! (lh == 4) || (lh == 4 && ! (rh == 3)))) && ! (rh == 1)) && ! (lh == 2)) && (! (lh == 3) || (lh == 3 && ! (rh == 3)))) && ! (rh == 0)) && i == 5) && lh == 1) && rh == 4)) || ((((((((((lh == 0 && rh == 0) && ! (rh == 1)) && ! (lh == 4)) && ! (rh == 4)) && ! (lh == 3)) && ! (rh == 2)) && ! (lh == 1)) && i == 5) && lh == 2) && rh == 3)) || ((((((((lh == 0 && rh == 0) || ((! (lh == 0) || (lh == 0 && ! (rh == 0))) && lh == 4)) && ! (lh == 2)) && ! (rh == 3)) && ! (lh == 1)) && i == 5) && lh == 3) && rh == 4)) || ((((((((((lh == 0 && rh == 0) || (((! (lh == 0) || (lh == 0 && ! (rh == 0))) && lh == 1) && rh == 1)) && (! (lh == 1) || (lh == 1 && ! (rh == 1)))) && ! (rh == 3)) && ! (lh == 2)) && (! (lh == 1) || (lh == 1 && ! (rh == 0)))) && ! (rh == 4)) && i == 5) && lh == 3) && rh == 2)) || (((((((((((((((((rh == 0 || (((! (rh == 0) && i == 5) && lh == 2) && rh == 2)) || ((((! (rh == 0) && (! (lh == 2) || (lh == 2 && ! (rh == 2)))) && i == 5) && lh == 1) && rh == 1)) || (((((! (rh == 0) && (! (lh == 2) || (lh == 2 && ! (rh == 2)))) && (! (lh == 1) || (lh == 1 && ! (rh == 1)))) && i == 5) && lh == 3) && rh == 3)) || ((((((! (rh == 0) && (! (lh == 2) || (lh == 2 && ! (rh == 2)))) && (! (lh == 1) || (lh == 1 && ! (rh == 1)))) && (! (lh == 3) || (lh == 3 && ! (rh == 3)))) && i == 5) && lh == 4) && rh == 4)) && ((! (i == 5) || (i == 5 && ! (lh == 2))) || ((i == 5 && lh == 2) && ! (rh == 1)))) && ((! (i == 5) || (i == 5 && ! (lh == 4))) || ((i == 5 && lh == 4) && ! (rh == 3)))) && ((! (i == 5) || (i == 5 && ! (lh == 1))) || ((i == 5 && lh == 1) && ! (rh == 1)))) && ((! (i == 5) || (i == 5 && ! (lh == 2))) || ((i == 5 && lh == 2) && ! (rh == 4)))) && ((! (i == 5) || (i == 5 && ! (lh == 3))) || ((i == 5 && lh == 3) && ! (rh == 3)))) && ((! (i == 5) || (i == 5 && ! (lh == 2))) || ((i == 5 && lh == 2) && ! (rh == 2)))) && ((! (i == 5) || (i == 5 && ! (lh == 1))) || ((i == 5 && lh == 1) && ! (rh == 0)))) && ((! (i == 5) || (i == 5 && ! (lh == 1))) || ((i == 5 && lh == 1) && ! (rh == 4)))) && ((! (i == 5) || (i == 5 && ! (lh == 2))) || ((i == 5 && lh == 2) && ! (rh == 3)))) && ((! (i == 5) || (i == 5 && ! (lh == 1))) || ((i == 5 && lh == 1) && ! (rh == 3)))) && ((! (i == 5) || (i == 5 && ! (lh == 3))) || ((i == 5 && lh == 3) && ! (rh == 4)))) && ((! (i == 5) || (i == 5 && ! (lh == 3))) || ((i == 5 && lh == 3) && ! (rh == 2)))) && lh == 0)) || ((((((((lh == 4 && ! (rh == 3)) && ! (lh == 2)) && ! (lh == 1)) && ! (lh == 3)) && ! (lh == 0)) && i == 5) && lh == 5) && rh == 4)) || ((((((((! (lh == 0) && ! (rh == 3)) && ! (lh == 2)) && ! (lh == 1)) && ! (lh == 3)) && ! (lh == 5)) && i == 5) && lh == 4) && rh == 4) (../plain/eureka_05.i:32:11-32:34)
[Info][Witness] unassume invariant: ((((((((((((((((((((lh == 0 && rh == 0) || ((! (lh == 0) || (lh == 0 && ! (rh == 0))) && rh == 2)) || (((! (lh == 0) || (lh == 0 && ! (rh == 0))) && ! (rh == 2)) && lh == 1)) || (((((! (lh == 0) || (lh == 0 && ! (rh == 0))) && ! (rh == 2)) && ! (lh == 1)) && lh == 3) && rh == 3)) || ((((((! (lh == 0) || (lh == 0 && ! (rh == 0))) && ! (rh == 2)) && ! (lh == 1)) && (! (lh == 3) || (lh == 3 && ! (rh == 3)))) && lh == 4) && rh == 4)) && i == 5) && lh == 2) && rh == 1) || (((((((((lh == 0 && rh == 0) || (((! (lh == 0) || (lh == 0 && ! (rh == 0))) && lh == 2) && rh == 2)) || ((((! (lh == 0) || (lh == 0 && ! (rh == 0))) && (! (lh == 2) || (lh == 2 && ! (rh == 2)))) && lh == 1) && rh == 1)) || ((((! (lh == 0) || (lh == 0 && ! (rh == 0))) && (! (lh == 2) || (lh == 2 && ! (rh == 2)))) && (! (lh == 1) || (lh == 1 && ! (rh == 1)))) && lh == 3)) || (((((! (lh == 0) || (lh == 0 && ! (rh == 0))) && (! (lh == 2) || (lh == 2 && ! (rh == 2)))) && (! (lh == 1) || (lh == 1 && ! (rh == 1)))) && ! (lh == 3)) && rh == 4)) && (! (lh == 2) || (lh == 2 && ! (rh == 1)))) && i == 5) && lh == 4) && rh == 3)) || ((((((((lh == 0 && rh == 0) || ! (lh == 0)) || (lh == 0 && ! (rh == 0))) && ! (lh == 2)) && (! (lh == 4) || (lh == 4 && ! (rh == 3)))) && i == 5) && lh == 1) && rh == 1)) || (((((((((lh == 0 && rh == 0) || ((! (lh == 0) || (lh == 0 && ! (rh == 0))) && rh == 2)) || ((((! (lh == 0) || (lh == 0 && ! (rh == 0))) && ! (rh == 2)) && lh == 3) && rh == 3)) || ((((! (lh == 0) || (lh == 0 && ! (rh == 0))) && ! (rh == 2)) && (! (lh == 3) || (lh == 3 && ! (rh == 3)))) && lh == 4)) && ! (rh == 1)) && (! (lh == 4) || (lh == 4 && ! (rh == 3)))) && i == 5) && lh == 2) && rh == 4)) || (((((((((((lh == 0 && rh == 0) || (((! (lh == 0) || (lh == 0 && ! (rh == 0))) && lh == 2) && rh == 2)) || ((((! (lh == 0) || (lh == 0 && ! (rh == 0))) && (! (lh == 2) || (lh == 2 && ! (rh == 2)))) && lh == 1) && rh == 1)) || ((! (lh == 0) || (lh == 0 && ! (rh == 0))) && (! (lh == 2) || (lh == 2 && ! (rh == 2))))) && (! (lh == 2) || (lh == 2 && ! (rh == 1)))) && ! (lh == 4)) && (! (lh == 1) || (lh == 1 && ! (rh == 1)))) && (! (lh == 2) || (lh == 2 && ! (rh == 4)))) && i == 5) && lh == 3) && rh == 3)) || ((((((((((lh == 0 && rh == 0) || ! (lh == 0)) || (lh == 0 && ! (rh == 0))) && ! (rh == 1)) && (! (lh == 4) || (lh == 4 && ! (rh == 3)))) && ! (rh == 4)) && (! (lh == 3) || (lh == 3 && ! (rh == 3)))) && i == 5) && lh == 2) && rh == 2)) || (((((((((((lh == 0 || ((! (lh == 0) && lh == 2) && rh == 2)) || ((! (lh == 0) && lh == 3) && rh == 3)) || ((! (lh == 0) && lh == 4) && rh == 4)) && (! (lh == 4) || (lh == 4 && ! (rh == 3)))) && ! (rh == 1)) && (! (lh == 2) || (lh == 2 && ! (rh == 4)))) && (! (lh == 3) || (lh == 3 && ! (rh == 3)))) && (! (lh == 2) || (lh == 2 && ! (rh == 2)))) && i == 5) && lh == 1) && rh == 0)) || ((((((((((lh == 3 && rh == 3) || lh == 4) && (! (lh == 4) || (lh == 4 && ! (rh == 3)))) && ! (rh == 1)) && ! (lh == 2)) && (! (lh == 3) || (lh == 3 && ! (rh == 3)))) && ! (rh == 0)) && i == 5) && lh == 1) && rh == 4)) || ((((((((((lh == 0 && rh == 0) && ! (rh == 1)) && ! (lh == 4)) && ! (rh == 4)) && ! (lh == 3)) && ! (rh == 2)) && ! (lh == 1)) && i == 5) && lh == 2) && rh == 3)) || ((((((((lh == 0 && rh == 0) || ((! (lh == 0) || (lh == 0 && ! (rh == 0))) && lh == 4)) && ! (lh == 2)) && ! (rh == 3)) && ! (lh == 1)) && i == 5) && lh == 3) && rh == 4)) || ((((((((((lh == 0 && rh == 0) || (((! (lh == 0) || (lh == 0 && ! (rh == 0))) && lh == 1) && rh == 1)) && (! (lh == 1) || (lh == 1 && ! (rh == 1)))) && ! (rh == 3)) && ! (lh == 2)) && (! (lh == 1) || (lh == 1 && ! (rh == 0)))) && ! (rh == 4)) && i == 5) && lh == 3) && rh == 2)) || (((((((((((((((((rh == 0 || (((! (rh == 0) && i == 5) && lh == 2) && rh == 2)) || ((((! (rh == 0) && (! (lh == 2) || (lh == 2 && ! (rh == 2)))) && i == 5) && lh == 1) && rh == 1)) || (((((! (rh == 0) && (! (lh == 2) || (lh == 2 && ! (rh == 2)))) && (! (lh == 1) || (lh == 1 && ! (rh == 1)))) && i == 5) && lh == 3) && rh == 3)) || ((((((! (rh == 0) && (! (lh == 2) || (lh == 2 && ! (rh == 2)))) && (! (lh == 1) || (lh == 1 && ! (rh == 1)))) && (! (lh == 3) || (lh == 3 && ! (rh == 3)))) && i == 5) && lh == 4) && rh == 4)) && ((! (i == 5) || (i == 5 && ! (lh == 2))) || ((i == 5 && lh == 2) && ! (rh == 1)))) && ((! (i == 5) || (i == 5 && ! (lh == 4))) || ((i == 5 && lh == 4) && ! (rh == 3)))) && ((! (i == 5) || (i == 5 && ! (lh == 1))) || ((i == 5 && lh == 1) && ! (rh == 1)))) && ((! (i == 5) || (i == 5 && ! (lh == 2))) || ((i == 5 && lh == 2) && ! (rh == 4)))) && ((! (i == 5) || (i == 5 && ! (lh == 3))) || ((i == 5 && lh == 3) && ! (rh == 3)))) && ((! (i == 5) || (i == 5 && ! (lh == 2))) || ((i == 5 && lh == 2) && ! (rh == 2)))) && ((! (i == 5) || (i == 5 && ! (lh == 1))) || ((i == 5 && lh == 1) && ! (rh == 0)))) && ((! (i == 5) || (i == 5 && ! (lh == 1))) || ((i == 5 && lh == 1) && ! (rh == 4)))) && ((! (i == 5) || (i == 5 && ! (lh == 2))) || ((i == 5 && lh == 2) && ! (rh == 3)))) && ((! (i == 5) || (i == 5 && ! (lh == 1))) || ((i == 5 && lh == 1) && ! (rh == 3)))) && ((! (i == 5) || (i == 5 && ! (lh == 3))) || ((i == 5 && lh == 3) && ! (rh == 4)))) && ((! (i == 5) || (i == 5 && ! (lh == 3))) || ((i == 5 && lh == 3) && ! (rh == 2)))) && lh == 0)) || ((((((((lh == 4 && ! (rh == 3)) && ! (lh == 2)) && ! (lh == 1)) && ! (lh == 3)) && ! (lh == 0)) && i == 5) && lh == 5) && rh == 4)) || ((((((((! (lh == 0) && ! (rh == 3)) && ! (lh == 2)) && ! (lh == 1)) && ! (lh == 3)) && ! (lh == 5)) && i == 5) && lh == 4) && rh == 4) (../plain/eureka_05.i:32:11-32:34)
[Info][Witness] unassume invariant: i == -1 && (((((i == 4 || (! (i == 4) && i == 0)) || ((! (i == 0) && ! (i == 4)) && i == 3)) || (((! (i == 0) && ! (i == 4)) && ! (i == 3)) && i == 1)) || ((((! (i == 0) && ! (i == 4)) && ! (i == 3)) && ! (i == 1)) && i == 2)) && (((((i == 0 || (! (i == 0) && i == 4)) || ((! (i == 0) && ! (i == 4)) && i == 3)) || (((! (i == 0) && ! (i == 4)) && ! (i == 3)) && i == 1)) || ((((! (i == 0) && ! (i == 4)) && ! (i == 3)) && ! (i == 1)) && i == 2)) || (((((! (i == 0) && ! (i == 4)) && ! (i == 3)) && ! (i == 1)) && ! (i == 2)) && i == -1))) (../plain/eureka_05.i:49:5-49:19)
[Info][Witness] unassume invariant: i == -1 && (((((i == 4 || (! (i == 4) && i == 0)) || ((! (i == 0) && ! (i == 4)) && i == 3)) || (((! (i == 0) && ! (i == 4)) && ! (i == 3)) && i == 1)) || ((((! (i == 0) && ! (i == 4)) && ! (i == 3)) && ! (i == 1)) && i == 2)) && (((((i == 0 || (! (i == 0) && i == 4)) || ((! (i == 0) && ! (i == 4)) && i == 3)) || (((! (i == 0) && ! (i == 4)) && ! (i == 3)) && i == 1)) || ((((! (i == 0) && ! (i == 4)) && ! (i == 3)) && ! (i == 1)) && i == 2)) || (((((! (i == 0) && ! (i == 4)) && ! (i == 3)) && ! (i == 1)) && ! (i == 2)) && i == -1))) (../plain/eureka_05.i:49:5-49:19)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 21
  dead: 0
  total lines: 21
[Warning][Deadcode][CWE-570] condition 'array[i] < array[rh]' is always false (../plain/eureka_05.i:33:14-33:34)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (../plain/eureka_05.i:12:73-12:74)
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
../plain/eureka_05.i:34: Error: Cannot resolve variable lh.
../plain/eureka_05.i:34: Error: Cannot resolve variable rh.
[Warning][Witness] invariant unconfirmed: (i == (4) || (!(i == (4)) && i == (0)) || (!(i == (0)) && !(i == (4)) && i == (3)) || (!(i == (0)) && !(i == (4)) && !(i == (3)) && i == (1)) || (!(i == (0)) && !(i == (4)) && !(i == (3)) && !(i == (1)) && i == (2))) && (i == (0) || (!(i == (0)) && i == (4)) || (!(i == (0)) && !(i == (4)) && i == (3)) || (!(i == (0)) && !(i == (4)) && !(i == (3)) && i == (1)) || (!(i == (0)) && !(i == (4)) && !(i == (3)) && !(i == (1)) && i == (2)) || (!(i == (0)) && !(i == (4)) && !(i == (3)) && !(i == (1)) && !(i == (2)) && i == (-1))) (../plain/eureka_05.i:45:3)
[Warning][Witness] invariant unconfirmed: (((lh == (0) && rh == (0)) || ((!(lh == (0)) || (lh == (0) && !(rh == (0)))) && rh == (2)) || ((!(lh == (0)) || (lh == (0) && !(rh == (0)))) && !(rh == (2)) && lh == (1)) || ((!(lh == (0)) || (lh == (0) && !(rh == (0)))) && !(rh == (2)) && !(lh == (1)) && lh == (3) && rh == (3)) || ((!(lh == (0)) || (lh == (0) && !(rh == (0)))) && !(rh == (2)) && !(lh == (1)) && (!(lh == (3)) || (lh == (3) && !(rh == (3)))) && lh == (4) && rh == (4))) && i == (5) && lh == (2) && rh == (1)) || (((lh == (0) && rh == (0)) || ((!(lh == (0)) || (lh == (0) && !(rh == (0)))) && lh == (2) && rh == (2)) || ((!(lh == (0)) || (lh == (0) && !(rh == (0)))) && (!(lh == (2)) || (lh == (2) && !(rh == (2)))) && lh == (1) && rh == (1)) || ((!(lh == (0)) || (lh == (0) && !(rh == (0)))) && (!(lh == (2)) || (lh == (2) && !(rh == (2)))) && (!(lh == (1)) || (lh == (1) && !(rh == (1)))) && lh == (3)) || ((!(lh == (0)) || (lh == (0) && !(rh == (0)))) && (!(lh == (2)) || (lh == (2) && !(rh == (2)))) && (!(lh == (1)) || (lh == (1) && !(rh == (1)))) && !(lh == (3)) && rh == (4))) && (!(lh == (2)) || (lh == (2) && !(rh == (1)))) && i == (5) && lh == (4) && rh == (3)) || (((lh == (0) && rh == (0)) || !(lh == (0)) || (lh == (0) && !(rh == (0)))) && !(lh == (2)) && (!(lh == (4)) || (lh == (4) && !(rh == (3)))) && i == (5) && lh == (1) && rh == (1)) || (((lh == (0) && rh == (0)) || ((!(lh == (0)) || (lh == (0) && !(rh == (0)))) && rh == (2)) || ((!(lh == (0)) || (lh == (0) && !(rh == (0)))) && !(rh == (2)) && lh == (3) && rh == (3)) || ((!(lh == (0)) || (lh == (0) && !(rh == (0)))) && !(rh == (2)) && (!(lh == (3)) || (lh == (3) && !(rh == (3)))) && lh == (4))) && !(rh == (1)) && (!(lh == (4)) || (lh == (4) && !(rh == (3)))) && i == (5) && lh == (2) && rh == (4)) || (((lh == (0) && rh == (0)) || ((!(lh == (0)) || (lh == (0) && !(rh == (0)))) && lh == (2) && rh == (2)) || ((!(lh == (0)) || (lh == (0) && !(rh == (0)))) && (!(lh == (2)) || (lh == (2) && !(rh == (2)))) && lh == (1) && rh == (1)) || ((!(lh == (0)) || (lh == (0) && !(rh == (0)))) && (!(lh == (2)) || (lh == (2) && !(rh == (2)))))) && (!(lh == (2)) || (lh == (2) && !(rh == (1)))) && !(lh == (4)) && (!(lh == (1)) || (lh == (1) && !(rh == (1)))) && (!(lh == (2)) || (lh == (2) && !(rh == (4)))) && i == (5) && lh == (3) && rh == (3)) || (((lh == (0) && rh == (0)) || !(lh == (0)) || (lh == (0) && !(rh == (0)))) && !(rh == (1)) && (!(lh == (4)) || (lh == (4) && !(rh == (3)))) && !(rh == (4)) && (!(lh == (3)) || (lh == (3) && !(rh == (3)))) && i == (5) && lh == (2) && rh == (2)) || ((lh == (0) || (!(lh == (0)) && lh == (2) && rh == (2)) || (!(lh == (0)) && lh == (3) && rh == (3)) || (!(lh == (0)) && lh == (4) && rh == (4))) && (!(lh == (4)) || (lh == (4) && !(rh == (3)))) && !(rh == (1)) && (!(lh == (2)) || (lh == (2) && !(rh == (4)))) && (!(lh == (3)) || (lh == (3) && !(rh == (3)))) && (!(lh == (2)) || (lh == (2) && !(rh == (2)))) && i == (5) && lh == (1) && rh == (0)) || (((lh == (3) && rh == (3)) || lh == (4)) && (!(lh == (4)) || (lh == (4) && !(rh == (3)))) && !(rh == (1)) && !(lh == (2)) && (!(lh == (3)) || (lh == (3) && !(rh == (3)))) && !(rh == (0)) && i == (5) && lh == (1) && rh == (4)) || (lh == (0) && rh == (0) && !(rh == (1)) && !(lh == (4)) && !(rh == (4)) && !(lh == (3)) && !(rh == (2)) && !(lh == (1)) && i == (5) && lh == (2) && rh == (3)) || (((lh == (0) && rh == (0)) || ((!(lh == (0)) || (lh == (0) && !(rh == (0)))) && lh == (4))) && !(lh == (2)) && !(rh == (3)) && !(lh == (1)) && i == (5) && lh == (3) && rh == (4)) || (((lh == (0) && rh == (0)) || ((!(lh == (0)) || (lh == (0) && !(rh == (0)))) && lh == (1) && rh == (1))) && (!(lh == (1)) || (lh == (1) && !(rh == (1)))) && !(rh == (3)) && !(lh == (2)) && (!(lh == (1)) || (lh == (1) && !(rh == (0)))) && !(rh == (4)) && i == (5) && lh == (3) && rh == (2)) || ((rh == (0) || (!(rh == (0)) && i == (5) && lh == (2) && rh == (2)) || (!(rh == (0)) && (!(lh == (2)) || (lh == (2) && !(rh == (2)))) && i == (5) && lh == (1) && rh == (1)) || (!(rh == (0)) && (!(lh == (2)) || (lh == (2) && !(rh == (2)))) && (!(lh == (1)) || (lh == (1) && !(rh == (1)))) && i == (5) && lh == (3) && rh == (3)) || (!(rh == (0)) && (!(lh == (2)) || (lh == (2) && !(rh == (2)))) && (!(lh == (1)) || (lh == (1) && !(rh == (1)))) && (!(lh == (3)) || (lh == (3) && !(rh == (3)))) && i == (5) && lh == (4) && rh == (4))) && (!(i == (5)) || (i == (5) && !(lh == (2))) || (i == (5) && lh == (2) && !(rh == (1)))) && (!(i == (5)) || (i == (5) && !(lh == (4))) || (i == (5) && lh == (4) && !(rh == (3)))) && (!(i == (5)) || (i == (5) && !(lh == (1))) || (i == (5) && lh == (1) && !(rh == (1)))) && (!(i == (5)) || (i == (5) && !(lh == (2))) || (i == (5) && lh == (2) && !(rh == (4)))) && (!(i == (5)) || (i == (5) && !(lh == (3))) || (i == (5) && lh == (3) && !(rh == (3)))) && (!(i == (5)) || (i == (5) && !(lh == (2))) || (i == (5) && lh == (2) && !(rh == (2)))) && (!(i == (5)) || (i == (5) && !(lh == (1))) || (i == (5) && lh == (1) && !(rh == (0)))) && (!(i == (5)) || (i == (5) && !(lh == (1))) || (i == (5) && lh == (1) && !(rh == (4)))) && (!(i == (5)) || (i == (5) && !(lh == (2))) || (i == (5) && lh == (2) && !(rh == (3)))) && (!(i == (5)) || (i == (5) && !(lh == (1))) || (i == (5) && lh == (1) && !(rh == (3)))) && (!(i == (5)) || (i == (5) && !(lh == (3))) || (i == (5) && lh == (3) && !(rh == (4)))) && (!(i == (5)) || (i == (5) && !(lh == (3))) || (i == (5) && lh == (3) && !(rh == (2)))) && lh == (0)) || (lh == (4) && !(rh == (3)) && !(lh == (2)) && !(lh == (1)) && !(lh == (3)) && !(lh == (0)) && i == (5) && lh == (5) && rh == (4)) || (!(lh == (0)) && !(rh == (3)) && !(lh == (2)) && !(lh == (1)) && !(lh == (3)) && !(lh == (5)) && i == (5) && lh == (4) && rh == (4)) (../plain/eureka_05.i:31:7)
[Error][Witness] invariant refuted: i == (-1) (../plain/eureka_05.i:47:2)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 2
  refuted: 1
  error: 2
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 5
SV-COMP result: false

vars = 49    evals = 178    narrow_reuses = 9

Timings:
                                  cputime   walltime   allocated   count
Default                            2.669s     2.681s    546.62MB      1×
  preprocess                         0.025s     0.024s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.15MB      4×
  Cabs2cil                           0.006s     0.006s      4.78MB      4×
  mergeCIL                           0.004s     0.004s      3.35MB      1×
  analysis                           2.625s     2.636s    529.35MB      1×
    createCFG                          0.001s     0.001s      0.63MB      1×
      handle                             0.001s     0.001s      0.10MB     34×
      iter_connect                       0.001s     0.001s      0.42MB     34×
        computeSCCs                        0.001s     0.001s      0.24MB     35×
    FrontC                             0.007s     0.007s      3.88MB      8×
    Cabs2cil                           0.009s     0.009s      4.90MB      8×
    global_inits                       0.001s     0.001s      0.29MB      1×
    solving                            1.370s     1.373s    465.82MB      1×
      S.Dom.equal                        0.001s     0.001s      0.07MB    187×
      base unassume                      0.376s     0.377s    356.46MB     40×
      cheap_full_reach                   0.001s     0.001s      0.02MB      1×
      postsolver                         0.018s     0.018s     11.18MB      1×
        postsolver_iter                    0.018s     0.018s     11.14MB      1×
    warn_global                        0.001s     0.001s      0.18MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
