- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: c1154961-4d0e-4f43-8028-a7987faff13a
    creation_time: 2025-03-22T18:08:29Z
    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/loop-lit/hhk2008.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-lit/hhk2008.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-lit/hhk2008.i: 71a7284f447428ecffa93ec68ad1c6e5855fc63e0841f7f396bb4f1c281c6b13
      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/loop-lit/hhk2008.i
        line: 32
        column: 5
        function: main
      value: 0 <= b
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-lit/hhk2008.i
        line: 32
        column: 5
        function: main
      value: 0 <= cnt
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-lit/hhk2008.i
        line: 32
        column: 5
        function: main
      value: a <= 1000000
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-lit/hhk2008.i
        line: 32
        column: 5
        function: main
      value: b <= 1000000
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-lit/hhk2008.i
        line: 32
        column: 5
        function: main
      value: (2147483648LL + (long long )a) + (long long )cnt >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-lit/hhk2008.i
        line: 32
        column: 5
        function: main
      value: (1000000LL - (long long )a) + (long long )cnt >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-lit/hhk2008.i
        line: 32
        column: 5
        function: main
      value: (2148483648LL + (long long )a) - (long long )b >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-lit/hhk2008.i
        line: 32
        column: 5
        function: main
      value: (2000000LL - (long long )a) - (long long )b >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-lit/hhk2008.i
        line: 32
        column: 5
        function: main
      value: (2000000LL - (long long )cnt) - (long long )res >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-lit/hhk2008.i
        line: 32
        column: 5
        function: main
      value: (((1000000LL + (long long )b) - (long long )res >= 0LL && (((((((((((((((((((((((((((((-2147483639
        <= res && res <= 1000009) && cnt <= 999991) && (-9LL + (long long )b) + (long
        long )cnt >= 0LL) && (2147483630LL + (long long )b) + (long long )res >= 0LL)
        && (2147483639LL + (long long )a) + (long long )b >= 0LL) && (2147483639LL
        + (long long )cnt) + (long long )res >= 0LL) && (4294967287LL + (long long
        )a) + (long long )res >= 0LL) && (-9LL - (long long )a) + (long long )res
        >= 0LL) && (9LL - (long long )b) + (long long )cnt >= 0LL) && (999991LL -
        (long long )a) + (long long )b >= 0LL) && (2148483630LL - (long long )cnt)
        + (long long )res >= 0LL) && (2148483639LL - (long long )b) + (long long )res
        >= 0LL) && (-9LL + (long long )b) - (long long )cnt >= 0LL) && (9LL + (long
        long )a) - (long long )res >= 0LL) && (1000009LL + (long long )cnt) - (long
        long )res >= 0LL) && (2148483639LL + (long long )a) - (long long )cnt >= 0LL)
        && (1999991LL - (long long )a) - (long long )cnt >= 0LL) && (1999991LL - (long
        long )b) - (long long )cnt >= 0LL) && (2000009LL - (long long )a) - (long
        long )res >= 0LL) && (2000009LL - (long long )b) - (long long )res >= 0LL)
        || ((((((((((((((((((((-2147483640 <= res && res <= 1000008) && cnt <= 999992)
        && (-8LL + (long long )b) + (long long )cnt >= 0LL) && (2147483632LL + (long
        long )b) + (long long )res >= 0LL) && (2147483640LL + (long long )a) + (long
        long )b >= 0LL) && (2147483640LL + (long long )cnt) + (long long )res >= 0LL)
        && (4294967288LL + (long long )a) + (long long )res >= 0LL) && (-8LL - (long
        long )a) + (long long )res >= 0LL) && (8LL - (long long )b) + (long long )cnt
        >= 0LL) && (999992LL - (long long )a) + (long long )b >= 0LL) && (2148483632LL
        - (long long )cnt) + (long long )res >= 0LL) && (2148483640LL - (long long
        )b) + (long long )res >= 0LL) && (-8LL + (long long )b) - (long long )cnt
        >= 0LL) && (8LL + (long long )a) - (long long )res >= 0LL) && (1000008LL +
        (long long )cnt) - (long long )res >= 0LL) && (2148483640LL + (long long )a)
        - (long long )cnt >= 0LL) && (1999992LL - (long long )a) - (long long )cnt
        >= 0LL) && (1999992LL - (long long )b) - (long long )cnt >= 0LL) && (2000008LL
        - (long long )a) - (long long )res >= 0LL) && (2000008LL - (long long )b)
        - (long long )res >= 0LL)) || ((((((((((((((((((((-2147483641 <= res && res
        <= 1000007) && cnt <= 999993) && (-7LL + (long long )b) + (long long )cnt
        >= 0LL) && (2147483634LL + (long long )b) + (long long )res >= 0LL) && (2147483641LL
        + (long long )a) + (long long )b >= 0LL) && (2147483641LL + (long long )cnt)
        + (long long )res >= 0LL) && (4294967289LL + (long long )a) + (long long )res
        >= 0LL) && (-7LL - (long long )a) + (long long )res >= 0LL) && (7LL - (long
        long )b) + (long long )cnt >= 0LL) && (999993LL - (long long )a) + (long long
        )b >= 0LL) && (2148483634LL - (long long )cnt) + (long long )res >= 0LL) &&
        (2148483641LL - (long long )b) + (long long )res >= 0LL) && (-7LL + (long
        long )b) - (long long )cnt >= 0LL) && (7LL + (long long )a) - (long long )res
        >= 0LL) && (1000007LL + (long long )cnt) - (long long )res >= 0LL) && (2148483641LL
        + (long long )a) - (long long )cnt >= 0LL) && (1999993LL - (long long )a)
        - (long long )cnt >= 0LL) && (1999993LL - (long long )b) - (long long )cnt
        >= 0LL) && (2000007LL - (long long )a) - (long long )res >= 0LL) && (2000007LL
        - (long long )b) - (long long )res >= 0LL)) || ((((((((((((((((((((-2147483642
        <= res && res <= 1000006) && cnt <= 999994) && (-6LL + (long long )b) + (long
        long )cnt >= 0LL) && (2147483636LL + (long long )b) + (long long )res >= 0LL)
        && (2147483642LL + (long long )a) + (long long )b >= 0LL) && (2147483642LL
        + (long long )cnt) + (long long )res >= 0LL) && (4294967290LL + (long long
        )a) + (long long )res >= 0LL) && (-6LL - (long long )a) + (long long )res
        >= 0LL) && (6LL - (long long )b) + (long long )cnt >= 0LL) && (999994LL -
        (long long )a) + (long long )b >= 0LL) && (2148483636LL - (long long )cnt)
        + (long long )res >= 0LL) && (2148483642LL - (long long )b) + (long long )res
        >= 0LL) && (-6LL + (long long )b) - (long long )cnt >= 0LL) && (6LL + (long
        long )a) - (long long )res >= 0LL) && (1000006LL + (long long )cnt) - (long
        long )res >= 0LL) && (2148483642LL + (long long )a) - (long long )cnt >= 0LL)
        && (1999994LL - (long long )a) - (long long )cnt >= 0LL) && (1999994LL - (long
        long )b) - (long long )cnt >= 0LL) && (2000006LL - (long long )a) - (long
        long )res >= 0LL) && (2000006LL - (long long )b) - (long long )res >= 0LL))
        || ((((((((((((((((((((-2147483643 <= res && res <= 1000005) && cnt <= 999995)
        && (-5LL + (long long )b) + (long long )cnt >= 0LL) && (2147483638LL + (long
        long )b) + (long long )res >= 0LL) && (2147483643LL + (long long )a) + (long
        long )b >= 0LL) && (2147483643LL + (long long )cnt) + (long long )res >= 0LL)
        && (4294967291LL + (long long )a) + (long long )res >= 0LL) && (-5LL - (long
        long )a) + (long long )res >= 0LL) && (5LL - (long long )b) + (long long )cnt
        >= 0LL) && (999995LL - (long long )a) + (long long )b >= 0LL) && (2148483638LL
        - (long long )cnt) + (long long )res >= 0LL) && (2148483643LL - (long long
        )b) + (long long )res >= 0LL) && (-5LL + (long long )b) - (long long )cnt
        >= 0LL) && (5LL + (long long )a) - (long long )res >= 0LL) && (1000005LL +
        (long long )cnt) - (long long )res >= 0LL) && (2148483643LL + (long long )a)
        - (long long )cnt >= 0LL) && (1999995LL - (long long )a) - (long long )cnt
        >= 0LL) && (1999995LL - (long long )b) - (long long )cnt >= 0LL) && (2000005LL
        - (long long )a) - (long long )res >= 0LL) && (2000005LL - (long long )b)
        - (long long )res >= 0LL)) || ((((((((((((((((((((-2147483644 <= res && res
        <= 1000004) && cnt <= 999996) && (-4LL + (long long )b) + (long long )cnt
        >= 0LL) && (2147483640LL + (long long )b) + (long long )res >= 0LL) && (2147483644LL
        + (long long )a) + (long long )b >= 0LL) && (2147483644LL + (long long )cnt)
        + (long long )res >= 0LL) && (4294967292LL + (long long )a) + (long long )res
        >= 0LL) && (-4LL - (long long )a) + (long long )res >= 0LL) && (4LL - (long
        long )b) + (long long )cnt >= 0LL) && (999996LL - (long long )a) + (long long
        )b >= 0LL) && (2148483640LL - (long long )cnt) + (long long )res >= 0LL) &&
        (2148483644LL - (long long )b) + (long long )res >= 0LL) && (-4LL + (long
        long )b) - (long long )cnt >= 0LL) && (4LL + (long long )a) - (long long )res
        >= 0LL) && (1000004LL + (long long )cnt) - (long long )res >= 0LL) && (2148483644LL
        + (long long )a) - (long long )cnt >= 0LL) && (1999996LL - (long long )a)
        - (long long )cnt >= 0LL) && (1999996LL - (long long )b) - (long long )cnt
        >= 0LL) && (2000004LL - (long long )a) - (long long )res >= 0LL) && (2000004LL
        - (long long )b) - (long long )res >= 0LL)) || ((((((((((((((((((((-2147483645
        <= res && res <= 1000003) && cnt <= 999997) && (-3LL + (long long )b) + (long
        long )cnt >= 0LL) && (2147483642LL + (long long )b) + (long long )res >= 0LL)
        && (2147483645LL + (long long )a) + (long long )b >= 0LL) && (2147483645LL
        + (long long )cnt) + (long long )res >= 0LL) && (4294967293LL + (long long
        )a) + (long long )res >= 0LL) && (-3LL - (long long )a) + (long long )res
        >= 0LL) && (3LL - (long long )b) + (long long )cnt >= 0LL) && (999997LL -
        (long long )a) + (long long )b >= 0LL) && (2148483642LL - (long long )cnt)
        + (long long )res >= 0LL) && (2148483645LL - (long long )b) + (long long )res
        >= 0LL) && (-3LL + (long long )b) - (long long )cnt >= 0LL) && (3LL + (long
        long )a) - (long long )res >= 0LL) && (1000003LL + (long long )cnt) - (long
        long )res >= 0LL) && (2148483645LL + (long long )a) - (long long )cnt >= 0LL)
        && (1999997LL - (long long )a) - (long long )cnt >= 0LL) && (1999997LL - (long
        long )b) - (long long )cnt >= 0LL) && (2000003LL - (long long )a) - (long
        long )res >= 0LL) && (2000003LL - (long long )b) - (long long )res >= 0LL))
        || ((((((((((((((((((((-2147483646 <= res && res <= 1000002) && cnt <= 999998)
        && (-2LL + (long long )b) + (long long )cnt >= 0LL) && (2147483644LL + (long
        long )b) + (long long )res >= 0LL) && (2147483646LL + (long long )a) + (long
        long )b >= 0LL) && (2147483646LL + (long long )cnt) + (long long )res >= 0LL)
        && (4294967294LL + (long long )a) + (long long )res >= 0LL) && (-2LL - (long
        long )a) + (long long )res >= 0LL) && (2LL - (long long )b) + (long long )cnt
        >= 0LL) && (999998LL - (long long )a) + (long long )b >= 0LL) && (2148483644LL
        - (long long )cnt) + (long long )res >= 0LL) && (2148483646LL - (long long
        )b) + (long long )res >= 0LL) && (-2LL + (long long )b) - (long long )cnt
        >= 0LL) && (2LL + (long long )a) - (long long )res >= 0LL) && (1000002LL +
        (long long )cnt) - (long long )res >= 0LL) && (2148483646LL + (long long )a)
        - (long long )cnt >= 0LL) && (1999998LL - (long long )a) - (long long )cnt
        >= 0LL) && (1999998LL - (long long )b) - (long long )cnt >= 0LL) && (2000002LL
        - (long long )a) - (long long )res >= 0LL) && (2000002LL - (long long )b)
        - (long long )res >= 0LL)) || ((((((((((((((((((((-2147483647 <= res && res
        <= 1000001) && cnt <= 999999) && (-1LL + (long long )b) + (long long )cnt
        >= 0LL) && (2147483646LL + (long long )b) + (long long )res >= 0LL) && (2147483647LL
        + (long long )a) + (long long )b >= 0LL) && (2147483647LL + (long long )cnt)
        + (long long )res >= 0LL) && (4294967295LL + (long long )a) + (long long )res
        >= 0LL) && (-1LL - (long long )a) + (long long )res >= 0LL) && (1LL - (long
        long )b) + (long long )cnt >= 0LL) && (999999LL - (long long )a) + (long long
        )b >= 0LL) && (2148483646LL - (long long )cnt) + (long long )res >= 0LL) &&
        (2148483647LL - (long long )b) + (long long )res >= 0LL) && (-1LL + (long
        long )b) - (long long )cnt >= 0LL) && (1LL + (long long )a) - (long long )res
        >= 0LL) && (1000001LL + (long long )cnt) - (long long )res >= 0LL) && (2148483647LL
        + (long long )a) - (long long )cnt >= 0LL) && (1999999LL - (long long )a)
        - (long long )cnt >= 0LL) && (1999999LL - (long long )b) - (long long )cnt
        >= 0LL) && (2000001LL - (long long )a) - (long long )res >= 0LL) && (2000001LL
        - (long long )b) - (long long )res >= 0LL)) || (((((((((((((((((((((res <=
        1000000 && cnt <= 1000000) && (2147483648LL + (long long )a) + (long long
        )b >= 0LL) && (2147483648LL + (long long )b) + (long long )res >= 0LL) &&
        (2147483648LL + (long long )cnt) + (long long )res >= 0LL) && (4294967296LL
        + (long long )a) + (long long )res >= 0LL) && (0LL - (long long )a) + (long
        long )res >= 0LL) && (0LL - (long long )b) + (long long )cnt >= 0LL) && (1000000LL
        - (long long )a) + (long long )b >= 0LL) && (2148483648LL - (long long )b)
        + (long long )res >= 0LL) && (2148483648LL - (long long )cnt) + (long long
        )res >= 0LL) && (long long )b + (long long )cnt >= 0LL) && (1000000LL + (long
        long )cnt) - (long long )res >= 0LL) && (2148483648LL + (long long )a) - (long
        long )cnt >= 0LL) && (2000000LL - (long long )a) - (long long )res >= 0LL)
        && (2000000LL - (long long )a) - (long long )cnt >= 0LL) && (2000000LL - (long
        long )b) - (long long )res >= 0LL) && (2000000LL - (long long )b) - (long
        long )cnt >= 0LL) && (long long )a - (long long )res >= 0LL) && (long long
        )b - (long long )cnt >= 0LL) && a == res) && b == cnt))) || (((((((((((((((((((((-2147483637
        <= res && res <= 2000000) && cnt <= 999989) && (-11LL + (long long )b) + (long
        long )cnt >= 0LL) && (2147483626LL + (long long )b) + (long long )res >= 0LL)
        && (2147483637LL + (long long )a) + (long long )b >= 0LL) && (2147483637LL
        + (long long )cnt) + (long long )res >= 0LL) && (4294967285LL + (long long
        )a) + (long long )res >= 0LL) && (-11LL - (long long )a) + (long long )res
        >= 0LL) && (999989LL - (long long )a) + (long long )b >= 0LL) && (1000000LL
        - (long long )b) + (long long )cnt >= 0LL) && (2148483626LL - (long long )cnt)
        + (long long )res >= 0LL) && (2148483637LL - (long long )b) + (long long )res
        >= 0LL) && (-11LL + (long long )b) - (long long )cnt >= 0LL) && (1999988LL
        + (long long )b) - (long long )res >= 0LL) && (2000000LL + (long long )cnt)
        - (long long )res >= 0LL) && (2148483637LL + (long long )a) - (long long )cnt
        >= 0LL) && (2149483648LL + (long long )a) - (long long )res >= 0LL) && (1999989LL
        - (long long )a) - (long long )cnt >= 0LL) && (1999989LL - (long long )b)
        - (long long )cnt >= 0LL) && (3000000LL - (long long )a) - (long long )res
        >= 0LL) && (3000000LL - (long long )b) - (long long )res >= 0LL)) || (((((((((((((((((((((-2147483638
        <= res && res <= 1000010) && cnt <= 999990) && (-10LL + (long long )b) + (long
        long )cnt >= 0LL) && (2147483628LL + (long long )b) + (long long )res >= 0LL)
        && (2147483638LL + (long long )a) + (long long )b >= 0LL) && (2147483638LL
        + (long long )cnt) + (long long )res >= 0LL) && (4294967286LL + (long long
        )a) + (long long )res >= 0LL) && (-10LL - (long long )a) + (long long )res
        >= 0LL) && (10LL - (long long )b) + (long long )cnt >= 0LL) && (999990LL -
        (long long )a) + (long long )b >= 0LL) && (2148483628LL - (long long )cnt)
        + (long long )res >= 0LL) && (2148483638LL - (long long )b) + (long long )res
        >= 0LL) && (-10LL + (long long )b) - (long long )cnt >= 0LL) && (10LL + (long
        long )a) - (long long )res >= 0LL) && (1000000LL + (long long )b) - (long
        long )res >= 0LL) && (1000010LL + (long long )cnt) - (long long )res >= 0LL)
        && (2148483638LL + (long long )a) - (long long )cnt >= 0LL) && (1999990LL
        - (long long )a) - (long long )cnt >= 0LL) && (1999990LL - (long long )b)
        - (long long )cnt >= 0LL) && (2000010LL - (long long )a) - (long long )res
        >= 0LL) && (2000010LL - (long long )b) - (long long )res >= 0LL)
      format: c_expression
