- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: aa762221-faf7-4cff-819e-29ef4a303b2d
    creation_time: 2025-03-20T23:41:28Z
    producer:
      name: Goblint
      version: heads/master-0-g66dff5a90-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp.json'' ''--disable'' ''witness.graphml.enabled''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/valid-memsafety.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i: e4aac8fd1b71e0bd84f9ab8e5c238dc6bf3a295fcb9cebe504ba6d0c9a6a7b7a
      data_model: ILP32
      language: C
      specification: 'CHECK( init(main()), LTL(G valid-free) )

        CHECK( init(main()), LTL(G valid-deref) )

        CHECK( init(main()), LTL(G valid-memtrack) )'
  content:
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 741
        column: 9
        function: main
      value: 0 == z
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 741
        column: 9
        function: main
      value: z == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 741
        column: 9
        function: main
      value: ((((((((((i == 1 && (((((y == 4 && ((4 <= length && (length <= 8 || length
        <= 5)) || length == 4)) || (y == 3 && ((3 <= length && ((length <= 7 || length
        <= 5) || length <= 4)) || length == 3))) || (y == 2 && ((2 <= length && (((length
        <= 6 || length <= 5) || length <= 4) || length <= 3)) || length == 2))) ||
        (y == 1 && ((1 <= length && (((length <= 5 || length <= 4) || length <= 3)
        || length <= 2)) || length == 1))) || (((0 == y && y == 0) && y == z) && (((((((0
        == length && y == length) && z == length) && length == 0) || ((((length ==
        0 || length == 1) || length == 2) || length == 3) || length == 4)) || (((length
        == 0 || length == 1) || length == 2) || length == 3)) || ((length == 0 ||
        length == 1) || length == 2)) || (length == 0 || length == 1))))) || ((((0
        == i && i == 0) && i == z) && y == 4) && length == 4)) || ((((0 == i && i
        == 0) && i == z) && y == 3) && length == 3)) || ((((0 == i && i == 0) && i
        == z) && y == 2) && length == 2)) || ((((0 == i && i == 0) && i == z) && y
        == 1) && length == 1)) || (((((((((((0 == i && 0 == y) && 0 == length) &&
        i == 0) && i == y) && i == z) && i == length) && y == 0) && y == z) && y ==
        length) && z == length) && length == 0)) || ((i == 2 && y == 4) && ((4 <=
        length && (length <= 12 || length <= 5)) || length == 4))) || ((i == 2 &&
        y == 3) && ((3 <= length && ((length <= 11 || length <= 5) || length <= 4))
        || length == 3))) || ((i == 2 && y == 2) && ((2 <= length && (((length <=
        10 || length <= 5) || length <= 4) || length <= 3)) || length == 2))) || ((i
        == 2 && y == 1) && ((1 <= length && ((((length <= 9 || length <= 5) || length
        <= 4) || length <= 3) || length <= 2)) || length == 1))) || ((((0 == y &&
        i == 2) && y == 0) && y == z) && (((((((((0 == length && y == length) && z
        == length) && length == 0) || (0 <= length && length <= 8)) || (0 <= length
        && length <= 5)) || (0 <= length && length <= 4)) || (0 <= length && length
        <= 3)) || (0 <= length && length <= 2)) || (length == 0 || length == 1)))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 740
        column: 5
        function: main
      value: 0 == y
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 740
        column: 5
        function: main
      value: 0 == z
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 740
        column: 5
        function: main
      value: y == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 740
        column: 5
        function: main
      value: y == z
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 740
        column: 5
        function: main
      value: z == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 740
        column: 5
        function: main
      value: (((i == 1 && (((((((0 == length && y == length) && z == length) && length
        == 0) || ((((length == 0 || length == 1) || length == 2) || length == 3) ||
        length == 4)) || (((length == 0 || length == 1) || length == 2) || length
        == 3)) || ((length == 0 || length == 1) || length == 2)) || (length == 0 ||
        length == 1))) || (i == 3 && (((((((((0 == length && y == length) && z ==
        length) && length == 0) || (0 <= length && length <= 12)) || (0 <= length
        && length <= 5)) || (0 <= length && length <= 4)) || (0 <= length && length
        <= 3)) || (0 <= length && length <= 2)) || (length == 0 || length == 1))))
        || ((((((((0 == i && 0 == length) && i == 0) && i == y) && i == z) && i ==
        length) && y == length) && z == length) && length == 0)) || (i == 2 && (((((((((0
        == length && y == length) && z == length) && length == 0) || (0 <= length
        && length <= 8)) || (0 <= length && length <= 5)) || (0 <= length && length
        <= 4)) || (0 <= length && length <= 3)) || (0 <= length && length <= 2)) ||
        (length == 0 || length == 1)))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 683
        column: 5
        function: create_item
      value: 0 == term_field
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 683
        column: 5
        function: create_item
      value: 1 == link_field
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 683
        column: 5
        function: create_item
      value: (unsigned int )at == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 683
        column: 5
        function: create_item
      value: (unsigned int )term_field == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 683
        column: 5
        function: create_item
      value: (unsigned int )link_field == 1U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 683
        column: 5
        function: create_item
      value: (cursor == & (*(*cursor))[link_field] && (((0 == y && y == 0) && h ==
        0) || ((1 == y && y == 1) && h == 1))) || (((1 == y && 2 == h) && y == 1)
        && h == 2)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 768
        column: 5
        function: main
      value: 0 == y
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 768
        column: 5
        function: main
      value: 0 == z
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 768
        column: 5
        function: main
      value: y == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 768
        column: 5
        function: main
      value: y == z
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 768
        column: 5
        function: main
      value: z == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 768
        column: 5
        function: main
      value: (unsigned int )end_point == 0U || (unsigned int )end_point == 1U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 768
        column: 5
        function: main
      value: (unsigned int )direction == 0U || (unsigned int )direction == 1U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 768
        column: 5
        function: main
      value: ((((((cursor == next && ((((((i == 2 || i == 3) && ((0 <= length && length
        <= 6) || ((0 <= length && length <= 7) || length == 0))) || (((0 <= length
        && (length <= 8 || length <= 1)) && (i == 2 || i == 3)) || (length == 0 &&
        ((i == 1 || i == 2) || i == 3)))) || ((0 <= length && (((length <= 9 || length
        <= 2) && (i == 2 || i == 3)) || (length <= 1 && ((i == 1 || i == 2) || i ==
        3)))) || (length == 0 && ((i == 1 || i == 2) || i == 3)))) || ((0 <= length
        && ((((length <= 10 || length <= 3) && (i == 2 || i == 3)) || (length <= 2
        && ((i == 1 || i == 2) || i == 3))) || (length <= 1 && ((i == 1 || i == 2)
        || i == 3)))) || (length == 0 && ((i == 1 || i == 2) || i == 3)))) || ((0
        <= length && (((((length <= 11 || length <= 4) && (i == 2 || i == 3)) || (length
        <= 3 && ((i == 1 || i == 2) || i == 3))) || (length <= 2 && ((i == 1 || i
        == 2) || i == 3))) || (length <= 1 && ((i == 1 || i == 2) || i == 3)))) ||
        (((length == 0 && cursor == 0) && next == 0) && ((i == 1 || i == 2) || i ==
        3))))) || (((((((((((0 == length && y == length) && z == length) && length
        == 0) && cursor == 0) && (((i == 0 || i == 1) || i == 2) || i == 3)) || ((0
        <= length && length <= 12) && (i == 2 || i == 3))) || ((0 <= length && length
        <= 5) && (i == 2 || i == 3))) || ((0 <= length && length <= 4) && ((i == 1
        || i == 2) || i == 3))) || ((0 <= length && length <= 3) && ((i == 1 || i
        == 2) || i == 3))) || ((0 <= length && length <= 2) && ((i == 1 || i == 2)
        || i == 3))) || ((length == 0 || length == 1) && ((i == 1 || i == 2) || i
        == 3)))) || (((0 <= length && length <= 1) && cursor == next) && (i == 2 ||
        i == 3))) || (((0 <= length && length <= 2) && cursor == next) && (i == 2
        || i == 3))) || (((0 <= length && length <= 3) && cursor == next) && (i ==
        2 || i == 3))) || (((0 <= length && length <= 4) && cursor == next) && (i
        == 2 || i == 3))) || (((0 <= length && length <= 5) && cursor == next) &&
        (i == 2 || i == 3))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext-properties/test-0217_1.i
        line: 746
        column: 9
        function: main
      value: (((((((((((((((((((i == 1 && (((((z == 4 && ((((((((((0 == y && 0 ==
        length) && y == 0) && y == length) && length == 0) || ((0 <= length && length
        <= 4) && ((y == 2 || y == 3) || y == 4))) || ((0 <= length && length <= 1)
        && (((y == 1 || y == 2) || y == 3) || y == 4))) || (length == 0 && ((((y ==
        0 || y == 1) || y == 2) || y == 3) || y == 4))) || (length == 0 && (((y ==
        0 || y == 1) || y == 2) || y == 3))) || (length == 0 && ((y == 0 || y == 1)
        || y == 2))) || (length == 0 && (y == 0 || y == 1)))) || (z == 3 && ((((((((((0
        == y && 0 == length) && y == 0) && y == length) && length == 0) || ((0 <=
        length && length <= 5) && ((y == 2 || y == 3) || y == 4))) || ((0 <= length
        && length <= 2) && (((y == 1 || y == 2) || y == 3) || y == 4))) || ((0 <=
        length && length <= 1) && ((((y == 0 || y == 1) || y == 2) || y == 3) || y
        == 4))) || (length == 0 && (((y == 0 || y == 1) || y == 2) || y == 3))) ||
        (length == 0 && ((y == 0 || y == 1) || y == 2))) || (length == 0 && (y ==
        0 || y == 1))))) || (z == 2 && ((((((((((0 == y && 0 == length) && y == 0)
        && y == length) && length == 0) || ((0 <= length && length <= 6) && ((y ==
        2 || y == 3) || y == 4))) || ((0 <= length && length <= 3) && (((y == 1 ||
        y == 2) || y == 3) || y == 4))) || ((0 <= length && length <= 2) && ((((y
        == 0 || y == 1) || y == 2) || y == 3) || y == 4))) || ((0 <= length && length
        <= 1) && (((y == 0 || y == 1) || y == 2) || y == 3))) || (length == 0 && ((y
        == 0 || y == 1) || y == 2))) || (length == 0 && (y == 0 || y == 1))))) ||
        (z == 1 && ((((((((((0 == y && 0 == length) && y == 0) && y == length) &&
        length == 0) || ((1 <= length && length <= 7) && ((y == 2 || y == 3) || y
        == 4))) || ((0 <= length && length <= 4) && (((y == 1 || y == 2) || y == 3)
        || y == 4))) || ((0 <= length && length <= 3) && ((((y == 0 || y == 1) ||
        y == 2) || y == 3) || y == 4))) || ((0 <= length && length <= 2) && (((y ==
        0 || y == 1) || y == 2) || y == 3))) || ((0 <= length && length <= 1) && ((y
        == 0 || y == 1) || y == 2))) || (length == 0 && (y == 0 || y == 1))))) ||
        ((0 == z && z == 0) && ((((((((((((0 == y && 0 == length) && y == 0) && y
        == z) && y == length) && z == length) && length == 0) || ((2 <= length &&
        length <= 8) && ((y == 2 || y == 3) || y == 4))) || ((1 <= length && length
        <= 5) && (((y == 1 || y == 2) || y == 3) || y == 4))) || ((0 <= length &&
        length <= 4) && ((((y == 0 || y == 1) || y == 2) || y == 3) || y == 4))) ||
        ((0 <= length && length <= 3) && (((y == 0 || y == 1) || y == 2) || y == 3)))
        || ((0 <= length && length <= 2) && ((y == 0 || y == 1) || y == 2))) || ((y
        == 0 || y == 1) && (length == 0 || length == 1)))))) || ((((0 == i && i ==
        0) && z == 7) && length == 0) && (((((((((0 == y && 0 == length) && i == y)
        && i == length) && y == 0) && y == length) || y == 4) || y == 3) || y == 2)
        || y == 1))) || ((((0 == i && i == 0) && z == 6) && length == 0) && (((((((((0
        == y && 0 == length) && i == y) && i == length) && y == 0) && y == length)
        || y == 4) || y == 3) || y == 2) || y == 1))) || ((((0 == i && i == 0) &&
        z == 5) && length == 0) && (((((((((0 == y && 0 == length) && i == y) && i
        == length) && y == 0) && y == length) || y == 4) || y == 3) || y == 2) ||
        y == 1))) || ((((0 == i && i == 0) && z == 4) && length == 0) && (((((((((0
        == y && 0 == length) && i == y) && i == length) && y == 0) && y == length)
        || y == 4) || y == 3) || y == 2) || y == 1))) || (((0 == i && i == 0) && z
        == 3) && ((((((((((0 == y && 0 == length) && i == y) && i == length) && y
        == 0) && y == length) && length == 0) || (y == 4 && length == 1)) || (y ==
        3 && length == 0)) || (y == 2 && length == 0)) || (y == 1 && length == 0))))
        || (((0 == i && i == 0) && z == 2) && ((((((((((0 == y && 0 == length) &&
        i == y) && i == length) && y == 0) && y == length) && length == 0) || (y ==
        4 && length == 2)) || (y == 3 && length == 1)) || (y == 2 && length == 0))
        || (y == 1 && length == 0)))) || (((0 == i && i == 0) && z == 1) && ((((((((((0
        == y && 0 == length) && i == y) && i == length) && y == 0) && y == length)
        && length == 0) || (y == 4 && length == 3)) || (y == 3 && length == 2)) ||
        (y == 2 && length == 1)) || (y == 1 && length == 0)))) || (((((0 == i && 0
        == z) && i == 0) && i == z) && z == 0) && ((((((((((((0 == y && 0 == length)
        && i == y) && i == length) && y == 0) && y == z) && y == length) && z == length)
        && length == 0) || (y == 4 && length == 4)) || (y == 3 && length == 3)) ||
        (y == 2 && length == 2)) || (y == 1 && length == 1)))) || ((i == 2 && z ==
        7) && ((((((((((0 == y && 0 == length) && y == 0) && y == length) && length
        == 0) || ((0 <= length && length <= 5) && ((((y == 0 || y == 1) || y == 2)
        || y == 3) || y == 4))) || (length == 0 && ((((y == 0 || y == 1) || y == 2)
        || y == 3) || y == 4))) || (length == 0 && ((((y == 0 || y == 1) || y == 2)
        || y == 3) || y == 4))) || (length == 0 && (((y == 0 || y == 1) || y == 2)
        || y == 3))) || (length == 0 && ((y == 0 || y == 1) || y == 2))) || (length
        == 0 && (y == 0 || y == 1))))) || ((i == 2 && z == 6) && ((((((((((0 == y
        && 0 == length) && y == 0) && y == length) && length == 0) || ((0 <= length
        && length <= 6) && ((((y == 0 || y == 1) || y == 2) || y == 3) || y == 4)))
        || (length == 0 && ((((y == 0 || y == 1) || y == 2) || y == 3) || y == 4)))
        || (length == 0 && ((((y == 0 || y == 1) || y == 2) || y == 3) || y == 4)))
        || (length == 0 && (((y == 0 || y == 1) || y == 2) || y == 3))) || (length
        == 0 && ((y == 0 || y == 1) || y == 2))) || (length == 0 && (y == 0 || y ==
        1))))) || ((i == 2 && z == 5) && ((((((((((0 == y && 0 == length) && y ==
        0) && y == length) && length == 0) || ((0 <= length && length <= 7) && ((((y
        == 0 || y == 1) || y == 2) || y == 3) || y == 4))) || (length == 0 && ((((y
        == 0 || y == 1) || y == 2) || y == 3) || y == 4))) || (length == 0 && ((((y
        == 0 || y == 1) || y == 2) || y == 3) || y == 4))) || (length == 0 && (((y
        == 0 || y == 1) || y == 2) || y == 3))) || (length == 0 && ((y == 0 || y ==
        1) || y == 2))) || (length == 0 && (y == 0 || y == 1))))) || ((i == 2 && z
        == 4) && ((((((((((0 == y && 0 == length) && y == 0) && y == length) && length
        == 0) || ((0 <= length && length <= 8) && ((((y == 0 || y == 1) || y == 2)
        || y == 3) || y == 4))) || ((0 <= length && length <= 1) && ((((y == 0 ||
        y == 1) || y == 2) || y == 3) || y == 4))) || (length == 0 && ((((y == 0 ||
        y == 1) || y == 2) || y == 3) || y == 4))) || (length == 0 && (((y == 0 ||
        y == 1) || y == 2) || y == 3))) || (length == 0 && ((y == 0 || y == 1) ||
        y == 2))) || (length == 0 && (y == 0 || y == 1))))) || ((i == 2 && z == 3)
        && ((((((((((0 == y && 0 == length) && y == 0) && y == length) && length ==
        0) || ((0 <= length && length <= 9) && ((((y == 0 || y == 1) || y == 2) ||
        y == 3) || y == 4))) || ((0 <= length && length <= 2) && ((((y == 0 || y ==
        1) || y == 2) || y == 3) || y == 4))) || ((0 <= length && length <= 1) &&
        ((((y == 0 || y == 1) || y == 2) || y == 3) || y == 4))) || (length == 0 &&
        (((y == 0 || y == 1) || y == 2) || y == 3))) || (length == 0 && ((y == 0 ||
        y == 1) || y == 2))) || (length == 0 && (y == 0 || y == 1))))) || ((i == 2
        && z == 2) && ((((((((((0 == y && 0 == length) && y == 0) && y == length)
        && length == 0) || ((0 <= length && length <= 10) && ((((y == 0 || y == 1)
        || y == 2) || y == 3) || y == 4))) || ((0 <= length && length <= 3) && ((((y
        == 0 || y == 1) || y == 2) || y == 3) || y == 4))) || ((0 <= length && length
        <= 2) && ((((y == 0 || y == 1) || y == 2) || y == 3) || y == 4))) || ((0 <=
        length && length <= 1) && (((y == 0 || y == 1) || y == 2) || y == 3))) ||
        (length == 0 && ((y == 0 || y == 1) || y == 2))) || (length == 0 && (y ==
        0 || y == 1))))) || ((i == 2 && z == 1) && ((((((((((0 == y && 0 == length)
        && y == 0) && y == length) && length == 0) || ((0 <= length && length <= 11)
        && ((((y == 0 || y == 1) || y == 2) || y == 3) || y == 4))) || ((0 <= length
        && length <= 4) && ((((y == 0 || y == 1) || y == 2) || y == 3) || y == 4)))
        || ((0 <= length && length <= 3) && ((((y == 0 || y == 1) || y == 2) || y
        == 3) || y == 4))) || ((0 <= length && length <= 2) && (((y == 0 || y == 1)
        || y == 2) || y == 3))) || ((0 <= length && length <= 1) && ((y == 0 || y
        == 1) || y == 2))) || (length == 0 && (y == 0 || y == 1))))) || (((0 == z
        && i == 2) && z == 0) && ((((((((((((0 == y && 0 == length) && y == 0) &&
        y == z) && y == length) && z == length) && length == 0) || ((0 <= length &&
        length <= 12) && ((((y == 0 || y == 1) || y == 2) || y == 3) || y == 4)))
        || ((0 <= length && length <= 5) && ((((y == 0 || y == 1) || y == 2) || y
        == 3) || y == 4))) || ((0 <= length && length <= 4) && ((((y == 0 || y ==
        1) || y == 2) || y == 3) || y == 4))) || ((0 <= length && length <= 3) &&
        (((y == 0 || y == 1) || y == 2) || y == 3))) || ((0 <= length && length <=
        2) && ((y == 0 || y == 1) || y == 2))) || ((y == 0 || y == 1) && (length ==
        0 || length == 1))))) || ((i == 1 && z == 7) && ((((((((((0 == y && 0 == length)
        && y == 0) && y == length) && length == 0) || ((0 <= length && length <= 1)
        && ((y == 2 || y == 3) || y == 4))) || (length == 0 && (((y == 1 || y == 2)
        || y == 3) || y == 4))) || (length == 0 && ((((y == 0 || y == 1) || y == 2)
        || y == 3) || y == 4))) || (length == 0 && (((y == 0 || y == 1) || y == 2)
        || y == 3))) || (length == 0 && ((y == 0 || y == 1) || y == 2))) || (length
        == 0 && (y == 0 || y == 1))))) || ((i == 1 && z == 6) && ((((((((((0 == y
        && 0 == length) && y == 0) && y == length) && length == 0) || ((0 <= length
        && length <= 2) && ((y == 2 || y == 3) || y == 4))) || (length == 0 && (((y
        == 1 || y == 2) || y == 3) || y == 4))) || (length == 0 && ((((y == 0 || y
        == 1) || y == 2) || y == 3) || y == 4))) || (length == 0 && (((y == 0 || y
        == 1) || y == 2) || y == 3))) || (length == 0 && ((y == 0 || y == 1) || y
        == 2))) || (length == 0 && (y == 0 || y == 1))))) || ((i == 1 && z == 5) &&
        ((((((((((0 == y && 0 == length) && y == 0) && y == length) && length == 0)
        || ((0 <= length && length <= 3) && ((y == 2 || y == 3) || y == 4))) || (length
        == 0 && (((y == 1 || y == 2) || y == 3) || y == 4))) || (length == 0 && ((((y
        == 0 || y == 1) || y == 2) || y == 3) || y == 4))) || (length == 0 && (((y
        == 0 || y == 1) || y == 2) || y == 3))) || (length == 0 && ((y == 0 || y ==
        1) || y == 2))) || (length == 0 && (y == 0 || y == 1))))
      format: c_expression
