- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 2003a356-415d-4a60-b4cb-234519f994c1
    creation_time: 2025-03-22T18:07:38Z
    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/termination.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c: 484b00968af178bafd1c632864ac68eeb543ca8851deb47f0795724cfa80a660
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(F end) )
  content:
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (-2LL + (long long )N_COL) + (long long )N_LIN >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (-1LL + (long long )N_LIN) + (long long )j >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (-1LL + (long long )N_COL) + (long long )j >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (2147483647LL + (long long )N_LIN) + (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (2147483647LL + (long long )N_COL) + (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (2147483648LL + (long long )j) + (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (0LL - (long long )N_COL) + (long long )N_LIN >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (1LL - (long long )N_LIN) + (long long )j >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (1LL - (long long )N_COL) + (long long )j >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (2147483648LL - (long long )j) + (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (2147483649LL - (long long )N_LIN) + (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (2147483649LL - (long long )N_COL) + (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (-1LL + (long long )N_LIN) - (long long )j >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (-1LL + (long long )N_COL) - (long long )j >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (2147483646LL + (long long )N_LIN) - (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (2147483646LL + (long long )N_COL) - (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (2147483647LL + (long long )j) - (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (1LL - (long long )N_LIN) - (long long )j >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (1LL - (long long )N_COL) - (long long )j >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (2LL - (long long )N_COL) - (long long )N_LIN >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (2147483647LL - (long long )j) - (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (2147483648LL - (long long )N_LIN) - (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (2147483648LL - (long long )N_COL) - (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (long long )N_COL - (long long )N_LIN >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: 0U == j
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: 1U == N_LIN
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: 1U == N_COL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: N_LIN == 1U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: N_LIN == N_COL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: N_COL == 1U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: j == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 22
        column: 5
        function: main
      value: (((((((((((((((((-2LL + (long long )N_LIN) + (long long )k >= 0LL &&
        (-2LL + (long long )N_COL) + (long long )k >= 0LL) && (-1LL + (long long )j)
        + (long long )k >= 0LL) && (2147483647LL + (long long )k) + (long long )maior
        >= 0LL) && (-1LL - (long long )j) + (long long )k >= 0LL) && (0LL - (long
        long )N_LIN) + (long long )k >= 0LL) && (0LL - (long long )N_COL) + (long
        long )k >= 0LL) && (2147483649LL - (long long )k) + (long long )maior >= 0LL)
        && (1LL + (long long )j) - (long long )k >= 0LL) && (2147483646LL + (long
        long )k) - (long long )maior >= 0LL) && (1LL - (long long )j) - (long long
        )k >= 0LL) && (2LL - (long long )N_LIN) - (long long )k >= 0LL) && (2LL -
        (long long )N_COL) - (long long )k >= 0LL) && (2147483648LL - (long long )k)
        - (long long )maior >= 0LL) && (long long )N_LIN - (long long )k >= 0LL) &&
        (long long )N_COL - (long long )k >= 0LL) && k == 1U) || (((((((((((((((((((-1LL
        + (long long )N_LIN) + (long long )k >= 0LL && (-1LL + (long long )N_COL)
        + (long long )k >= 0LL) && (2147483648LL + (long long )k) + (long long )maior
        >= 0LL) && (0LL - (long long )j) + (long long )k >= 0LL) && (1LL - (long long
        )N_LIN) + (long long )k >= 0LL) && (1LL - (long long )N_COL) + (long long
        )k >= 0LL) && (2147483648LL - (long long )k) + (long long )maior >= 0LL) &&
        (long long )j + (long long )k >= 0LL) && (-1LL + (long long )N_LIN) - (long
        long )k >= 0LL) && (-1LL + (long long )N_COL) - (long long )k >= 0LL) && (2147483647LL
        + (long long )k) - (long long )maior >= 0LL) && (0LL - (long long )j) - (long
        long )k >= 0LL) && (1LL - (long long )N_LIN) - (long long )k >= 0LL) && (1LL
        - (long long )N_COL) - (long long )k >= 0LL) && (2147483647LL - (long long
        )k) - (long long )maior >= 0LL) && (long long )j - (long long )k >= 0LL) &&
        0U == k) && j == k) && k == 0U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 21
        column: 3
        function: main
      value: (-2LL + (long long )N_COL) + (long long )N_LIN >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 21
        column: 3
        function: main
      value: (2147483647LL + (long long )N_LIN) + (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 21
        column: 3
        function: main
      value: (2147483647LL + (long long )N_COL) + (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 21
        column: 3
        function: main
      value: (0LL - (long long )N_COL) + (long long )N_LIN >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 21
        column: 3
        function: main
      value: (0LL - (long long )j) + (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 21
        column: 3
        function: main
      value: (2147483649LL - (long long )N_LIN) + (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 21
        column: 3
        function: main
      value: (2147483649LL - (long long )N_COL) + (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 21
        column: 3
        function: main
      value: (2147483646LL + (long long )N_LIN) - (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 21
        column: 3
        function: main
      value: (2147483646LL + (long long )N_COL) - (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 21
        column: 3
        function: main
      value: (2LL - (long long )N_COL) - (long long )N_LIN >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 21
        column: 3
        function: main
      value: (2147483648LL - (long long )N_LIN) - (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 21
        column: 3
        function: main
      value: (2147483648LL - (long long )N_COL) - (long long )maior >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 21
        column: 3
        function: main
      value: (long long )N_COL - (long long )N_LIN >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 21
        column: 3
        function: main
      value: 1U == N_LIN
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 21
        column: 3
        function: main
      value: 1U == N_COL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 21
        column: 3
        function: main
      value: N_LIN == 1U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 21
        column: 3
        function: main
      value: N_LIN == N_COL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 21
        column: 3
        function: main
      value: N_COL == 1U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/matrix-1.c
        line: 21
        column: 3
        function: main
      value: (((((((((((((((((((((((((((((-2LL + (long long )N_LIN) + (long long )j
        >= 0LL && (-2LL + (long long )N_LIN) + (long long )k >= 0LL) && (-2LL + (long
        long )N_COL) + (long long )j >= 0LL) && (-2LL + (long long )N_COL) + (long
        long )k >= 0LL) && (-2LL + (long long )j) + (long long )k >= 0LL) && (2147483647LL
        + (long long )j) + (long long )maior >= 0LL) && (2147483647LL + (long long
        )k) + (long long )maior >= 0LL) && (0LL - (long long )N_LIN) + (long long
        )j >= 0LL) && (0LL - (long long )N_LIN) + (long long )k >= 0LL) && (0LL -
        (long long )N_COL) + (long long )j >= 0LL) && (0LL - (long long )N_COL) +
        (long long )k >= 0LL) && (2147483649LL - (long long )j) + (long long )maior
        >= 0LL) && (2147483649LL - (long long )k) + (long long )maior >= 0LL) && (2147483646LL
        + (long long )j) - (long long )maior >= 0LL) && (2147483646LL + (long long
        )k) - (long long )maior >= 0LL) && (2LL - (long long )N_LIN) - (long long
        )j >= 0LL) && (2LL - (long long )N_LIN) - (long long )k >= 0LL) && (2LL -
        (long long )N_COL) - (long long )j >= 0LL) && (2LL - (long long )N_COL) -
        (long long )k >= 0LL) && (2LL - (long long )j) - (long long )k >= 0LL) &&
        (2147483648LL - (long long )j) - (long long )maior >= 0LL) && (2147483648LL
        - (long long )k) - (long long )maior >= 0LL) && (long long )N_LIN - (long
        long )j >= 0LL) && (long long )N_LIN - (long long )k >= 0LL) && (long long
        )N_COL - (long long )j >= 0LL) && (long long )N_COL - (long long )k >= 0LL)
        && (long long )j - (long long )k >= 0LL) && j == 1U) && k == 1U) || (((((((((((((((((((((((((((((-1LL
        + (long long )N_LIN) + (long long )j >= 0LL && (-1LL + (long long )N_LIN)
        + (long long )k >= 0LL) && (-1LL + (long long )N_COL) + (long long )j >= 0LL)
        && (-1LL + (long long )N_COL) + (long long )k >= 0LL) && (2147483648LL + (long
        long )j) + (long long )maior >= 0LL) && (2147483648LL + (long long )k) + (long
        long )maior >= 0LL) && (1LL - (long long )N_LIN) + (long long )j >= 0LL) &&
        (1LL - (long long )N_LIN) + (long long )k >= 0LL) && (1LL - (long long )N_COL)
        + (long long )j >= 0LL) && (1LL - (long long )N_COL) + (long long )k >= 0LL)
        && (2147483648LL - (long long )j) + (long long )maior >= 0LL) && (6442450943LL
        - (long long )k) + (long long )maior >= 0LL) && (long long )j + (long long
        )k >= 0LL) && (-1LL + (long long )N_LIN) - (long long )j >= 0LL) && (-1LL
        + (long long )N_COL) - (long long )j >= 0LL) && (2147483647LL + (long long
        )j) - (long long )maior >= 0LL) && (2147483647LL + (long long )k) - (long
        long )maior >= 0LL) && (4294967294LL + (long long )N_LIN) - (long long )k
        >= 0LL) && (4294967294LL + (long long )N_COL) - (long long )k >= 0LL) && (4294967295LL
        + (long long )j) - (long long )k >= 0LL) && (1LL - (long long )N_LIN) - (long
        long )j >= 0LL) && (1LL - (long long )N_COL) - (long long )j >= 0LL) && (2147483647LL
        - (long long )j) - (long long )maior >= 0LL) && (4294967295LL - (long long
        )j) - (long long )k >= 0LL) && (4294967296LL - (long long )N_LIN) - (long
        long )k >= 0LL) && (4294967296LL - (long long )N_COL) - (long long )k >= 0LL)
        && (6442450942LL - (long long )k) - (long long )maior >= 0LL) && 0U == j)
        && j == 0U)
      format: c_expression
