/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 pesco/benchmark52_polynomial.yml.witness.yml --witness.yaml.validate pesco/benchmark52_polynomial.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/benchmark52_polynomial.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: (i >= (-1) && i <= (17)) || ((!(i >= (-1)) || (i >= (-1) && !(i <= (17)))) && i >= (4) && i <= (22)) || ((!(i >= (-1)) || (i >= (-1) && !(i <= (17)))) && (!(i >= (4)) || (i >= (4) && !(i <= (22)))) && i >= (-8) && i <= (10)) || ((!(i >= (-1)) || (i >= (-1) && !(i <= (17)))) && (!(i >= (4)) || (i >= (4) && !(i <= (22)))) && (!(i >= (-8)) || (i >= (-8) && !(i <= (10)))) && i >= (-7) && i <= (11)) || ((!(i >= (-1)) || (i >= (-1) && !(i <= (17)))) && (!(i >= (4)) || (i >= (4) && !(i <= (22)))) && (!(i >= (-8)) || (i >= (-8) && !(i <= (10)))) && (!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && i >= (-3) && i <= (15)) || ((!(i >= (-1)) || (i >= (-1) && !(i <= (17)))) && (!(i >= (4)) || (i >= (4) && !(i <= (22)))) && (!(i >= (-8)) || (i >= (-8) && !(i <= (10)))) && (!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && i >= (-6) && i <= (12)) || ((!(i >= (-1)) || (i >= (-1) && !(i <= (17)))) && (!(i >= (4)) || (i >= (4) && !(i <= (22)))) && (!(i >= (-8)) || (i >= (-8) && !(i <= (10)))) && (!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && i >= (-2) && i <= (16)) || ((!(i >= (-1)) || (i >= (-1) && !(i <= (17)))) && (!(i >= (4)) || (i >= (4) && !(i <= (22)))) && (!(i >= (-8)) || (i >= (-8) && !(i <= (10)))) && (!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && i >= (-5) && i <= (13)) || ((!(i >= (-1)) || (i >= (-1) && !(i <= (17)))) && (!(i >= (4)) || (i >= (4) && !(i <= (22)))) && (!(i >= (-8)) || (i >= (-8) && !(i <= (10)))) && (!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && (!(i >= (-5)) || (i >= (-5) && !(i <= (13)))) && i >= (-4) && i <= (14)) || ((!(i >= (-1)) || (i >= (-1) && !(i <= (17)))) && (!(i >= (4)) || (i >= (4) && !(i <= (22)))) && (!(i >= (-8)) || (i >= (-8) && !(i <= (10)))) && (!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && (!(i >= (-5)) || (i >= (-5) && !(i <= (13)))) && (!(i >= (-4)) || (i >= (-4) && !(i <= (14)))) && i >= (5) && i <= (23)) (../plain/benchmark52_polynomial.i:25:3)
[Warning][Witness] couldn't locate invariant: (i >= (3) && i <= (21)) || ((!(i >= (3)) || (i >= (3) && !(i <= (21)))) && i >= (-6) && i <= (12)) || ((!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && i >= (-5) && i <= (13)) || ((!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (-5)) || (i >= (-5) && !(i <= (13)))) && i >= (-2) && i <= (16)) || ((!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (-5)) || (i >= (-5) && !(i <= (13)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && i >= (0) && i <= (18)) || ((!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (-5)) || (i >= (-5) && !(i <= (13)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && (!(i >= (0)) || (i >= (0) && !(i <= (18)))) && i >= (-3) && i <= (15)) || ((!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (-5)) || (i >= (-5) && !(i <= (13)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && (!(i >= (0)) || (i >= (0) && !(i <= (18)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && i >= (-7) && i <= (11)) || ((!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (-5)) || (i >= (-5) && !(i <= (13)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && (!(i >= (0)) || (i >= (0) && !(i <= (18)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && i >= (1) && i <= (19)) || ((!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (-5)) || (i >= (-5) && !(i <= (13)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && (!(i >= (0)) || (i >= (0) && !(i <= (18)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (1)) || (i >= (1) && !(i <= (19)))) && i >= (-9) && i <= (9)) || ((!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (-5)) || (i >= (-5) && !(i <= (13)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && (!(i >= (0)) || (i >= (0) && !(i <= (18)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (1)) || (i >= (1) && !(i <= (19)))) && (!(i >= (-9)) || (i >= (-9) && !(i <= (9)))) && i >= (-8) && i <= (10)) || ((!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (-5)) || (i >= (-5) && !(i <= (13)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && (!(i >= (0)) || (i >= (0) && !(i <= (18)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (1)) || (i >= (1) && !(i <= (19)))) && (!(i >= (-9)) || (i >= (-9) && !(i <= (9)))) && (!(i >= (-8)) || (i >= (-8) && !(i <= (10)))) && i >= (4) && i <= (22)) || ((!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (-5)) || (i >= (-5) && !(i <= (13)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && (!(i >= (0)) || (i >= (0) && !(i <= (18)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (1)) || (i >= (1) && !(i <= (19)))) && (!(i >= (-9)) || (i >= (-9) && !(i <= (9)))) && (!(i >= (-8)) || (i >= (-8) && !(i <= (10)))) && (!(i >= (4)) || (i >= (4) && !(i <= (22)))) && i >= (2) && i <= (20)) || ((!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (0)) || (i >= (0) && !(i <= (18)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && (!(i >= (2)) || (i >= (2) && !(i <= (20)))) && (!(i >= (-8)) || (i >= (-8) && !(i <= (10)))) && (!(i >= (-5)) || (i >= (-5) && !(i <= (13)))) && (!(i >= (4)) || (i >= (4) && !(i <= (22)))) && (!(i >= (-9)) || (i >= (-9) && !(i <= (9)))) && (!(i >= (1)) || (i >= (1) && !(i <= (19)))) && i >= (-1) && i <= (17)) || ((!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (0)) || (i >= (0) && !(i <= (18)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && (!(i >= (2)) || (i >= (2) && !(i <= (20)))) && (!(i >= (-8)) || (i >= (-8) && !(i <= (10)))) && (!(i >= (-5)) || (i >= (-5) && !(i <= (13)))) && (!(i >= (4)) || (i >= (4) && !(i <= (22)))) && (!(i >= (-9)) || (i >= (-9) && !(i <= (9)))) && (!(i >= (1)) || (i >= (1) && !(i <= (19)))) && (!(i >= (-1)) || (i >= (-1) && !(i <= (17)))) && i >= (-4) && i <= (14)) (../plain/benchmark52_polynomial.i:23:5)
[Info][Witness] unassume invariant: ((((((((((((((i >= -7 && i <= 11) || (((! (i >= -7) || (i >= -7 && ! (i <= 11))) && i >= -3) && i <= 15)) || ((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && i >= 3) && i <= 21)) || (((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && i >= -6) && i <= 12)) || ((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && i >= 0) && i <= 18)) || (((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && i >= -2) && i <= 16)) || ((((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && (! (i >= -2) || (i >= -2 && ! (i <= 16)))) && i >= 2) && i <= 20)) || (((((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && (! (i >= -2) || (i >= -2 && ! (i <= 16)))) && (! (i >= 2) || (i >= 2 && ! (i <= 20)))) && i >= -8) && i <= 10)) || ((((((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && (! (i >= -2) || (i >= -2 && ! (i <= 16)))) && (! (i >= 2) || (i >= 2 && ! (i <= 20)))) && (! (i >= -8) || (i >= -8 && ! (i <= 10)))) && i >= -5) && i <= 13)) || (((((((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && (! (i >= -2) || (i >= -2 && ! (i <= 16)))) && (! (i >= 2) || (i >= 2 && ! (i <= 20)))) && (! (i >= -8) || (i >= -8 && ! (i <= 10)))) && (! (i >= -5) || (i >= -5 && ! (i <= 13)))) && i >= 4) && i <= 22)) || ((((((((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && (! (i >= -2) || (i >= -2 && ! (i <= 16)))) && (! (i >= 2) || (i >= 2 && ! (i <= 20)))) && (! (i >= -8) || (i >= -8 && ! (i <= 10)))) && (! (i >= -5) || (i >= -5 && ! (i <= 13)))) && (! (i >= 4) || (i >= 4 && ! (i <= 22)))) && i >= -9) && i <= 9)) || (((((((((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && (! (i >= -2) || (i >= -2 && ! (i <= 16)))) && (! (i >= 2) || (i >= 2 && ! (i <= 20)))) && (! (i >= -8) || (i >= -8 && ! (i <= 10)))) && (! (i >= -5) || (i >= -5 && ! (i <= 13)))) && (! (i >= 4) || (i >= 4 && ! (i <= 22)))) && (! (i >= -9) || (i >= -9 && ! (i <= 9)))) && i >= 1) && i <= 19)) || ((((((((((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && (! (i >= -2) || (i >= -2 && ! (i <= 16)))) && (! (i >= 2) || (i >= 2 && ! (i <= 20)))) && (! (i >= -8) || (i >= -8 && ! (i <= 10)))) && (! (i >= -5) || (i >= -5 && ! (i <= 13)))) && (! (i >= 4) || (i >= 4 && ! (i <= 22)))) && (! (i >= -9) || (i >= -9 && ! (i <= 9)))) && (! (i >= 1) || (i >= 1 && ! (i <= 19)))) && i >= -1) && i <= 17)) || (((((((((((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && (! (i >= -2) || (i >= -2 && ! (i <= 16)))) && (! (i >= 2) || (i >= 2 && ! (i <= 20)))) && (! (i >= -8) || (i >= -8 && ! (i <= 10)))) && (! (i >= -5) || (i >= -5 && ! (i <= 13)))) && (! (i >= 4) || (i >= 4 && ! (i <= 22)))) && (! (i >= -9) || (i >= -9 && ! (i <= 9)))) && (! (i >= 1) || (i >= 1 && ! (i <= 19)))) && (! (i >= -1) || (i >= -1 && ! (i <= 17)))) && i >= 5) && i <= 23)) || ((((((((((((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && (! (i >= -2) || (i >= -2 && ! (i <= 16)))) && (! (i >= 2) || (i >= 2 && ! (i <= 20)))) && (! (i >= -8) || (i >= -8 && ! (i <= 10)))) && (! (i >= -5) || (i >= -5 && ! (i <= 13)))) && (! (i >= 4) || (i >= 4 && ! (i <= 22)))) && (! (i >= -9) || (i >= -9 && ! (i <= 9)))) && (! (i >= 1) || (i >= 1 && ! (i <= 19)))) && (! (i >= -1) || (i >= -1 && ! (i <= 17)))) && (! (i >= 5) || (i >= 5 && ! (i <= 23)))) && i >= -4) && i <= 14) (../plain/benchmark52_polynomial.i:21:7-21:27)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (../plain/benchmark52_polynomial.i:22:10-22:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (../plain/benchmark52_polynomial.i:23:5-23:14)
[Info][Witness] unassume invariant: ((((((((((((((i >= -7 && i <= 11) || (((! (i >= -7) || (i >= -7 && ! (i <= 11))) && i >= -3) && i <= 15)) || ((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && i >= 3) && i <= 21)) || (((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && i >= -6) && i <= 12)) || ((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && i >= 0) && i <= 18)) || (((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && i >= -2) && i <= 16)) || ((((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && (! (i >= -2) || (i >= -2 && ! (i <= 16)))) && i >= 2) && i <= 20)) || (((((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && (! (i >= -2) || (i >= -2 && ! (i <= 16)))) && (! (i >= 2) || (i >= 2 && ! (i <= 20)))) && i >= -8) && i <= 10)) || ((((((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && (! (i >= -2) || (i >= -2 && ! (i <= 16)))) && (! (i >= 2) || (i >= 2 && ! (i <= 20)))) && (! (i >= -8) || (i >= -8 && ! (i <= 10)))) && i >= -5) && i <= 13)) || (((((((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && (! (i >= -2) || (i >= -2 && ! (i <= 16)))) && (! (i >= 2) || (i >= 2 && ! (i <= 20)))) && (! (i >= -8) || (i >= -8 && ! (i <= 10)))) && (! (i >= -5) || (i >= -5 && ! (i <= 13)))) && i >= 4) && i <= 22)) || ((((((((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && (! (i >= -2) || (i >= -2 && ! (i <= 16)))) && (! (i >= 2) || (i >= 2 && ! (i <= 20)))) && (! (i >= -8) || (i >= -8 && ! (i <= 10)))) && (! (i >= -5) || (i >= -5 && ! (i <= 13)))) && (! (i >= 4) || (i >= 4 && ! (i <= 22)))) && i >= -9) && i <= 9)) || (((((((((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && (! (i >= -2) || (i >= -2 && ! (i <= 16)))) && (! (i >= 2) || (i >= 2 && ! (i <= 20)))) && (! (i >= -8) || (i >= -8 && ! (i <= 10)))) && (! (i >= -5) || (i >= -5 && ! (i <= 13)))) && (! (i >= 4) || (i >= 4 && ! (i <= 22)))) && (! (i >= -9) || (i >= -9 && ! (i <= 9)))) && i >= 1) && i <= 19)) || ((((((((((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && (! (i >= -2) || (i >= -2 && ! (i <= 16)))) && (! (i >= 2) || (i >= 2 && ! (i <= 20)))) && (! (i >= -8) || (i >= -8 && ! (i <= 10)))) && (! (i >= -5) || (i >= -5 && ! (i <= 13)))) && (! (i >= 4) || (i >= 4 && ! (i <= 22)))) && (! (i >= -9) || (i >= -9 && ! (i <= 9)))) && (! (i >= 1) || (i >= 1 && ! (i <= 19)))) && i >= -1) && i <= 17)) || (((((((((((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && (! (i >= -2) || (i >= -2 && ! (i <= 16)))) && (! (i >= 2) || (i >= 2 && ! (i <= 20)))) && (! (i >= -8) || (i >= -8 && ! (i <= 10)))) && (! (i >= -5) || (i >= -5 && ! (i <= 13)))) && (! (i >= 4) || (i >= 4 && ! (i <= 22)))) && (! (i >= -9) || (i >= -9 && ! (i <= 9)))) && (! (i >= 1) || (i >= 1 && ! (i <= 19)))) && (! (i >= -1) || (i >= -1 && ! (i <= 17)))) && i >= 5) && i <= 23)) || ((((((((((((((((! (i >= -7) || (i >= -7 && ! (i <= 11))) && (! (i >= -3) || (i >= -3 && ! (i <= 15)))) && (! (i >= 3) || (i >= 3 && ! (i <= 21)))) && (! (i >= -6) || (i >= -6 && ! (i <= 12)))) && (! (i >= 0) || (i >= 0 && ! (i <= 18)))) && (! (i >= -2) || (i >= -2 && ! (i <= 16)))) && (! (i >= 2) || (i >= 2 && ! (i <= 20)))) && (! (i >= -8) || (i >= -8 && ! (i <= 10)))) && (! (i >= -5) || (i >= -5 && ! (i <= 13)))) && (! (i >= 4) || (i >= 4 && ! (i <= 22)))) && (! (i >= -9) || (i >= -9 && ! (i <= 9)))) && (! (i >= 1) || (i >= 1 && ! (i <= 19)))) && (! (i >= -1) || (i >= -1 && ! (i <= 17)))) && (! (i >= 5) || (i >= 5 && ! (i <= 23)))) && i >= -4) && i <= 14) (../plain/benchmark52_polynomial.i:23:5-23:14)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 13
  dead: 0
  total lines: 13
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (../plain/benchmark52_polynomial.i:11:76-11:77)
[Warning][Witness] invariant unconfirmed: (i >= (-7) && i <= (11)) || ((!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && i >= (-3) && i <= (15)) || ((!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && i >= (3) && i <= (21)) || ((!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (3)) || (i >= (3) && !(i <= (21)))) && i >= (-6) && i <= (12)) || ((!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && i >= (0) && i <= (18)) || ((!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (0)) || (i >= (0) && !(i <= (18)))) && i >= (-2) && i <= (16)) || ((!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (0)) || (i >= (0) && !(i <= (18)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && i >= (2) && i <= (20)) || ((!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (0)) || (i >= (0) && !(i <= (18)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && (!(i >= (2)) || (i >= (2) && !(i <= (20)))) && i >= (-8) && i <= (10)) || ((!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (0)) || (i >= (0) && !(i <= (18)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && (!(i >= (2)) || (i >= (2) && !(i <= (20)))) && (!(i >= (-8)) || (i >= (-8) && !(i <= (10)))) && i >= (-5) && i <= (13)) || ((!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (0)) || (i >= (0) && !(i <= (18)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && (!(i >= (2)) || (i >= (2) && !(i <= (20)))) && (!(i >= (-8)) || (i >= (-8) && !(i <= (10)))) && (!(i >= (-5)) || (i >= (-5) && !(i <= (13)))) && i >= (4) && i <= (22)) || ((!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (0)) || (i >= (0) && !(i <= (18)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && (!(i >= (2)) || (i >= (2) && !(i <= (20)))) && (!(i >= (-8)) || (i >= (-8) && !(i <= (10)))) && (!(i >= (-5)) || (i >= (-5) && !(i <= (13)))) && (!(i >= (4)) || (i >= (4) && !(i <= (22)))) && i >= (-9) && i <= (9)) || ((!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (0)) || (i >= (0) && !(i <= (18)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && (!(i >= (2)) || (i >= (2) && !(i <= (20)))) && (!(i >= (-8)) || (i >= (-8) && !(i <= (10)))) && (!(i >= (-5)) || (i >= (-5) && !(i <= (13)))) && (!(i >= (4)) || (i >= (4) && !(i <= (22)))) && (!(i >= (-9)) || (i >= (-9) && !(i <= (9)))) && i >= (1) && i <= (19)) || ((!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (0)) || (i >= (0) && !(i <= (18)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && (!(i >= (2)) || (i >= (2) && !(i <= (20)))) && (!(i >= (-8)) || (i >= (-8) && !(i <= (10)))) && (!(i >= (-5)) || (i >= (-5) && !(i <= (13)))) && (!(i >= (4)) || (i >= (4) && !(i <= (22)))) && (!(i >= (-9)) || (i >= (-9) && !(i <= (9)))) && (!(i >= (1)) || (i >= (1) && !(i <= (19)))) && i >= (-1) && i <= (17)) || ((!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (0)) || (i >= (0) && !(i <= (18)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && (!(i >= (2)) || (i >= (2) && !(i <= (20)))) && (!(i >= (-8)) || (i >= (-8) && !(i <= (10)))) && (!(i >= (-5)) || (i >= (-5) && !(i <= (13)))) && (!(i >= (4)) || (i >= (4) && !(i <= (22)))) && (!(i >= (-9)) || (i >= (-9) && !(i <= (9)))) && (!(i >= (1)) || (i >= (1) && !(i <= (19)))) && (!(i >= (-1)) || (i >= (-1) && !(i <= (17)))) && i >= (5) && i <= (23)) || ((!(i >= (-7)) || (i >= (-7) && !(i <= (11)))) && (!(i >= (-3)) || (i >= (-3) && !(i <= (15)))) && (!(i >= (3)) || (i >= (3) && !(i <= (21)))) && (!(i >= (-6)) || (i >= (-6) && !(i <= (12)))) && (!(i >= (0)) || (i >= (0) && !(i <= (18)))) && (!(i >= (-2)) || (i >= (-2) && !(i <= (16)))) && (!(i >= (2)) || (i >= (2) && !(i <= (20)))) && (!(i >= (-8)) || (i >= (-8) && !(i <= (10)))) && (!(i >= (-5)) || (i >= (-5) && !(i <= (13)))) && (!(i >= (4)) || (i >= (4) && !(i <= (22)))) && (!(i >= (-9)) || (i >= (-9) && !(i <= (9)))) && (!(i >= (1)) || (i >= (1) && !(i <= (19)))) && (!(i >= (-1)) || (i >= (-1) && !(i <= (17)))) && (!(i >= (5)) || (i >= (5) && !(i <= (23)))) && i >= (-4) && i <= (14)) (../plain/benchmark52_polynomial.i:22:3)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 1
  refuted: 0
  error: 2
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 3
SV-COMP result: unknown

vars = 32    evals = 29    narrow_reuses = 1

Timings:
                                  cputime   walltime   allocated   count
Default                            0.518s     0.535s    171.11MB      1×
  preprocess                         0.023s     0.022s      0.01MB      1×
  FrontC                             0.005s     0.005s      4.10MB      4×
  Cabs2cil                           0.005s     0.005s      4.71MB      4×
  mergeCIL                           0.003s     0.003s      3.34MB      1×
  analysis                           0.479s     0.495s    154.02MB      1×
    createCFG                          0.001s     0.001s      0.60MB      1×
      handle                             0.001s     0.001s      0.09MB     33×
      iter_connect                       0.001s     0.001s      0.40MB     33×
        computeSCCs                        0.001s     0.001s      0.23MB     34×
    FrontC                             0.013s     0.013s      2.81MB      2×
    Cabs2cil                           0.002s     0.002s      2.20MB      2×
    global_inits                       0.001s     0.001s      0.05MB      1×
    solving                            0.206s     0.206s    122.44MB      1×
      S.Dom.equal                        0.001s     0.001s      0.02MB     30×
      base unassume                      0.081s     0.081s     97.50MB      9×
      cheap_full_reach                   0.001s     0.001s      0.02MB      1×
      postsolver                         0.008s     0.008s      7.31MB      1×
        postsolver_iter                    0.008s     0.008s      7.27MB      1×
    warn_global                        0.001s     0.001s      0.11MB      1×
    witness                            0.001s     0.001s      0.01MB      1×
    result output                      0.001s     0.001s      0.01MB      1×
