- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 31b95e26-6b52-4f79-a160-f9b0a671f576
    creation_time: 2025-03-22T11:30:51Z
    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/goblint-regression/28-race_reach_90-arrayloop2_racing.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i: f41f3c018db74ffccd5759d166eb9816a1bf73b1747e3e539ecb5bf51feb56af
      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/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1045
        column: 5
        function: t1_fun
      value: (unsigned int )arg == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1045
        column: 5
        function: t1_fun
      value: ((((((((((((((((((((((((((j <= 9 && ((((((((((((((((((((((7 <= j || 6
        <= j) || 6 <= j) || 6 <= j) || 6 <= j) || 6 <= j) || 5 <= j) || 5 <= j) ||
        5 <= j) || 5 <= j) || 5 <= j) || 4 <= j) || 4 <= j) || 4 <= j) || 4 <= j)
        || 4 <= j) || 3 <= j) || 3 <= j) || 3 <= j) || 3 <= j) || 3 <= j) || 2 <=
        j) || 2 <= j)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (2 <= j &&
        j <= 9)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (1 <= j && j <= 9))
        || j == 9) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (1 <= j && j <=
        9)) || (8 <= j && j <= 9)) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) ||
        (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (0 <= j && j <= 9)) || (8 <=
        j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <= 9)) || (0 <= j &&
        j <= 9)) || (7 <= j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <=
        9)) || (0 <= j && j <= 9)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1066
        column: 280
        function: t2_fun
      value: (unsigned int )arg == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1066
        column: 280
        function: t2_fun
      value: (((((((((((((((((((((((((((((((((((((((((((((j <= 9 && ((3 <= j || 2
        <= j) || 2 <= j)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (2 <= j
        && j <= 9)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (1 <= j && j <=
        9)) || j == 9) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (1 <= j &&
        j <= 9)) || (8 <= j && j <= 9)) || (1 <= j && j <= 9)) || (8 <= j && j <=
        9)) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (0 <= j && j <= 9)) ||
        (8 <= j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <= 9)) || (0 <=
        j && j <= 9)) || (7 <= j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j &&
        j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <= 9)) || (7 <= j && j <=
        9)) || (6 <= j && j <= 9)) || (6 <= j && j <= 9)) || (6 <= j && j <= 9)) ||
        (6 <= j && j <= 9)) || (6 <= j && j <= 9)) || (5 <= j && j <= 9)) || (5 <=
        j && j <= 9)) || (5 <= j && j <= 9)) || (5 <= j && j <= 9)) || (5 <= j &&
        j <= 9)) || (4 <= j && j <= 9)) || (4 <= j && j <= 9)) || (4 <= j && j <=
        9)) || (4 <= j && j <= 9)) || (4 <= j && j <= 9)) || (3 <= j && j <= 9)) ||
        (3 <= j && j <= 9)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1046
        column: 154
        function: t1_fun
      value: (unsigned int )arg == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1046
        column: 154
        function: t1_fun
      value: ((((((((((((((((((((((((((j <= 9 && ((((((((((((((((((((((7 <= j || 6
        <= j) || 6 <= j) || 6 <= j) || 6 <= j) || 6 <= j) || 5 <= j) || 5 <= j) ||
        5 <= j) || 5 <= j) || 5 <= j) || 4 <= j) || 4 <= j) || 4 <= j) || 4 <= j)
        || 4 <= j) || 3 <= j) || 3 <= j) || 3 <= j) || 3 <= j) || 3 <= j) || 2 <=
        j) || 2 <= j)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (2 <= j &&
        j <= 9)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (1 <= j && j <= 9))
        || j == 9) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (1 <= j && j <=
        9)) || (8 <= j && j <= 9)) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) ||
        (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (0 <= j && j <= 9)) || (8 <=
        j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <= 9)) || (0 <= j &&
        j <= 9)) || (7 <= j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <=
        9)) || (0 <= j && j <= 9)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1046
        column: 46
        function: t1_fun
      value: (unsigned int )arg == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1046
        column: 46
        function: t1_fun
      value: ((((((((((((((((((((((((((j <= 9 && ((((((((((((((((((((((7 <= j || 6
        <= j) || 6 <= j) || 6 <= j) || 6 <= j) || 6 <= j) || 5 <= j) || 5 <= j) ||
        5 <= j) || 5 <= j) || 5 <= j) || 4 <= j) || 4 <= j) || 4 <= j) || 4 <= j)
        || 4 <= j) || 3 <= j) || 3 <= j) || 3 <= j) || 3 <= j) || 3 <= j) || 2 <=
        j) || 2 <= j)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (2 <= j &&
        j <= 9)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (1 <= j && j <= 9))
        || j == 9) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (1 <= j && j <=
        9)) || (8 <= j && j <= 9)) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) ||
        (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (0 <= j && j <= 9)) || (8 <=
        j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <= 9)) || (0 <= j &&
        j <= 9)) || (7 <= j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <=
        9)) || (0 <= j && j <= 9)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1077
        column: 3
        function: main
      value: (j == 30 && (((((((((i == 10 || i == 9) || i == 8) || i == 7) || i ==
        6) || i == 5) || i == 4) || i == 3) || i == 2) || i == 1)) || (0 == i && i
        == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1066
        column: 7
        function: t2_fun
      value: (unsigned int )arg == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1066
        column: 7
        function: t2_fun
      value: (((((((((((((((((((((((((((((((((((((((((((((j <= 9 && ((3 <= j || 2
        <= j) || 2 <= j)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (2 <= j
        && j <= 9)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (1 <= j && j <=
        9)) || j == 9) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (1 <= j &&
        j <= 9)) || (8 <= j && j <= 9)) || (1 <= j && j <= 9)) || (8 <= j && j <=
        9)) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (0 <= j && j <= 9)) ||
        (8 <= j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <= 9)) || (0 <=
        j && j <= 9)) || (7 <= j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j &&
        j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <= 9)) || (7 <= j && j <=
        9)) || (6 <= j && j <= 9)) || (6 <= j && j <= 9)) || (6 <= j && j <= 9)) ||
        (6 <= j && j <= 9)) || (6 <= j && j <= 9)) || (5 <= j && j <= 9)) || (5 <=
        j && j <= 9)) || (5 <= j && j <= 9)) || (5 <= j && j <= 9)) || (5 <= j &&
        j <= 9)) || (4 <= j && j <= 9)) || (4 <= j && j <= 9)) || (4 <= j && j <=
        9)) || (4 <= j && j <= 9)) || (4 <= j && j <= 9)) || (3 <= j && j <= 9)) ||
        (3 <= j && j <= 9)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1083
        column: 3
        function: main
      value: i == 10
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1083
        column: 3
        function: main
      value: j == 30
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1083
        column: 3
        function: main
      value: i == 10000
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1083
        column: 3
        function: main
      value: i == 10000
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1083
        column: 3
        function: main
      value: ((((4 <= i && i <= 10000) || i == 3) || i == 2) || i == 1) || (0 == i
        && i == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1066
        column: 154
        function: t2_fun
      value: (unsigned int )arg == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1066
        column: 154
        function: t2_fun
      value: (((((((((((((((((((((((((((((((((((((((((((((j <= 9 && ((3 <= j || 2
        <= j) || 2 <= j)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (2 <= j
        && j <= 9)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (1 <= j && j <=
        9)) || j == 9) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (1 <= j &&
        j <= 9)) || (8 <= j && j <= 9)) || (1 <= j && j <= 9)) || (8 <= j && j <=
        9)) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (0 <= j && j <= 9)) ||
        (8 <= j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <= 9)) || (0 <=
        j && j <= 9)) || (7 <= j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j &&
        j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <= 9)) || (7 <= j && j <=
        9)) || (6 <= j && j <= 9)) || (6 <= j && j <= 9)) || (6 <= j && j <= 9)) ||
        (6 <= j && j <= 9)) || (6 <= j && j <= 9)) || (5 <= j && j <= 9)) || (5 <=
        j && j <= 9)) || (5 <= j && j <= 9)) || (5 <= j && j <= 9)) || (5 <= j &&
        j <= 9)) || (4 <= j && j <= 9)) || (4 <= j && j <= 9)) || (4 <= j && j <=
        9)) || (4 <= j && j <= 9)) || (4 <= j && j <= 9)) || (3 <= j && j <= 9)) ||
        (3 <= j && j <= 9)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1046
        column: 7
        function: t1_fun
      value: (unsigned int )arg == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1046
        column: 7
        function: t1_fun
      value: ((((((((((((((((((((((((((j <= 9 && ((((((((((((((((((((((7 <= j || 6
        <= j) || 6 <= j) || 6 <= j) || 6 <= j) || 6 <= j) || 5 <= j) || 5 <= j) ||
        5 <= j) || 5 <= j) || 5 <= j) || 4 <= j) || 4 <= j) || 4 <= j) || 4 <= j)
        || 4 <= j) || 3 <= j) || 3 <= j) || 3 <= j) || 3 <= j) || 3 <= j) || 2 <=
        j) || 2 <= j)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (2 <= j &&
        j <= 9)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (1 <= j && j <= 9))
        || j == 9) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (1 <= j && j <=
        9)) || (8 <= j && j <= 9)) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) ||
        (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (0 <= j && j <= 9)) || (8 <=
        j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <= 9)) || (0 <= j &&
        j <= 9)) || (7 <= j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <=
        9)) || (0 <= j && j <= 9)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1066
        column: 46
        function: t2_fun
      value: (unsigned int )arg == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1066
        column: 46
        function: t2_fun
      value: (((((((((((((((((((((((((((((((((((((((((((((j <= 9 && ((3 <= j || 2
        <= j) || 2 <= j)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (2 <= j
        && j <= 9)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (1 <= j && j <=
        9)) || j == 9) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (1 <= j &&
        j <= 9)) || (8 <= j && j <= 9)) || (1 <= j && j <= 9)) || (8 <= j && j <=
        9)) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (0 <= j && j <= 9)) ||
        (8 <= j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <= 9)) || (0 <=
        j && j <= 9)) || (7 <= j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j &&
        j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <= 9)) || (7 <= j && j <=
        9)) || (6 <= j && j <= 9)) || (6 <= j && j <= 9)) || (6 <= j && j <= 9)) ||
        (6 <= j && j <= 9)) || (6 <= j && j <= 9)) || (5 <= j && j <= 9)) || (5 <=
        j && j <= 9)) || (5 <= j && j <= 9)) || (5 <= j && j <= 9)) || (5 <= j &&
        j <= 9)) || (4 <= j && j <= 9)) || (4 <= j && j <= 9)) || (4 <= j && j <=
        9)) || (4 <= j && j <= 9)) || (4 <= j && j <= 9)) || (3 <= j && j <= 9)) ||
        (3 <= j && j <= 9)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1082
        column: 28
        function: main
      value: i == 10
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1082
        column: 28
        function: main
      value: j == 30
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1082
        column: 28
        function: main
      value: ((((4 <= i && i <= 10000) || i == 3) || i == 2) || i == 1) || (0 == i
        && i == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1061
        column: 3
        function: t2_fun
      value: (unsigned int )arg == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1061
        column: 3
        function: t2_fun
      value: ((((((((((3 <= j && j <= 10) || j == 10) || (2 <= j && j <= 10)) || (9
        <= j && j <= 10)) || (1 <= j && j <= 10)) || (8 <= j && j <= 10)) || 0 <=
        j) || (7 <= j && j <= 10)) || (6 <= j && j <= 10)) || (5 <= j && j <= 10))
        || (4 <= j && j <= 10)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1080
        column: 5
        function: main
      value: (((((((((((((((((((((((((((((((((((((((((((((i == 9 && (((((((((((10
        <= j && j <= 30) || j == 9) || j == 8) || j == 7) || j == 6) || j == 5) ||
        j == 4) || j == 3) || j == 2) || j == 1) || (0 == j && j == 0))) || (i ==
        8 && ((((((j == 9 || (10 <= j && j <= 30)) || j == 8) || j == 7) || j == 6)
        || j == 5) || j == 4))) || (i == 8 && j == 3)) || (i == 8 && j == 2)) || (i
        == 8 && j == 1)) || ((0 == j && i == 8) && j == 0)) || (i == 7 && (((((((10
        <= j && j <= 30) || j == 9) || j == 8) || j == 7) || j == 6) || j == 5) ||
        j == 4))) || (i == 7 && j == 3)) || (i == 7 && j == 2)) || (i == 7 && j ==
        1)) || ((0 == j && i == 7) && j == 0)) || (i == 6 && (((((((10 <= j && j <=
        30) || j == 9) || j == 8) || j == 7) || j == 6) || j == 5) || j == 4))) ||
        (i == 6 && j == 3)) || (i == 6 && j == 2)) || (i == 6 && j == 1)) || ((0 ==
        j && i == 6) && j == 0)) || (i == 5 && (((((((10 <= j && j <= 30) || j ==
        9) || j == 8) || j == 7) || j == 6) || j == 5) || j == 4))) || (i == 5 &&
        j == 3)) || (i == 5 && j == 2)) || (i == 5 && j == 1)) || ((0 == j && i ==
        5) && j == 0)) || (i == 4 && (((((((10 <= j && j <= 30) || j == 9) || j ==
        8) || j == 7) || j == 6) || j == 5) || j == 4))) || (i == 4 && j == 3)) ||
        (i == 4 && j == 2)) || (i == 4 && j == 1)) || ((0 == j && i == 4) && j ==
        0)) || (i == 3 && (((((((10 <= j && j <= 30) || j == 9) || j == 8) || j ==
        7) || j == 6) || j == 5) || j == 4))) || (i == 3 && j == 3)) || (i == 3 &&
        j == 2)) || (i == 3 && j == 1)) || ((0 == j && i == 3) && j == 0)) || (i ==
        2 && (((((((10 <= j && j <= 30) || j == 9) || j == 8) || j == 7) || j == 6)
        || j == 5) || j == 4))) || (i == 2 && j == 3)) || (i == 2 && j == 2)) || (i
        == 2 && j == 1)) || ((0 == j && i == 2) && j == 0)) || (i == 1 && (((((((10
        <= j && j <= 30) || j == 9) || j == 8) || j == 7) || j == 6) || j == 5) ||
        j == 4))) || (i == 1 && j == 3)) || (i == 1 && j == 2)) || (i == 1 && j ==
        1)) || ((0 == j && i == 1) && j == 0)) || ((0 == i && i == 0) && (((((((10
        <= j && j <= 30) || j == 9) || j == 8) || j == 7) || j == 5) || j == 6) ||
        j == 4))) || ((0 == i && i == 0) && j == 3)) || ((0 == i && i == 0) && j ==
        2)) || ((0 == i && i == 0) && j == 1)) || ((((0 == i && 0 == j) && i == 0)
        && i == j) && j == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1041
        column: 3
        function: t1_fun
      value: (unsigned int )arg == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1041
        column: 3
        function: t1_fun
      value: ((((((j <= 10 && ((((7 <= j || 6 <= j) || 5 <= j) || 4 <= j) || 3 <=
        j)) || j == 10) || (2 <= j && j <= 10)) || (9 <= j && j <= 10)) || (1 <= j
        && j <= 10)) || (8 <= j && j <= 10)) || 0 <= j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1046
        column: 280
        function: t1_fun
      value: (unsigned int )arg == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1046
        column: 280
        function: t1_fun
      value: ((((((((((((((((((((((((((j <= 9 && ((((((((((((((((((((((7 <= j || 6
        <= j) || 6 <= j) || 6 <= j) || 6 <= j) || 6 <= j) || 5 <= j) || 5 <= j) ||
        5 <= j) || 5 <= j) || 5 <= j) || 4 <= j) || 4 <= j) || 4 <= j) || 4 <= j)
        || 4 <= j) || 3 <= j) || 3 <= j) || 3 <= j) || 3 <= j) || 3 <= j) || 2 <=
        j) || 2 <= j)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (2 <= j &&
        j <= 9)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (1 <= j && j <= 9))
        || j == 9) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (1 <= j && j <=
        9)) || (8 <= j && j <= 9)) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) ||
        (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (0 <= j && j <= 9)) || (8 <=
        j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <= 9)) || (0 <= j &&
        j <= 9)) || (7 <= j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <=
        9)) || (0 <= j && j <= 9)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1083
        column: 72
        function: main
      value: i == 10
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1083
        column: 72
        function: main
      value: j == 30
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1083
        column: 72
        function: main
      value: i == 10000
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1083
        column: 72
        function: main
      value: i == 10000
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1083
        column: 72
        function: main
      value: i == 10000
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1083
        column: 72
        function: main
      value: ((((4 <= i && i <= 10000) || i == 3) || i == 2) || i == 1) || (0 == i
        && i == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1082
        column: 143
        function: main
      value: i == 10
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1082
        column: 143
        function: main
      value: j == 30
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1082
        column: 143
        function: main
      value: i == 10000
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1082
        column: 143
        function: main
      value: ((((4 <= i && i <= 10000) || i == 3) || i == 2) || i == 1) || (0 == i
        && i == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1065
        column: 5
        function: t2_fun
      value: (unsigned int )arg == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/28-race_reach_90-arrayloop2_racing.i
        line: 1065
        column: 5
        function: t2_fun
      value: (((((((((((((((((((((((((((((((((((((((((((((j <= 9 && ((3 <= j || 2
        <= j) || 2 <= j)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (2 <= j
        && j <= 9)) || j == 9) || (2 <= j && j <= 9)) || j == 9) || (1 <= j && j <=
        9)) || j == 9) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (1 <= j &&
        j <= 9)) || (8 <= j && j <= 9)) || (1 <= j && j <= 9)) || (8 <= j && j <=
        9)) || (1 <= j && j <= 9)) || (8 <= j && j <= 9)) || (0 <= j && j <= 9)) ||
        (8 <= j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <= 9)) || (0 <=
        j && j <= 9)) || (7 <= j && j <= 9)) || (0 <= j && j <= 9)) || (7 <= j &&
        j <= 9)) || (0 <= j && j <= 9)) || (7 <= j && j <= 9)) || (7 <= j && j <=
        9)) || (6 <= j && j <= 9)) || (6 <= j && j <= 9)) || (6 <= j && j <= 9)) ||
        (6 <= j && j <= 9)) || (6 <= j && j <= 9)) || (5 <= j && j <= 9)) || (5 <=
        j && j <= 9)) || (5 <= j && j <= 9)) || (5 <= j && j <= 9)) || (5 <= j &&
        j <= 9)) || (4 <= j && j <= 9)) || (4 <= j && j <= 9)) || (4 <= j && j <=
        9)) || (4 <= j && j <= 9)) || (4 <= j && j <= 9)) || (3 <= j && j <= 9)) ||
        (3 <= j && j <= 9)
      format: c_expression
