- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 4531cc9f-469c-487d-b55a-8696a0fff526
    creation_time: 2025-03-22T11:17:46Z
    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/09-regions_22-nocollapse.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i: a0270befea30c9963adb19613f3074c8c29d9100e1f0592dc0c89cf3d3dda0df
      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/09-regions_22-nocollapse.i
        line: 1054
        column: 3
        function: main
      value: (((j == 30 && (((((((i == 8 || i == 7) || i == 6) || i == 5) || i ==
        4) || i == 3) || i == 2) || i == 1)) || (0 == i && i == 0)) || (i == 10 &&
        j == 30)) || (i == 9 && j == 30)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i
        line: 1057
        column: 5
        function: main
      value: ((((((((((((((((((((((((((((((((((((((((((((((((((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 == 5) || j == 6) || 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) && ((((((j == 9 || (10 <= j && j <= 30)) || j == 8) ||
        j == 7) || j == 6) || j == 5) || 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)) || (i == 9 && (((((((10
        <= j && j <= 30) || j == 9) || j == 8) || j == 7) || j == 6) || j == 5) ||
        j == 4))) || (i == 9 && j == 3)) || (i == 9 && j == 2)) || (i == 9 && j ==
        1)) || ((0 == j && i == 9) && 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)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i
        line: 1039
        column: 5
        function: f
      value: (unsigned int )arg == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i
        line: 1039
        column: 5
        function: f
      value: ((((((((((((((((((((((((((((((((((((((((((((((((j == 9 || (8 <= j &&
        j <= 9)) || (8 <= j && j <= 9)) || (8 <= j && j <= 9)) || (8 <= j && j <=
        9)) || (8 <= j && j <= 9)) || (7 <= j && j <= 9)) || (7 <= j && j <= 9)) ||
        (7 <= 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)) || (3 <= j && j <= 9)) || (3 <= j && j <= 9)) || (3 <= j && j <=
        9)) || (2 <= j && j <= 9)) || (2 <= j && j <= 9)) || (2 <= j && j <= 9)) ||
        (2 <= j && j <= 9)) || (2 <= j && j <= 9)) || (1 <= j && j <= 9)) || (1 <=
        j && j <= 9)) || (1 <= j && j <= 9)) || (1 <= j && j <= 9)) || (1 <= j &&
        j <= 9)) || (0 <= j && j <= 9)) || (0 <= j && j <= 9)) || (0 <= j && j <=
        9)) || (0 <= j && j <= 9)) || (0 <= j && j <= 9)) || j == 9) || j == 9) ||
        j == 9) || j == 9
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i
        line: 1035
        column: 3
        function: f
      value: (unsigned int )arg == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/goblint-regression/09-regions_22-nocollapse.i
        line: 1035
        column: 3
        function: f
      value: ((j <= 10 && ((((((((9 <= j || 8 <= j) || 7 <= j) || 6 <= j) || 5 <=
        j) || 4 <= j) || 3 <= j) || 2 <= j) || 1 <= j)) || 0 <= j) || j == 10
      format: c_expression
