- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 20d84f1d-67d7-4689-a75f-f79cf0ff57ee
    creation_time: 2025-03-20T23:38: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/valid-memsafety.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c: 4cd641fa41c29ed0240eed782d3555502472fe8bb63d504547076d8eeefa2c0d
      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/verifythis/prefixsum_iter.c
        line: 54
        column: 5
        function: check
      value: (2147483647LL - (long long )n) + (long long )sum >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 54
        column: 5
        function: check
      value: (2147483647LL - (long long )n) - (long long )sum >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 54
        column: 5
        function: check
      value: sum == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 54
        column: 5
        function: check
      value: ((0LL - (long long )i) + (long long )n >= 0LL && (((((((((((((4 <= n
        && 4 <= i) && (-8LL + (long long )i) + (long long )n >= 0LL) && (-4LL + (long
        long )n) + (long long )sum >= 0LL) && (-4LL + (long long )i) + (long long
        )sum >= 0LL) && (2147483647LL - (long long )i) + (long long )sum >= 0LL) &&
        (-4LL + (long long )n) - (long long )sum >= 0LL) && (-4LL + (long long )i)
        - (long long )sum >= 0LL) && (2147483643LL + (long long )i) - (long long )n
        >= 0LL) && (2147483647LL - (long long )i) - (long long )sum >= 0LL) && (4294967294LL
        - (long long )i) - (long long )n >= 0LL) || ((((((((((3 <= n && (-6LL + (long
        long )i) + (long long )n >= 0LL) && (-3LL + (long long )n) + (long long )sum
        >= 0LL) && (-3LL + (long long )i) + (long long )sum >= 0LL) && (3LL - (long
        long )i) + (long long )sum >= 0LL) && (-3LL + (long long )n) - (long long
        )sum >= 0LL) && (-3LL + (long long )i) - (long long )sum >= 0LL) && (2147483644LL
        + (long long )i) - (long long )n >= 0LL) && (3LL - (long long )i) - (long
        long )sum >= 0LL) && (2147483650LL - (long long )i) - (long long )n >= 0LL)
        && i == 3)) || ((((((((((2 <= n && (-4LL + (long long )i) + (long long )n
        >= 0LL) && (-2LL + (long long )n) + (long long )sum >= 0LL) && (-2LL + (long
        long )i) + (long long )sum >= 0LL) && (2LL - (long long )i) + (long long )sum
        >= 0LL) && (-2LL + (long long )n) - (long long )sum >= 0LL) && (-2LL + (long
        long )i) - (long long )sum >= 0LL) && (2147483645LL + (long long )i) - (long
        long )n >= 0LL) && (2LL - (long long )i) - (long long )sum >= 0LL) && (2147483649LL
        - (long long )i) - (long long )n >= 0LL) && i == 2)) || ((((((((((1 <= n &&
        (-2LL + (long long )i) + (long long )n >= 0LL) && (-1LL + (long long )n) +
        (long long )sum >= 0LL) && (-1LL + (long long )i) + (long long )sum >= 0LL)
        && (1LL - (long long )i) + (long long )sum >= 0LL) && (-1LL + (long long )n)
        - (long long )sum >= 0LL) && (-1LL + (long long )i) - (long long )sum >= 0LL)
        && (2147483646LL + (long long )i) - (long long )n >= 0LL) && (1LL - (long
        long )i) - (long long )sum >= 0LL) && (2147483648LL - (long long )i) - (long
        long )n >= 0LL) && i == 1))) || ((((((((((((((-2147483647 <= n && (2147483647LL
        + (long long )n) + (long long )sum >= 0LL) && (2147483647LL + (long long )i)
        + (long long )n >= 0LL) && (0LL - (long long )i) + (long long )sum >= 0LL)
        && (2147483647LL - (long long )i) + (long long )n >= 0LL) && (long long )i
        + (long long )sum >= 0LL) && (2147483647LL + (long long )n) - (long long )sum
        >= 0LL) && (2147483647LL + (long long )i) - (long long )n >= 0LL) && (0LL
        - (long long )i) - (long long )sum >= 0LL) && (2147483647LL - (long long )i)
        - (long long )n >= 0LL) && (long long )i - (long long )sum >= 0LL) && 0 ==
        i) && 0 == sum) && i == 0) && i == sum)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 35
        column: 9
        function: downsweep
      value: 1 <= space
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 35
        column: 9
        function: downsweep
      value: (2147483647LL + (long long )space) + (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 35
        column: 9
        function: downsweep
      value: (2147483646LL - (long long )n) + (long long )space >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 35
        column: 9
        function: downsweep
      value: (4294967295LL - (long long )n) + (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 35
        column: 9
        function: downsweep
      value: (2147483646LL + (long long )space) - (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 35
        column: 9
        function: downsweep
      value: (4294967294LL - (long long )n) - (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 35
        column: 9
        function: downsweep
      value: right % 2 == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 35
        column: 9
        function: downsweep
      value: ((((((((((((((((((((((((((space <= 67108863 && (2214592512LL - (long
        long )space) + (long long )temp >= 0LL) && (2214592511LL - (long long )n)
        - (long long )space >= 0LL) && (2214592511LL - (long long )space) - (long
        long )temp >= 0LL) && ((((((((((((((((((((((0 <= left && 2 <= n) && 3 <= right)
        && right <= 268435451) && left <= 67108863) && (-5LL + (long long )n) + (long
        long )right >= 0LL) && (-4LL + (long long )right) + (long long )space >= 0LL)
        && (-3LL + (long long )n) + (long long )space >= 0LL) && (2147483645LL + (long
        long )right) + (long long )temp >= 0LL) && (2147483646LL + (long long )n)
        + (long long )temp >= 0LL) && (201326591LL - (long long )right) + (long long
        )space >= 0LL) && (2147483644LL - (long long )n) + (long long )right >= 0LL)
        && (2415919103LL - (long long )right) + (long long )temp >= 0LL) && (-2LL
        + (long long )right) - (long long )space >= 0LL) && (-1LL + (long long )n)
        - (long long )space >= 0LL) && (134217727LL + (long long )n) - (long long
        )right >= 0LL) && (2147483644LL + (long long )right) - (long long )temp >=
        0LL) && (2147483645LL + (long long )n) - (long long )temp >= 0LL) && (335544319LL
        - (long long )right) - (long long )space >= 0LL) && (2415919102LL - (long
        long )n) - (long long )right >= 0LL) && (2415919102LL - (long long )right)
        - (long long )temp >= 0LL) && temp == 0) || ((((((((((((((((((-2147483647
        <= n && 1 <= right) && right <= 134217725) && (-2LL + (long long )right) +
        (long long )space >= 0LL) && (2147483646LL + (long long )n) + (long long )space
        >= 0LL) && (2147483646LL + (long long )n) + (long long )right >= 0LL) && (2147483647LL
        + (long long )right) + (long long )temp >= 0LL) && (4294967295LL + (long long
        )n) + (long long )temp >= 0LL) && (67108863LL - (long long )right) + (long
        long )space >= 0LL) && (2147483646LL - (long long )n) + (long long )right
        >= 0LL) && (2281701375LL - (long long )right) + (long long )temp >= 0LL) &&
        (2147483646LL + (long long )right) - (long long )temp >= 0LL) && (2214592511LL
        + (long long )n) - (long long )space >= 0LL) && (2281701374LL + (long long
        )n) - (long long )right >= 0LL) && (4294967294LL + (long long )n) - (long
        long )temp >= 0LL) && (201326591LL - (long long )right) - (long long )space
        >= 0LL) && (2281701374LL - (long long )n) - (long long )right >= 0LL) && (2281701374LL
        - (long long )right) - (long long )temp >= 0LL) && (long long )right - (long
        long )space >= 0LL))) || ((((((((((((((((((((((((6 <= left && 8 <= n) && 9
        <= right) && space <= 134217727) && left <= 2147483645) && (-17LL + (long
        long )n) + (long long )right >= 0LL) && (-10LL + (long long )right) + (long
        long )space >= 0LL) && (-9LL + (long long )n) + (long long )space >= 0LL)
        && (2147483639LL + (long long )right) + (long long )temp >= 0LL) && (2147483640LL
        + (long long )n) + (long long )temp >= 0LL) && (2147483638LL - (long long
        )n) + (long long )right >= 0LL) && (2147483646LL - (long long )right) + (long
        long )space >= 0LL) && (2281701376LL - (long long )space) + (long long )temp
        >= 0LL) && (4294967295LL - (long long )right) + (long long )temp >= 0LL) &&
        (-8LL + (long long )right) - (long long )space >= 0LL) && (-7LL + (long long
        )n) - (long long )space >= 0LL) && (268435455LL + (long long )n) - (long long
        )right >= 0LL) && (2147483638LL + (long long )right) - (long long )temp >=
        0LL) && (2147483639LL + (long long )n) - (long long )temp >= 0LL) && (2281701375LL
        - (long long )n) - (long long )space >= 0LL) && (2281701375LL - (long long
        )space) - (long long )temp >= 0LL) && (2281701375LL - (long long )right) -
        (long long )space >= 0LL) && (4294967294LL - (long long )n) - (long long )right
        >= 0LL) && (4294967294LL - (long long )right) - (long long )temp >= 0LL) &&
        temp == 0)) || (((((((((((((((((((((((((4 <= left && 6 <= n) && 7 <= right)
        && space <= 134217727) && right <= 1073741815) && left <= 671088639) && (-13LL
        + (long long )n) + (long long )right >= 0LL) && (-8LL + (long long )right)
        + (long long )space >= 0LL) && (-7LL + (long long )n) + (long long )space
        >= 0LL) && (2147483641LL + (long long )right) + (long long )temp >= 0LL) &&
        (2147483642LL + (long long )n) + (long long )temp >= 0LL) && (939524095LL
        - (long long )right) + (long long )space >= 0LL) && (2147483640LL - (long
        long )n) + (long long )right >= 0LL) && (2281701376LL - (long long )space)
        + (long long )temp >= 0LL) && (3221225471LL - (long long )right) + (long long
        )temp >= 0LL) && (-6LL + (long long )right) - (long long )space >= 0LL) &&
        (-5LL + (long long )n) - (long long )space >= 0LL) && (268435455LL + (long
        long )n) - (long long )right >= 0LL) && (2147483640LL + (long long )right)
        - (long long )temp >= 0LL) && (2147483641LL + (long long )n) - (long long
        )temp >= 0LL) && (1207959551LL - (long long )right) - (long long )space >=
        0LL) && (2281701375LL - (long long )n) - (long long )space >= 0LL) && (2281701375LL
        - (long long )space) - (long long )temp >= 0LL) && (3221225470LL - (long long
        )n) - (long long )right >= 0LL) && (3221225470LL - (long long )right) - (long
        long )temp >= 0LL) && temp == 0)) || (((((((((((((((((((((((((2 <= left &&
        4 <= n) && 5 <= right) && space <= 134217727) && right <= 805306361) && left
        <= 402653183) && (-9LL + (long long )n) + (long long )right >= 0LL) && (-6LL
        + (long long )right) + (long long )space >= 0LL) && (-5LL + (long long )n)
        + (long long )space >= 0LL) && (2147483643LL + (long long )right) + (long
        long )temp >= 0LL) && (2147483644LL + (long long )n) + (long long )temp >=
        0LL) && (671088639LL - (long long )right) + (long long )space >= 0LL) && (2147483642LL
        - (long long )n) + (long long )right >= 0LL) && (2281701376LL - (long long
        )space) + (long long )temp >= 0LL) && (2952790015LL - (long long )right) +
        (long long )temp >= 0LL) && (-4LL + (long long )right) - (long long )space
        >= 0LL) && (-3LL + (long long )n) - (long long )space >= 0LL) && (268435455LL
        + (long long )n) - (long long )right >= 0LL) && (2147483642LL + (long long
        )right) - (long long )temp >= 0LL) && (2147483643LL + (long long )n) - (long
        long )temp >= 0LL) && (939524095LL - (long long )right) - (long long )space
        >= 0LL) && (2281701375LL - (long long )n) - (long long )space >= 0LL) && (2281701375LL
        - (long long )space) - (long long )temp >= 0LL) && (2952790014LL - (long long
        )n) - (long long )right >= 0LL) && (2952790014LL - (long long )right) - (long
        long )temp >= 0LL) && temp == 0)) || (((((((((((((((((((((((((0 <= left &&
        2 <= n) && 3 <= right) && space <= 134217727) && right <= 536870907) && left
        <= 134217727) && (-5LL + (long long )n) + (long long )right >= 0LL) && (-4LL
        + (long long )right) + (long long )space >= 0LL) && (-3LL + (long long )n)
        + (long long )space >= 0LL) && (2147483645LL + (long long )right) + (long
        long )temp >= 0LL) && (2147483646LL + (long long )n) + (long long )temp >=
        0LL) && (402653183LL - (long long )right) + (long long )space >= 0LL) && (2147483644LL
        - (long long )n) + (long long )right >= 0LL) && (2281701376LL - (long long
        )space) + (long long )temp >= 0LL) && (2684354559LL - (long long )right) +
        (long long )temp >= 0LL) && (-2LL + (long long )right) - (long long )space
        >= 0LL) && (-1LL + (long long )n) - (long long )space >= 0LL) && (268435455LL
        + (long long )n) - (long long )right >= 0LL) && (2147483644LL + (long long
        )right) - (long long )temp >= 0LL) && (2147483645LL + (long long )n) - (long
        long )temp >= 0LL) && (671088639LL - (long long )right) - (long long )space
        >= 0LL) && (2281701375LL - (long long )n) - (long long )space >= 0LL) && (2281701375LL
        - (long long )space) - (long long )temp >= 0LL) && (2684354558LL - (long long
        )n) - (long long )right >= 0LL) && (2684354558LL - (long long )right) - (long
        long )temp >= 0LL) && temp == 0)) || ((((((((((((((((((((((-2147483647 <=
        n && 1 <= right) && space <= 134217727) && right <= 268435453) && (-2LL +
        (long long )right) + (long long )space >= 0LL) && (2147483646LL + (long long
        )n) + (long long )space >= 0LL) && (2147483646LL + (long long )n) + (long
        long )right >= 0LL) && (2147483647LL + (long long )right) + (long long )temp
        >= 0LL) && (4294967295LL + (long long )n) + (long long )temp >= 0LL) && (134217727LL
        - (long long )right) + (long long )space >= 0LL) && (2147483646LL - (long
        long )n) + (long long )right >= 0LL) && (2281701376LL - (long long )space)
        + (long long )temp >= 0LL) && (2415919103LL - (long long )right) + (long long
        )temp >= 0LL) && (2147483646LL + (long long )right) - (long long )temp >=
        0LL) && (2281701375LL + (long long )n) - (long long )space >= 0LL) && (2415919102LL
        + (long long )n) - (long long )right >= 0LL) && (4294967294LL + (long long
        )n) - (long long )temp >= 0LL) && (402653183LL - (long long )right) - (long
        long )space >= 0LL) && (2281701375LL - (long long )n) - (long long )space
        >= 0LL) && (2281701375LL - (long long )space) - (long long )temp >= 0LL) &&
        (2415919102LL - (long long )n) - (long long )right >= 0LL) && (2415919102LL
        - (long long )right) - (long long )temp >= 0LL) && (long long )right - (long
        long )space >= 0LL)) || ((((((((((((((((((((((((6 <= left && 8 <= n) && 9
        <= right) && space <= 268435455) && left <= 2147483645) && (-17LL + (long
        long )n) + (long long )right >= 0LL) && (-10LL + (long long )right) + (long
        long )space >= 0LL) && (-9LL + (long long )n) + (long long )space >= 0LL)
        && (2147483639LL + (long long )right) + (long long )temp >= 0LL) && (2147483640LL
        + (long long )n) + (long long )temp >= 0LL) && (2147483638LL - (long long
        )n) + (long long )right >= 0LL) && (2147483646LL - (long long )right) + (long
        long )space >= 0LL) && (2415919104LL - (long long )space) + (long long )temp
        >= 0LL) && (4294967295LL - (long long )right) + (long long )temp >= 0LL) &&
        (-8LL + (long long )right) - (long long )space >= 0LL) && (-7LL + (long long
        )n) - (long long )space >= 0LL) && (536870911LL + (long long )n) - (long long
        )right >= 0LL) && (2147483638LL + (long long )right) - (long long )temp >=
        0LL) && (2147483639LL + (long long )n) - (long long )temp >= 0LL) && (2415919103LL
        - (long long )n) - (long long )space >= 0LL) && (2415919103LL - (long long
        )space) - (long long )temp >= 0LL) && (2415919103LL - (long long )right) -
        (long long )space >= 0LL) && (4294967294LL - (long long )n) - (long long )right
        >= 0LL) && (4294967294LL - (long long )right) - (long long )temp >= 0LL) &&
        temp == 0)) || (((((((((((((((((((((((((4 <= left && 6 <= n) && 7 <= right)
        && space <= 268435455) && right <= 2147483639) && left <= 1342177279) && (-13LL
        + (long long )n) + (long long )right >= 0LL) && (-8LL + (long long )right)
        + (long long )space >= 0LL) && (-7LL + (long long )n) + (long long )space
        >= 0LL) && (2147483641LL + (long long )right) + (long long )temp >= 0LL) &&
        (2147483642LL + (long long )n) + (long long )temp >= 0LL) && (1879048191LL
        - (long long )right) + (long long )space >= 0LL) && (2147483640LL - (long
        long )n) + (long long )right >= 0LL) && (2415919104LL - (long long )space)
        + (long long )temp >= 0LL) && (4294967295LL - (long long )right) + (long long
        )temp >= 0LL) && (-6LL + (long long )right) - (long long )space >= 0LL) &&
        (-5LL + (long long )n) - (long long )space >= 0LL) && (536870911LL + (long
        long )n) - (long long )right >= 0LL) && (2147483640LL + (long long )right)
        - (long long )temp >= 0LL) && (2147483641LL + (long long )n) - (long long
        )temp >= 0LL) && (2415919103LL - (long long )n) - (long long )space >= 0LL)
        && (2415919103LL - (long long )space) - (long long )temp >= 0LL) && (2415919103LL
        - (long long )right) - (long long )space >= 0LL) && (4294967294LL - (long
        long )n) - (long long )right >= 0LL) && (4294967294LL - (long long )right)
        - (long long )temp >= 0LL) && temp == 0)) || (((((((((((((((((((((((((2 <=
        left && 4 <= n) && 5 <= right) && space <= 268435455) && right <= 1610612729)
        && left <= 805306367) && (-9LL + (long long )n) + (long long )right >= 0LL)
        && (-6LL + (long long )right) + (long long )space >= 0LL) && (-5LL + (long
        long )n) + (long long )space >= 0LL) && (2147483643LL + (long long )right)
        + (long long )temp >= 0LL) && (2147483644LL + (long long )n) + (long long
        )temp >= 0LL) && (1342177279LL - (long long )right) + (long long )space >=
        0LL) && (2147483642LL - (long long )n) + (long long )right >= 0LL) && (2415919104LL
        - (long long )space) + (long long )temp >= 0LL) && (3758096383LL - (long long
        )right) + (long long )temp >= 0LL) && (-4LL + (long long )right) - (long long
        )space >= 0LL) && (-3LL + (long long )n) - (long long )space >= 0LL) && (536870911LL
        + (long long )n) - (long long )right >= 0LL) && (2147483642LL + (long long
        )right) - (long long )temp >= 0LL) && (2147483643LL + (long long )n) - (long
        long )temp >= 0LL) && (1879048191LL - (long long )right) - (long long )space
        >= 0LL) && (2415919103LL - (long long )n) - (long long )space >= 0LL) && (2415919103LL
        - (long long )space) - (long long )temp >= 0LL) && (3758096382LL - (long long
        )n) - (long long )right >= 0LL) && (3758096382LL - (long long )right) - (long
        long )temp >= 0LL) && temp == 0)) || (((((((((((((((((((((((((0 <= left &&
        2 <= n) && 3 <= right) && space <= 268435455) && right <= 1073741819) && left
        <= 268435455) && (-5LL + (long long )n) + (long long )right >= 0LL) && (-4LL
        + (long long )right) + (long long )space >= 0LL) && (-3LL + (long long )n)
        + (long long )space >= 0LL) && (2147483645LL + (long long )right) + (long
        long )temp >= 0LL) && (2147483646LL + (long long )n) + (long long )temp >=
        0LL) && (805306367LL - (long long )right) + (long long )space >= 0LL) && (2147483644LL
        - (long long )n) + (long long )right >= 0LL) && (2415919104LL - (long long
        )space) + (long long )temp >= 0LL) && (3221225471LL - (long long )right) +
        (long long )temp >= 0LL) && (-2LL + (long long )right) - (long long )space
        >= 0LL) && (-1LL + (long long )n) - (long long )space >= 0LL) && (536870911LL
        + (long long )n) - (long long )right >= 0LL) && (2147483644LL + (long long
        )right) - (long long )temp >= 0LL) && (2147483645LL + (long long )n) - (long
        long )temp >= 0LL) && (1342177279LL - (long long )right) - (long long )space
        >= 0LL) && (2415919103LL - (long long )n) - (long long )space >= 0LL) && (2415919103LL
        - (long long )space) - (long long )temp >= 0LL) && (3221225470LL - (long long
        )n) - (long long )right >= 0LL) && (3221225470LL - (long long )right) - (long
        long )temp >= 0LL) && temp == 0)) || ((((((((((((((((((((((-2147483647 <=
        n && 1 <= right) && space <= 268435455) && right <= 536870909) && (-2LL +
        (long long )right) + (long long )space >= 0LL) && (2147483646LL + (long long
        )n) + (long long )space >= 0LL) && (2147483646LL + (long long )n) + (long
        long )right >= 0LL) && (2147483647LL + (long long )right) + (long long )temp
        >= 0LL) && (4294967295LL + (long long )n) + (long long )temp >= 0LL) && (268435455LL
        - (long long )right) + (long long )space >= 0LL) && (2147483646LL - (long
        long )n) + (long long )right >= 0LL) && (2415919104LL - (long long )space)
        + (long long )temp >= 0LL) && (2684354559LL - (long long )right) + (long long
        )temp >= 0LL) && (2147483646LL + (long long )right) - (long long )temp >=
        0LL) && (2415919103LL + (long long )n) - (long long )space >= 0LL) && (2684354558LL
        + (long long )n) - (long long )right >= 0LL) && (4294967294LL + (long long
        )n) - (long long )temp >= 0LL) && (805306367LL - (long long )right) - (long
        long )space >= 0LL) && (2415919103LL - (long long )n) - (long long )space
        >= 0LL) && (2415919103LL - (long long )space) - (long long )temp >= 0LL) &&
        (2684354558LL - (long long )n) - (long long )right >= 0LL) && (2684354558LL
        - (long long )right) - (long long )temp >= 0LL) && (long long )right - (long
        long )space >= 0LL)) || ((((((((((((((((((((((((6 <= left && 8 <= n) && 9
        <= right) && space <= 536870911) && left <= 2147483645) && (-17LL + (long
        long )n) + (long long )right >= 0LL) && (-10LL + (long long )right) + (long
        long )space >= 0LL) && (-9LL + (long long )n) + (long long )space >= 0LL)
        && (2147483639LL + (long long )right) + (long long )temp >= 0LL) && (2147483640LL
        + (long long )n) + (long long )temp >= 0LL) && (2147483638LL - (long long
        )n) + (long long )right >= 0LL) && (2147483646LL - (long long )right) + (long
        long )space >= 0LL) && (2684354560LL - (long long )space) + (long long )temp
        >= 0LL) && (4294967295LL - (long long )right) + (long long )temp >= 0LL) &&
        (-8LL + (long long )right) - (long long )space >= 0LL) && (-7LL + (long long
        )n) - (long long )space >= 0LL) && (1073741823LL + (long long )n) - (long
        long )right >= 0LL) && (2147483638LL + (long long )right) - (long long )temp
        >= 0LL) && (2147483639LL + (long long )n) - (long long )temp >= 0LL) && (2684354559LL
        - (long long )n) - (long long )space >= 0LL) && (2684354559LL - (long long
        )space) - (long long )temp >= 0LL) && (2684354559LL - (long long )right) -
        (long long )space >= 0LL) && (4294967294LL - (long long )n) - (long long )right
        >= 0LL) && (4294967294LL - (long long )right) - (long long )temp >= 0LL) &&
        temp == 0)) || ((((((((((((((((((((((((4 <= left && 6 <= n) && 7 <= right)
        && space <= 536870911) && left <= 2147483645) && (-13LL + (long long )n) +
        (long long )right >= 0LL) && (-8LL + (long long )right) + (long long )space
        >= 0LL) && (-7LL + (long long )n) + (long long )space >= 0LL) && (2147483641LL
        + (long long )right) + (long long )temp >= 0LL) && (2147483642LL + (long long
        )n) + (long long )temp >= 0LL) && (2147483640LL - (long long )n) + (long long
        )right >= 0LL) && (2147483646LL - (long long )right) + (long long )space >=
        0LL) && (2684354560LL - (long long )space) + (long long )temp >= 0LL) && (4294967295LL
        - (long long )right) + (long long )temp >= 0LL) && (-6LL + (long long )right)
        - (long long )space >= 0LL) && (-5LL + (long long )n) - (long long )space
        >= 0LL) && (1073741823LL + (long long )n) - (long long )right >= 0LL) && (2147483640LL
        + (long long )right) - (long long )temp >= 0LL) && (2147483641LL + (long long
        )n) - (long long )temp >= 0LL) && (2684354559LL - (long long )n) - (long long
        )space >= 0LL) && (2684354559LL - (long long )space) - (long long )temp >=
        0LL) && (2684354559LL - (long long )right) - (long long )space >= 0LL) &&
        (4294967294LL - (long long )n) - (long long )right >= 0LL) && (4294967294LL
        - (long long )right) - (long long )temp >= 0LL) && temp == 0)) || ((((((((((((((((((((((((2
        <= left && 4 <= n) && 5 <= right) && space <= 536870911) && left <= 1610612735)
        && (-9LL + (long long )n) + (long long )right >= 0LL) && (-6LL + (long long
        )right) + (long long )space >= 0LL) && (-5LL + (long long )n) + (long long
        )space >= 0LL) && (2147483643LL + (long long )right) + (long long )temp >=
        0LL) && (2147483644LL + (long long )n) + (long long )temp >= 0LL) && (2147483642LL
        - (long long )n) + (long long )right >= 0LL) && (2147483646LL - (long long
        )right) + (long long )space >= 0LL) && (2684354560LL - (long long )space)
        + (long long )temp >= 0LL) && (4294967295LL - (long long )right) + (long long
        )temp >= 0LL) && (-4LL + (long long )right) - (long long )space >= 0LL) &&
        (-3LL + (long long )n) - (long long )space >= 0LL) && (1073741823LL + (long
        long )n) - (long long )right >= 0LL) && (2147483642LL + (long long )right)
        - (long long )temp >= 0LL) && (2147483643LL + (long long )n) - (long long
        )temp >= 0LL) && (2684354559LL - (long long )n) - (long long )space >= 0LL)
        && (2684354559LL - (long long )space) - (long long )temp >= 0LL) && (2684354559LL
        - (long long )right) - (long long )space >= 0LL) && (4294967294LL - (long
        long )n) - (long long )right >= 0LL) && (4294967294LL - (long long )right)
        - (long long )temp >= 0LL) && temp == 0)) || (((((((((((((((((((((((((0 <=
        left && 2 <= n) && 3 <= right) && space <= 536870911) && right <= 2147483643)
        && left <= 536870911) && (-5LL + (long long )n) + (long long )right >= 0LL)
        && (-4LL + (long long )right) + (long long )space >= 0LL) && (-3LL + (long
        long )n) + (long long )space >= 0LL) && (2147483645LL + (long long )right)
        + (long long )temp >= 0LL) && (2147483646LL + (long long )n) + (long long
        )temp >= 0LL) && (1610612735LL - (long long )right) + (long long )space >=
        0LL) && (2147483644LL - (long long )n) + (long long )right >= 0LL) && (2684354560LL
        - (long long )space) + (long long )temp >= 0LL) && (4294967295LL - (long long
        )right) + (long long )temp >= 0LL) && (-2LL + (long long )right) - (long long
        )space >= 0LL) && (-1LL + (long long )n) - (long long )space >= 0LL) && (1073741823LL
        + (long long )n) - (long long )right >= 0LL) && (2147483644LL + (long long
        )right) - (long long )temp >= 0LL) && (2147483645LL + (long long )n) - (long
        long )temp >= 0LL) && (2684354559LL - (long long )n) - (long long )space >=
        0LL) && (2684354559LL - (long long )space) - (long long )temp >= 0LL) && (2684354559LL
        - (long long )right) - (long long )space >= 0LL) && (4294967294LL - (long
        long )n) - (long long )right >= 0LL) && (4294967294LL - (long long )right)
        - (long long )temp >= 0LL) && temp == 0)) || ((((((((((((((((((((((-2147483647
        <= n && 1 <= right) && space <= 536870911) && right <= 1073741821) && (-2LL
        + (long long )right) + (long long )space >= 0LL) && (2147483646LL + (long
        long )n) + (long long )space >= 0LL) && (2147483646LL + (long long )n) + (long
        long )right >= 0LL) && (2147483647LL + (long long )right) + (long long )temp
        >= 0LL) && (4294967295LL + (long long )n) + (long long )temp >= 0LL) && (536870911LL
        - (long long )right) + (long long )space >= 0LL) && (2147483646LL - (long
        long )n) + (long long )right >= 0LL) && (2684354560LL - (long long )space)
        + (long long )temp >= 0LL) && (3221225471LL - (long long )right) + (long long
        )temp >= 0LL) && (2147483646LL + (long long )right) - (long long )temp >=
        0LL) && (2684354559LL + (long long )n) - (long long )space >= 0LL) && (3221225470LL
        + (long long )n) - (long long )right >= 0LL) && (4294967294LL + (long long
        )n) - (long long )temp >= 0LL) && (1610612735LL - (long long )right) - (long
        long )space >= 0LL) && (2684354559LL - (long long )n) - (long long )space
        >= 0LL) && (2684354559LL - (long long )space) - (long long )temp >= 0LL) &&
        (3221225470LL - (long long )n) - (long long )right >= 0LL) && (3221225470LL
        - (long long )right) - (long long )temp >= 0LL) && (long long )right - (long
        long )space >= 0LL)) || ((((((((((((((((((((((((6 <= left && 8 <= n) && 9
        <= right) && space <= 1073741823) && left <= 2147483645) && (-17LL + (long
        long )n) + (long long )right >= 0LL) && (-10LL + (long long )right) + (long
        long )space >= 0LL) && (-9LL + (long long )n) + (long long )space >= 0LL)
        && (2147483639LL + (long long )right) + (long long )temp >= 0LL) && (2147483640LL
        + (long long )n) + (long long )temp >= 0LL) && (2147483638LL - (long long
        )n) + (long long )right >= 0LL) && (2147483646LL - (long long )right) + (long
        long )space >= 0LL) && (3221225472LL - (long long )space) + (long long )temp
        >= 0LL) && (4294967295LL - (long long )right) + (long long )temp >= 0LL) &&
        (-8LL + (long long )right) - (long long )space >= 0LL) && (-7LL + (long long
        )n) - (long long )space >= 0LL) && (2147483638LL + (long long )right) - (long
        long )temp >= 0LL) && (2147483639LL + (long long )n) - (long long )right >=
        0LL) && (2147483639LL + (long long )n) - (long long )temp >= 0LL) && (3221225471LL
        - (long long )n) - (long long )space >= 0LL) && (3221225471LL - (long long
        )space) - (long long )temp >= 0LL) && (3221225471LL - (long long )right) -
        (long long )space >= 0LL) && (4294967294LL - (long long )n) - (long long )right
        >= 0LL) && (4294967294LL - (long long )right) - (long long )temp >= 0LL) &&
        temp == 0)) || ((((((((((((((((((((((((4 <= left && 6 <= n) && 7 <= right)
        && space <= 1073741823) && left <= 2147483645) && (-13LL + (long long )n)
        + (long long )right >= 0LL) && (-8LL + (long long )right) + (long long )space
        >= 0LL) && (-7LL + (long long )n) + (long long )space >= 0LL) && (2147483641LL
        + (long long )right) + (long long )temp >= 0LL) && (2147483642LL + (long long
        )n) + (long long )temp >= 0LL) && (2147483640LL - (long long )n) + (long long
        )right >= 0LL) && (2147483646LL - (long long )right) + (long long )space >=
        0LL) && (3221225472LL - (long long )space) + (long long )temp >= 0LL) && (4294967295LL
        - (long long )right) + (long long )temp >= 0LL) && (-6LL + (long long )right)
        - (long long )space >= 0LL) && (-5LL + (long long )n) - (long long )space
        >= 0LL) && (2147483640LL + (long long )right) - (long long )temp >= 0LL) &&
        (2147483641LL + (long long )n) - (long long )right >= 0LL) && (2147483641LL
        + (long long )n) - (long long )temp >= 0LL) && (3221225471LL - (long long
        )n) - (long long )space >= 0LL) && (3221225471LL - (long long )space) - (long
        long )temp >= 0LL) && (3221225471LL - (long long )right) - (long long )space
        >= 0LL) && (4294967294LL - (long long )n) - (long long )right >= 0LL) && (4294967294LL
        - (long long )right) - (long long )temp >= 0LL) && temp == 0)) || ((((((((((((((((((((((((2
        <= left && 4 <= n) && 5 <= right) && space <= 1073741823) && left <= 2147483645)
        && (-9LL + (long long )n) + (long long )right >= 0LL) && (-6LL + (long long
        )right) + (long long )space >= 0LL) && (-5LL + (long long )n) + (long long
        )space >= 0LL) && (2147483643LL + (long long )right) + (long long )temp >=
        0LL) && (2147483644LL + (long long )n) + (long long )temp >= 0LL) && (2147483642LL
        - (long long )n) + (long long )right >= 0LL) && (2147483646LL - (long long
        )right) + (long long )space >= 0LL) && (3221225472LL - (long long )space)
        + (long long )temp >= 0LL) && (4294967295LL - (long long )right) + (long long
        )temp >= 0LL) && (-4LL + (long long )right) - (long long )space >= 0LL) &&
        (-3LL + (long long )n) - (long long )space >= 0LL) && (2147483642LL + (long
        long )right) - (long long )temp >= 0LL) && (2147483643LL + (long long )n)
        - (long long )right >= 0LL) && (2147483643LL + (long long )n) - (long long
        )temp >= 0LL) && (3221225471LL - (long long )n) - (long long )space >= 0LL)
        && (3221225471LL - (long long )space) - (long long )temp >= 0LL) && (3221225471LL
        - (long long )right) - (long long )space >= 0LL) && (4294967294LL - (long
        long )n) - (long long )right >= 0LL) && (4294967294LL - (long long )right)
        - (long long )temp >= 0LL) && temp == 0)) || ((((((((((((((((((((((((6 <=
        left && 8 <= n) && 9 <= right) && space <= 67108863) && left <= 2147483645)
        && (-17LL + (long long )n) + (long long )right >= 0LL) && (-10LL + (long long
        )right) + (long long )space >= 0LL) && (-9LL + (long long )n) + (long long
        )space >= 0LL) && (2147483639LL + (long long )right) + (long long )temp >=
        0LL) && (2147483640LL + (long long )n) + (long long )temp >= 0LL) && (2147483638LL
        - (long long )n) + (long long )right >= 0LL) && (2147483646LL - (long long
        )right) + (long long )space >= 0LL) && (2214592512LL - (long long )space)
        + (long long )temp >= 0LL) && (4294967295LL - (long long )right) + (long long
        )temp >= 0LL) && (-8LL + (long long )right) - (long long )space >= 0LL) &&
        (-7LL + (long long )n) - (long long )space >= 0LL) && (134217727LL + (long
        long )n) - (long long )right >= 0LL) && (2147483638LL + (long long )right)
        - (long long )temp >= 0LL) && (2147483639LL + (long long )n) - (long long
        )temp >= 0LL) && (2214592511LL - (long long )n) - (long long )space >= 0LL)
        && (2214592511LL - (long long )space) - (long long )temp >= 0LL) && (2214592511LL
        - (long long )right) - (long long )space >= 0LL) && (4294967294LL - (long
        long )n) - (long long )right >= 0LL) && (4294967294LL - (long long )right)
        - (long long )temp >= 0LL) && temp == 0)) || ((((((((((((((((((((((((0 <=
        left && 2 <= n) && 3 <= right) && space <= 1073741823) && left <= 1073741823)
        && (-5LL + (long long )n) + (long long )right >= 0LL) && (-4LL + (long long
        )right) + (long long )space >= 0LL) && (-3LL + (long long )n) + (long long
        )space >= 0LL) && (2147483645LL + (long long )right) + (long long )temp >=
        0LL) && (2147483646LL + (long long )n) + (long long )temp >= 0LL) && (2147483644LL
        - (long long )n) + (long long )right >= 0LL) && (2147483646LL - (long long
        )right) + (long long )space >= 0LL) && (3221225472LL - (long long )space)
        + (long long )temp >= 0LL) && (4294967295LL - (long long )right) + (long long
        )temp >= 0LL) && (-2LL + (long long )right) - (long long )space >= 0LL) &&
        (-1LL + (long long )n) - (long long )space >= 0LL) && (2147483644LL + (long
        long )right) - (long long )temp >= 0LL) && (2147483645LL + (long long )n)
        - (long long )right >= 0LL) && (2147483645LL + (long long )n) - (long long
        )temp >= 0LL) && (3221225471LL - (long long )n) - (long long )space >= 0LL)
        && (3221225471LL - (long long )space) - (long long )temp >= 0LL) && (3221225471LL
        - (long long )right) - (long long )space >= 0LL) && (4294967294LL - (long
        long )n) - (long long )right >= 0LL) && (4294967294LL - (long long )right)
        - (long long )temp >= 0LL) && temp == 0)) || (((((((((((((((((((((((((4 <=
        left && 6 <= n) && 7 <= right) && space <= 67108863) && right <= 536870903)
        && left <= 335544319) && (-13LL + (long long )n) + (long long )right >= 0LL)
        && (-8LL + (long long )right) + (long long )space >= 0LL) && (-7LL + (long
        long )n) + (long long )space >= 0LL) && (2147483641LL + (long long )right)
        + (long long )temp >= 0LL) && (2147483642LL + (long long )n) + (long long
        )temp >= 0LL) && (469762047LL - (long long )right) + (long long )space >=
        0LL) && (2147483640LL - (long long )n) + (long long )right >= 0LL) && (2214592512LL
        - (long long )space) + (long long )temp >= 0LL) && (2684354559LL - (long long
        )right) + (long long )temp >= 0LL) && (-6LL + (long long )right) - (long long
        )space >= 0LL) && (-5LL + (long long )n) - (long long )space >= 0LL) && (134217727LL
        + (long long )n) - (long long )right >= 0LL) && (2147483640LL + (long long
        )right) - (long long )temp >= 0LL) && (2147483641LL + (long long )n) - (long
        long )temp >= 0LL) && (603979775LL - (long long )right) - (long long )space
        >= 0LL) && (2214592511LL - (long long )n) - (long long )space >= 0LL) && (2214592511LL
        - (long long )space) - (long long )temp >= 0LL) && (2684354558LL - (long long
        )n) - (long long )right >= 0LL) && (2684354558LL - (long long )right) - (long
        long )temp >= 0LL) && temp == 0)) || ((((((((((((((((((((((-2147483647 <=
        n && 1 <= right) && space <= 1073741823) && right <= 2147483645) && (-2LL
        + (long long )right) + (long long )space >= 0LL) && (2147483646LL + (long
        long )n) + (long long )space >= 0LL) && (2147483646LL + (long long )n) + (long
        long )right >= 0LL) && (2147483647LL + (long long )right) + (long long )temp
        >= 0LL) && (4294967295LL + (long long )n) + (long long )temp >= 0LL) && (1073741823LL
        - (long long )right) + (long long )space >= 0LL) && (2147483646LL - (long
        long )n) + (long long )right >= 0LL) && (3221225472LL - (long long )space)
        + (long long )temp >= 0LL) && (4294967295LL - (long long )right) + (long long
        )temp >= 0LL) && (2147483646LL + (long long )right) - (long long )temp >=
        0LL) && (3221225471LL + (long long )n) - (long long )space >= 0LL) && (4294967294LL
        + (long long )n) - (long long )right >= 0LL) && (4294967294LL + (long long
        )n) - (long long )temp >= 0LL) && (3221225471LL - (long long )n) - (long long
        )space >= 0LL) && (3221225471LL - (long long )space) - (long long )temp >=
        0LL) && (3221225471LL - (long long )right) - (long long )space >= 0LL) &&
        (4294967294LL - (long long )n) - (long long )right >= 0LL) && (4294967294LL
        - (long long )right) - (long long )temp >= 0LL) && (long long )right - (long
        long )space >= 0LL)) || (((((((((((((((((((((((((2 <= left && 4 <= n) && 5
        <= right) && space <= 67108863) && right <= 402653177) && left <= 201326591)
        && (-9LL + (long long )n) + (long long )right >= 0LL) && (-6LL + (long long
        )right) + (long long )space >= 0LL) && (-5LL + (long long )n) + (long long
        )space >= 0LL) && (2147483643LL + (long long )right) + (long long )temp >=
        0LL) && (2147483644LL + (long long )n) + (long long )temp >= 0LL) && (335544319LL
        - (long long )right) + (long long )space >= 0LL) && (2147483642LL - (long
        long )n) + (long long )right >= 0LL) && (2214592512LL - (long long )space)
        + (long long )temp >= 0LL) && (2550136831LL - (long long )right) + (long long
        )temp >= 0LL) && (-4LL + (long long )right) - (long long )space >= 0LL) &&
        (-3LL + (long long )n) - (long long )space >= 0LL) && (134217727LL + (long
        long )n) - (long long )right >= 0LL) && (2147483642LL + (long long )right)
        - (long long )temp >= 0LL) && (2147483643LL + (long long )n) - (long long
        )temp >= 0LL) && (469762047LL - (long long )right) - (long long )space >=
        0LL) && (2214592511LL - (long long )n) - (long long )space >= 0LL) && (2214592511LL
        - (long long )space) - (long long )temp >= 0LL) && (2550136830LL - (long long
        )n) - (long long )right >= 0LL) && (2550136830LL - (long long )right) - (long
        long )temp >= 0LL) && temp == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 69
        column: 5
        function: main
      value: (4294967295LL - (long long )n) + (long long )space >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 69
        column: 5
        function: main
      value: (4294967294LL - (long long )n) - (long long )space >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 69
        column: 5
        function: main
      value: ((0LL - (long long )i) + (long long )n >= 0LL && (((((((((((((4 <= n
        && 4 <= i) && (-8LL + (long long )i) + (long long )n >= 0LL) && (2147483644LL
        + (long long )n) + (long long )space >= 0LL) && (2147483644LL + (long long
        )i) + (long long )space >= 0LL) && (4294967295LL - (long long )i) + (long
        long )space >= 0LL) && (2147483643LL + (long long )n) - (long long )space
        >= 0LL) && (2147483643LL + (long long )i) - (long long )n >= 0LL) && (2147483643LL
        + (long long )i) - (long long )space >= 0LL) && (4294967294LL - (long long
        )i) - (long long )n >= 0LL) && (4294967294LL - (long long )i) - (long long
        )space >= 0LL) || ((((((((((3 <= n && (-6LL + (long long )i) + (long long
        )n >= 0LL) && (2147483645LL + (long long )n) + (long long )space >= 0LL) &&
        (2147483645LL + (long long )i) + (long long )space >= 0LL) && (2147483651LL
        - (long long )i) + (long long )space >= 0LL) && (2147483644LL + (long long
        )n) - (long long )space >= 0LL) && (2147483644LL + (long long )i) - (long
        long )n >= 0LL) && (2147483644LL + (long long )i) - (long long )space >= 0LL)
        && (2147483650LL - (long long )i) - (long long )n >= 0LL) && (2147483650LL
        - (long long )i) - (long long )space >= 0LL) && i == 3)) || ((((((((((2 <=
        n && (-4LL + (long long )i) + (long long )n >= 0LL) && (2147483646LL + (long
        long )n) + (long long )space >= 0LL) && (2147483646LL + (long long )i) + (long
        long )space >= 0LL) && (2147483650LL - (long long )i) + (long long )space
        >= 0LL) && (2147483645LL + (long long )n) - (long long )space >= 0LL) && (2147483645LL
        + (long long )i) - (long long )n >= 0LL) && (2147483645LL + (long long )i)
        - (long long )space >= 0LL) && (2147483649LL - (long long )i) - (long long
        )n >= 0LL) && (2147483649LL - (long long )i) - (long long )space >= 0LL) &&
        i == 2)) || ((((((((((1 <= n && (-2LL + (long long )i) + (long long )n >=
        0LL) && (2147483647LL + (long long )n) + (long long )space >= 0LL) && (2147483647LL
        + (long long )i) + (long long )space >= 0LL) && (2147483649LL - (long long
        )i) + (long long )space >= 0LL) && (2147483646LL + (long long )n) - (long
        long )space >= 0LL) && (2147483646LL + (long long )i) - (long long )n >= 0LL)
        && (2147483646LL + (long long )i) - (long long )space >= 0LL) && (2147483648LL
        - (long long )i) - (long long )n >= 0LL) && (2147483648LL - (long long )i)
        - (long long )space >= 0LL) && i == 1))) || ((((((((((((2147483647LL + (long
        long )i) + (long long )n >= 0LL && (2147483648LL + (long long )i) + (long
        long )space >= 0LL) && (4294967295LL + (long long )n) + (long long )space
        >= 0LL) && (2147483647LL - (long long )i) + (long long )n >= 0LL) && (2147483648LL
        - (long long )i) + (long long )space >= 0LL) && (2147483647LL + (long long
        )i) - (long long )n >= 0LL) && (2147483647LL + (long long )i) - (long long
        )space >= 0LL) && (4294967294LL + (long long )n) - (long long )space >= 0LL)
        && (2147483647LL - (long long )i) - (long long )n >= 0LL) && (2147483647LL
        - (long long )i) - (long long )space >= 0LL) && 0 == i) && i == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 33
        column: 5
        function: downsweep
      value: -2147483647 <= n
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 33
        column: 5
        function: downsweep
      value: 0 <= space
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 33
        column: 5
        function: downsweep
      value: (4294967295LL + (long long )n) + (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 33
        column: 5
        function: downsweep
      value: (4294967295LL - (long long )n) + (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 33
        column: 5
        function: downsweep
      value: (4294967295LL - (long long )right) + (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 33
        column: 5
        function: downsweep
      value: (4294967294LL + (long long )n) - (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 33
        column: 5
        function: downsweep
      value: (4294967294LL - (long long )n) - (long long )right >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 33
        column: 5
        function: downsweep
      value: (4294967294LL - (long long )n) - (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 33
        column: 5
        function: downsweep
      value: (4294967294LL - (long long )right) - (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 33
        column: 5
        function: downsweep
      value: ((((((((((((1 <= right && (-1LL + (long long )right) + (long long )space
        >= 0LL) && (2147483646LL + (long long )n) + (long long )right >= 0LL) && (2147483647LL
        + (long long )n) + (long long )space >= 0LL) && (2147483647LL + (long long
        )right) + (long long )temp >= 0LL) && (2147483648LL + (long long )space) +
        (long long )temp >= 0LL) && (0LL - (long long )n) + (long long )right >= 0LL)
        && (2147483647LL - (long long )n) + (long long )space >= 0LL) && (2147483647LL
        - (long long )right) + (long long )space >= 0LL) && (2147483646LL + (long
        long )right) - (long long )temp >= 0LL) && (2147483647LL + (long long )space)
        - (long long )temp >= 0LL) && right % 2 == 1) && ((((((((((space <= 67108863
        && (2214592512LL - (long long )space) + (long long )temp >= 0LL) && (67108863LL
        + (long long )right) - (long long )space >= 0LL) && (2214592511LL + (long
        long )n) - (long long )space >= 0LL) && (2415919102LL + (long long )n) - (long
        long )right >= 0LL) && (2214592511LL - (long long )n) - (long long )space
        >= 0LL) && (2214592511LL - (long long )space) - (long long )temp >= 0LL) &&
        (2214592511LL - (long long )right) - (long long )space >= 0LL) || (((((((space
        <= 134217727 && (2281701376LL - (long long )space) + (long long )temp >= 0LL)
        && (134217727LL + (long long )right) - (long long )space >= 0LL) && (2281701375LL
        + (long long )n) - (long long )space >= 0LL) && (2684354558LL + (long long
        )n) - (long long )right >= 0LL) && (2281701375LL - (long long )n) - (long
        long )space >= 0LL) && (2281701375LL - (long long )space) - (long long )temp
        >= 0LL) && (2281701375LL - (long long )right) - (long long )space >= 0LL))
        || (((((((space <= 268435455 && (2415919104LL - (long long )space) + (long
        long )temp >= 0LL) && (268435455LL + (long long )right) - (long long )space
        >= 0LL) && (2415919103LL + (long long )n) - (long long )space >= 0LL) && (3221225470LL
        + (long long )n) - (long long )right >= 0LL) && (2415919103LL - (long long
        )n) - (long long )space >= 0LL) && (2415919103LL - (long long )space) - (long
        long )temp >= 0LL) && (2415919103LL - (long long )right) - (long long )space
        >= 0LL)) || (((((((space <= 536870911 && (2684354560LL - (long long )space)
        + (long long )temp >= 0LL) && (536870911LL + (long long )right) - (long long
        )space >= 0LL) && (2684354559LL + (long long )n) - (long long )space >= 0LL)
        && (4294967294LL + (long long )n) - (long long )right >= 0LL) && (2684354559LL
        - (long long )n) - (long long )space >= 0LL) && (2684354559LL - (long long
        )space) - (long long )temp >= 0LL) && (2684354559LL - (long long )right) -
        (long long )space >= 0LL))) || (((((((((((((((((space <= 1073741823 && (3221225472LL
        + (long long )n) + (long long )space >= 0LL) && (3221225473LL + (long long
        )space) + (long long )temp >= 0LL) && (3221225473LL + (long long )right) +
        (long long )space >= 0LL) && (4294967295LL + (long long )n) + (long long )right
        >= 0LL) && (4294967296LL + (long long )right) + (long long )temp >= 0LL) &&
        (3221225472LL - (long long )n) + (long long )space >= 0LL) && (3221225472LL
        - (long long )space) + (long long )temp >= 0LL) && (3221225472LL - (long long
        )right) + (long long )space >= 0LL) && (4294967295LL - (long long )n) + (long
        long )right >= 0LL) && (3221225471LL + (long long )n) - (long long )space
        >= 0LL) && (3221225472LL + (long long )space) - (long long )temp >= 0LL) &&
        (3221225472LL + (long long )right) - (long long )space >= 0LL) && (4294967294LL
        + (long long )n) - (long long )right >= 0LL) && (4294967295LL + (long long
        )right) - (long long )temp >= 0LL) && (3221225471LL - (long long )n) - (long
        long )space >= 0LL) && (3221225471LL - (long long )space) - (long long )temp
        >= 0LL) && (3221225471LL - (long long )right) - (long long )space >= 0LL)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 20
        column: 9
        function: upsweep
      value: (((((((((((((((((((right % 16 == 15 && ((((((16 <= space && space <=
        2147483646) && (2147483631LL - (long long )n) + (long long )space >= 0LL)
        && space % 16 == 0) && left % 16 == 15) && ((((2147483631LL - (long long )left)
        + (long long )space >= 0LL && (4294967294LL - (long long )left) - (long long
        )n >= 0LL) && ((((((((((((((112 <= n && 127 <= right) && 143 <= left) && (-255LL
        + (long long )left) + (long long )n >= 0LL) && (-159LL + (long long )left)
        + (long long )space >= 0LL) && (-128LL + (long long )n) + (long long )space
        >= 0LL) && (2147483535LL - (long long )left) + (long long )n >= 0LL) && (-127LL
        + (long long )left) - (long long )space >= 0LL) && (-96LL + (long long )n)
        - (long long )space >= 0LL) && (2147483504LL + (long long )left) - (long long
        )n >= 0LL) && (4294967167LL - (long long )n) - (long long )space >= 0LL) &&
        (4294967167LL - (long long )left) - (long long )space >= 0LL) || (((((((((((80
        <= n && 95 <= right) && 111 <= left) && (-191LL + (long long )left) + (long
        long )n >= 0LL) && (-127LL + (long long )left) + (long long )space >= 0LL)
        && (-96LL + (long long )n) + (long long )space >= 0LL) && (2147483567LL -
        (long long )left) + (long long )n >= 0LL) && (-95LL + (long long )left) -
        (long long )space >= 0LL) && (-64LL + (long long )n) - (long long )space >=
        0LL) && (2147483536LL + (long long )left) - (long long )n >= 0LL) && (4294967199LL
        - (long long )n) - (long long )space >= 0LL) && (4294967199LL - (long long
        )left) - (long long )space >= 0LL)) || (((((((((((48 <= n && 63 <= right)
        && 79 <= left) && (-127LL + (long long )left) + (long long )n >= 0LL) && (-95LL
        + (long long )left) + (long long )space >= 0LL) && (-64LL + (long long )n)
        + (long long )space >= 0LL) && (2147483599LL - (long long )left) + (long long
        )n >= 0LL) && (-63LL + (long long )left) - (long long )space >= 0LL) && (-32LL
        + (long long )n) - (long long )space >= 0LL) && (2147483568LL + (long long
        )left) - (long long )n >= 0LL) && (4294967231LL - (long long )n) - (long long
        )space >= 0LL) && (4294967231LL - (long long )left) - (long long )space >=
        0LL)) || (((((((((((17 <= n && 31 <= right) && 47 <= left) && (-64LL + (long
        long )left) + (long long )n >= 0LL) && (-63LL + (long long )left) + (long
        long )space >= 0LL) && (-33LL + (long long )n) + (long long )space >= 0LL)
        && (2147483630LL - (long long )left) + (long long )n >= 0LL) && (-31LL + (long
        long )left) - (long long )space >= 0LL) && (-1LL + (long long )n) - (long
        long )space >= 0LL) && (2147483600LL + (long long )left) - (long long )n >=
        0LL) && (4294967263LL - (long long )n) - (long long )space >= 0LL) && (4294967263LL
        - (long long )left) - (long long )space >= 0LL))) || ((((((((((((((15 <= left
        && 15 <= right) && 17 <= n) && left <= 2147483645) && (-33LL + (long long
        )n) + (long long )space >= 0LL) && (-32LL + (long long )left) + (long long
        )n >= 0LL) && (-31LL + (long long )left) + (long long )space >= 0LL) && (-2LL
        - (long long )left) + (long long )n >= 0LL) && (-1LL - (long long )left) +
        (long long )space >= 0LL) && (-1LL + (long long )n) - (long long )space >=
        0LL) && (1LL + (long long )left) - (long long )space >= 0LL) && (2147483632LL
        + (long long )left) - (long long )n >= 0LL) && (4294967291LL - (long long
        )left) - (long long )space >= 0LL) && (4294967292LL - (long long )left) -
        (long long )n >= 0LL) && (4294967293LL - (long long )n) - (long long )space
        >= 0LL))) || ((((((((((((((((56 <= n && 63 <= right) && 71 <= left) && (-127LL
        + (long long )left) + (long long )n >= 0LL) && (-79LL + (long long )left)
        + (long long )space >= 0LL) && (-64LL + (long long )n) + (long long )space
        >= 0LL) && (15LL - (long long )left) + (long long )n >= 0LL) && (2147483639LL
        - (long long )n) + (long long )space >= 0LL) && (2147483639LL - (long long
        )left) + (long long )space >= 0LL) && (-63LL + (long long )left) - (long long
        )space >= 0LL) && (-48LL + (long long )n) - (long long )space >= 0LL) && (2147483576LL
        + (long long )left) - (long long )n >= 0LL) && (2147483655LL - (long long
        )n) - (long long )space >= 0LL) && (2147483655LL - (long long )left) - (long
        long )space >= 0LL) && (4294967294LL - (long long )left) - (long long )n >=
        0LL) && space == 8) && left % 16 == 7))) || (((((((((((((((40 <= n && (-95LL
        + (long long )left) + (long long )n >= 0LL) && (-63LL + (long long )left)
        + (long long )space >= 0LL) && (-48LL + (long long )n) + (long long )space
        >= 0LL) && (15LL - (long long )left) + (long long )n >= 0LL) && (47LL - (long
        long )left) + (long long )space >= 0LL) && (2147483639LL - (long long )n)
        + (long long )space >= 0LL) && (-47LL + (long long )left) - (long long )space
        >= 0LL) && (-32LL + (long long )n) - (long long )space >= 0LL) && (2147483592LL
        + (long long )left) - (long long )n >= 0LL) && (63LL - (long long )left) -
        (long long )space >= 0LL) && (2147483655LL - (long long )n) - (long long )space
        >= 0LL) && (2147483702LL - (long long )left) - (long long )n >= 0LL) && space
        == 8) && left == 55) && right == 47)) || (((((((((((((((24 <= n && (-63LL
        + (long long )left) + (long long )n >= 0LL) && (-47LL + (long long )left)
        + (long long )space >= 0LL) && (-32LL + (long long )n) + (long long )space
        >= 0LL) && (15LL - (long long )left) + (long long )n >= 0LL) && (31LL - (long
        long )left) + (long long )space >= 0LL) && (2147483639LL - (long long )n)
        + (long long )space >= 0LL) && (-31LL + (long long )left) - (long long )space
        >= 0LL) && (-16LL + (long long )n) - (long long )space >= 0LL) && (2147483608LL
        + (long long )left) - (long long )n >= 0LL) && (47LL - (long long )left) -
        (long long )space >= 0LL) && (2147483655LL - (long long )n) - (long long )space
        >= 0LL) && (2147483686LL - (long long )left) - (long long )n >= 0LL) && space
        == 8) && left == 39) && right == 31)) || (((((((((((((((9 <= n && (-32LL +
        (long long )left) + (long long )n >= 0LL) && (-31LL + (long long )left) +
        (long long )space >= 0LL) && (-17LL + (long long )n) + (long long )space >=
        0LL) && (14LL - (long long )left) + (long long )n >= 0LL) && (15LL - (long
        long )left) + (long long )space >= 0LL) && (2147483639LL - (long long )n)
        + (long long )space >= 0LL) && (-15LL + (long long )left) - (long long )space
        >= 0LL) && (-1LL + (long long )n) - (long long )space >= 0LL) && (2147483624LL
        + (long long )left) - (long long )n >= 0LL) && (31LL - (long long )left) -
        (long long )space >= 0LL) && (2147483655LL - (long long )n) - (long long )space
        >= 0LL) && (2147483670LL - (long long )left) - (long long )n >= 0LL) && space
        == 8) && left == 23) && right == 15)) || ((((((((((((((((7 <= right && 9 <=
        n) && (-17LL + (long long )n) + (long long )space >= 0LL) && (-16LL + (long
        long )left) + (long long )n >= 0LL) && (-15LL + (long long )left) + (long
        long )space >= 0LL) && (-2LL - (long long )left) + (long long )n >= 0LL) &&
        (-1LL - (long long )left) + (long long )space >= 0LL) && (2147483639LL - (long
        long )n) + (long long )space >= 0LL) && (-1LL + (long long )n) - (long long
        )space >= 0LL) && (1LL + (long long )left) - (long long )space >= 0LL) &&
        (2147483640LL + (long long )left) - (long long )n >= 0LL) && (15LL - (long
        long )left) - (long long )space >= 0LL) && (2147483654LL - (long long )left)
        - (long long )n >= 0LL) && (2147483655LL - (long long )n) - (long long )space
        >= 0LL) && space == 8) && left == 7) && right % 8 == 7)) || (((((((((((((((((28
        <= n && 31 <= right) && 35 <= left) && (-63LL + (long long )left) + (long
        long )n >= 0LL) && (-39LL + (long long )left) + (long long )space >= 0LL)
        && (-32LL + (long long )n) + (long long )space >= 0LL) && (7LL - (long long
        )left) + (long long )n >= 0LL) && (2147483643LL - (long long )n) + (long long
        )space >= 0LL) && (2147483643LL - (long long )left) + (long long )space >=
        0LL) && (-31LL + (long long )left) - (long long )space >= 0LL) && (-24LL +
        (long long )n) - (long long )space >= 0LL) && (2147483612LL + (long long )left)
        - (long long )n >= 0LL) && (2147483651LL - (long long )n) - (long long )space
        >= 0LL) && (2147483651LL - (long long )left) - (long long )space >= 0LL) &&
        (4294967294LL - (long long )left) - (long long )n >= 0LL) && space == 4) &&
        left % 8 == 3) && right % 8 == 7)) || (((((((((((((((20 <= n && (-47LL + (long
        long )left) + (long long )n >= 0LL) && (-31LL + (long long )left) + (long
        long )space >= 0LL) && (-24LL + (long long )n) + (long long )space >= 0LL)
        && (7LL - (long long )left) + (long long )n >= 0LL) && (23LL - (long long
        )left) + (long long )space >= 0LL) && (2147483643LL - (long long )n) + (long
        long )space >= 0LL) && (-23LL + (long long )left) - (long long )space >= 0LL)
        && (-16LL + (long long )n) - (long long )space >= 0LL) && (2147483620LL +
        (long long )left) - (long long )n >= 0LL) && (31LL - (long long )left) - (long
        long )space >= 0LL) && (2147483651LL - (long long )n) - (long long )space
        >= 0LL) && (2147483674LL - (long long )left) - (long long )n >= 0LL) && space
        == 4) && left == 27) && right == 23)) || (((((((((((((((12 <= n && (-31LL
        + (long long )left) + (long long )n >= 0LL) && (-23LL + (long long )left)
        + (long long )space >= 0LL) && (-16LL + (long long )n) + (long long )space
        >= 0LL) && (7LL - (long long )left) + (long long )n >= 0LL) && (15LL - (long
        long )left) + (long long )space >= 0LL) && (2147483643LL - (long long )n)
        + (long long )space >= 0LL) && (-15LL + (long long )left) - (long long )space
        >= 0LL) && (-8LL + (long long )n) - (long long )space >= 0LL) && (2147483628LL
        + (long long )left) - (long long )n >= 0LL) && (23LL - (long long )left) -
        (long long )space >= 0LL) && (2147483651LL - (long long )n) - (long long )space
        >= 0LL) && (2147483666LL - (long long )left) - (long long )n >= 0LL) && space
        == 4) && left == 19) && right == 15)) || (((((((((((((((5 <= n && (-16LL +
        (long long )left) + (long long )n >= 0LL) && (-15LL + (long long )left) +
        (long long )space >= 0LL) && (-9LL + (long long )n) + (long long )space >=
        0LL) && (6LL - (long long )left) + (long long )n >= 0LL) && (7LL - (long long
        )left) + (long long )space >= 0LL) && (2147483643LL - (long long )n) + (long
        long )space >= 0LL) && (-7LL + (long long )left) - (long long )space >= 0LL)
        && (-1LL + (long long )n) - (long long )space >= 0LL) && (2147483636LL + (long
        long )left) - (long long )n >= 0LL) && (15LL - (long long )left) - (long long
        )space >= 0LL) && (2147483651LL - (long long )n) - (long long )space >= 0LL)
        && (2147483658LL - (long long )left) - (long long )n >= 0LL) && space == 4)
        && left == 11) && right == 7)) || ((((((((((((((((3 <= right && 5 <= n) &&
        (-9LL + (long long )n) + (long long )space >= 0LL) && (-8LL + (long long )left)
        + (long long )n >= 0LL) && (-7LL + (long long )left) + (long long )space >=
        0LL) && (-2LL - (long long )left) + (long long )n >= 0LL) && (-1LL - (long
        long )left) + (long long )space >= 0LL) && (2147483643LL - (long long )n)
        + (long long )space >= 0LL) && (-1LL + (long long )n) - (long long )space
        >= 0LL) && (1LL + (long long )left) - (long long )space >= 0LL) && (2147483644LL
        + (long long )left) - (long long )n >= 0LL) && (7LL - (long long )left) -
        (long long )space >= 0LL) && (2147483650LL - (long long )left) - (long long
        )n >= 0LL) && (2147483651LL - (long long )n) - (long long )space >= 0LL) &&
        space == 4) && left == 3) && right % 4 == 3)) || (((((((((((((((((14 <= n
        && 15 <= right) && 17 <= left) && (-31LL + (long long )left) + (long long
        )n >= 0LL) && (-19LL + (long long )left) + (long long )space >= 0LL) && (-16LL
        + (long long )n) + (long long )space >= 0LL) && (3LL - (long long )left) +
        (long long )n >= 0LL) && (2147483645LL - (long long )n) + (long long )space
        >= 0LL) && (2147483645LL - (long long )left) + (long long )space >= 0LL) &&
        (-15LL + (long long )left) - (long long )space >= 0LL) && (-12LL + (long long
        )n) - (long long )space >= 0LL) && (2147483630LL + (long long )left) - (long
        long )n >= 0LL) && (2147483649LL - (long long )n) - (long long )space >= 0LL)
        && (2147483649LL - (long long )left) - (long long )space >= 0LL) && (4294967294LL
        - (long long )left) - (long long )n >= 0LL) && space == 2) && left % 4 ==
        1) && right % 4 == 3)) || (((((((((((((((10 <= n && (-23LL + (long long )left)
        + (long long )n >= 0LL) && (-15LL + (long long )left) + (long long )space
        >= 0LL) && (-12LL + (long long )n) + (long long )space >= 0LL) && (3LL - (long
        long )left) + (long long )n >= 0LL) && (11LL - (long long )left) + (long long
        )space >= 0LL) && (2147483645LL - (long long )n) + (long long )space >= 0LL)
        && (-11LL + (long long )left) - (long long )space >= 0LL) && (-8LL + (long
        long )n) - (long long )space >= 0LL) && (2147483634LL + (long long )left)
        - (long long )n >= 0LL) && (15LL - (long long )left) - (long long )space >=
        0LL) && (2147483649LL - (long long )n) - (long long )space >= 0LL) && (2147483660LL
        - (long long )left) - (long long )n >= 0LL) && space == 2) && left == 13)
        && right == 11)) || (((((((((((((((6 <= n && (-15LL + (long long )left) +
        (long long )n >= 0LL) && (-11LL + (long long )left) + (long long )space >=
        0LL) && (-8LL + (long long )n) + (long long )space >= 0LL) && (3LL - (long
        long )left) + (long long )n >= 0LL) && (7LL - (long long )left) + (long long
        )space >= 0LL) && (2147483645LL - (long long )n) + (long long )space >= 0LL)
        && (-7LL + (long long )left) - (long long )space >= 0LL) && (-4LL + (long
        long )n) - (long long )space >= 0LL) && (2147483638LL + (long long )left)
        - (long long )n >= 0LL) && (11LL - (long long )left) - (long long )space >=
        0LL) && (2147483649LL - (long long )n) - (long long )space >= 0LL) && (2147483656LL
        - (long long )left) - (long long )n >= 0LL) && space == 2) && left == 9) &&
        right == 7)) || (((((((((((((((3 <= n && (-8LL + (long long )left) + (long
        long )n >= 0LL) && (-7LL + (long long )left) + (long long )space >= 0LL) &&
        (-5LL + (long long )n) + (long long )space >= 0LL) && (2LL - (long long )left)
        + (long long )n >= 0LL) && (3LL - (long long )left) + (long long )space >=
        0LL) && (2147483645LL - (long long )n) + (long long )space >= 0LL) && (-3LL
        + (long long )left) - (long long )space >= 0LL) && (-1LL + (long long )n)
        - (long long )space >= 0LL) && (2147483642LL + (long long )left) - (long long
        )n >= 0LL) && (7LL - (long long )left) - (long long )space >= 0LL) && (2147483649LL
        - (long long )n) - (long long )space >= 0LL) && (2147483652LL - (long long
        )left) - (long long )n >= 0LL) && space == 2) && left == 5) && right == 3))
        || ((((((((((((((((1 <= right && 3 <= n) && (-5LL + (long long )n) + (long
        long )space >= 0LL) && (-4LL + (long long )left) + (long long )n >= 0LL) &&
        (-3LL + (long long )left) + (long long )space >= 0LL) && (-2LL - (long long
        )left) + (long long )n >= 0LL) && (-1LL - (long long )left) + (long long )space
        >= 0LL) && (2147483645LL - (long long )n) + (long long )space >= 0LL) && (-1LL
        + (long long )n) - (long long )space >= 0LL) && (1LL + (long long )left) -
        (long long )space >= 0LL) && (2147483646LL + (long long )left) - (long long
        )n >= 0LL) && (3LL - (long long )left) - (long long )space >= 0LL) && (2147483648LL
        - (long long )left) - (long long )n >= 0LL) && (2147483649LL - (long long
        )n) - (long long )space >= 0LL) && space == 2) && left == 1) && right % 2
        == 1)) || ((((((((((((((((((7 <= n && 7 <= right) && 8 <= left) && (-15LL
        + (long long )left) + (long long )n >= 0LL) && (-9LL + (long long )left) +
        (long long )space >= 0LL) && (-8LL + (long long )n) + (long long )space >=
        0LL) && (1LL - (long long )left) + (long long )n >= 0LL) && (2147483646LL
        - (long long )n) + (long long )space >= 0LL) && (2147483646LL - (long long
        )left) + (long long )space >= 0LL) && (-7LL + (long long )left) - (long long
        )space >= 0LL) && (-6LL + (long long )n) - (long long )space >= 0LL) && (2147483639LL
        + (long long )left) - (long long )n >= 0LL) && (2147483648LL - (long long
        )n) - (long long )space >= 0LL) && (2147483648LL - (long long )left) - (long
        long )space >= 0LL) && (4294967294LL - (long long )left) - (long long )n >=
        0LL) && 1 == space) && space == 1) && left % 2 == 0) && right % 2 == 1)) ||
        ((((((((((((((((5 <= n && (-11LL + (long long )left) + (long long )n >= 0LL)
        && (-7LL + (long long )left) + (long long )space >= 0LL) && (-6LL + (long
        long )n) + (long long )space >= 0LL) && (1LL - (long long )left) + (long long
        )n >= 0LL) && (5LL - (long long )left) + (long long )space >= 0LL) && (2147483646LL
        - (long long )n) + (long long )space >= 0LL) && (-5LL + (long long )left)
        - (long long )space >= 0LL) && (-4LL + (long long )n) - (long long )space
        >= 0LL) && (2147483641LL + (long long )left) - (long long )n >= 0LL) && (7LL
        - (long long )left) - (long long )space >= 0LL) && (2147483648LL - (long long
        )n) - (long long )space >= 0LL) && (2147483653LL - (long long )left) - (long
        long )n >= 0LL) && 1 == space) && space == 1) && left == 6) && right == 5))
        || ((((((((((((((((3 <= n && (-7LL + (long long )left) + (long long )n >=
        0LL) && (-5LL + (long long )left) + (long long )space >= 0LL) && (-4LL + (long
        long )n) + (long long )space >= 0LL) && (1LL - (long long )left) + (long long
        )n >= 0LL) && (3LL - (long long )left) + (long long )space >= 0LL) && (2147483646LL
        - (long long )n) + (long long )space >= 0LL) && (-3LL + (long long )left)
        - (long long )space >= 0LL) && (-2LL + (long long )n) - (long long )space
        >= 0LL) && (2147483643LL + (long long )left) - (long long )n >= 0LL) && (5LL
        - (long long )left) - (long long )space >= 0LL) && (2147483648LL - (long long
        )n) - (long long )space >= 0LL) && (2147483651LL - (long long )left) - (long
        long )n >= 0LL) && 1 == space) && space == 1) && left == 4) && right == 3))
        || ((((((((((((((((2 <= n && (-4LL + (long long )left) + (long long )n >=
        0LL) && (-3LL + (long long )n) + (long long )space >= 0LL) && (-3LL + (long
        long )left) + (long long )space >= 0LL) && (0LL - (long long )left) + (long
        long )n >= 0LL) && (1LL - (long long )left) + (long long )space >= 0LL) &&
        (2147483646LL - (long long )n) + (long long )space >= 0LL) && (-1LL + (long
        long )n) - (long long )space >= 0LL) && (-1LL + (long long )left) - (long
        long )space >= 0LL) && (2147483645LL + (long long )left) - (long long )n >=
        0LL) && (3LL - (long long )left) - (long long )space >= 0LL) && (2147483648LL
        - (long long )n) - (long long )space >= 0LL) && (2147483649LL - (long long
        )left) - (long long )n >= 0LL) && 1 == space) && space == 1) && left == 2)
        && right == 1)) || (((((((((((((((2 <= n && (-3LL + (long long )n) + (long
        long )space >= 0LL) && (-2LL + (long long )left) + (long long )n >= 0LL) &&
        (-1LL + (long long )left) + (long long )space >= 0LL) && (-2LL - (long long
        )left) + (long long )n >= 0LL) && (-1LL - (long long )left) + (long long )space
        >= 0LL) && (2147483646LL - (long long )n) + (long long )space >= 0LL) && (-1LL
        + (long long )n) - (long long )space >= 0LL) && (1LL + (long long )left) -
        (long long )space >= 0LL) && (2147483647LL + (long long )left) - (long long
        )n >= 0LL) && (1LL - (long long )left) - (long long )space >= 0LL) && (2147483647LL
        - (long long )left) - (long long )n >= 0LL) && (2147483648LL - (long long
        )n) - (long long )space >= 0LL) && 1 == space) && space == 1) && left == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 18
        column: 5
        function: upsweep
      value: (4294967294LL - (long long )left) - (long long )n >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/verifythis/prefixsum_iter.c
        line: 18
        column: 5
        function: upsweep
      value: ((long long )left - (long long )n >= 0LL && (((((((((((((((((((9 <= n
        && 15 <= right) && 16 <= space) && 23 <= left) && (-39LL + (long long )left)
        + (long long )space >= 0LL) && (-32LL + (long long )left) + (long long )n
        >= 0LL) && (-25LL + (long long )n) + (long long )space >= 0LL) && (2147483630LL
        - (long long )left) + (long long )n >= 0LL) && (2147483631LL - (long long
        )n) + (long long )space >= 0LL) && (2147483631LL - (long long )left) + (long
        long )space >= 0LL) && (2147483585LL + (long long )left) - (long long )space
        >= 0LL) && (2147483615LL + (long long )n) - (long long )space >= 0LL) && (4294967294LL
        - (long long )n) - (long long )space >= 0LL) && (4294967294LL - (long long
        )left) - (long long )space >= 0LL) && space % 16 == 0) && left % 8 == 7) &&
        right % 16 == 15) || (((((((((((((((5 <= n && 7 <= right) && 11 <= left) &&
        (-19LL + (long long )left) + (long long )space >= 0LL) && (-16LL + (long long
        )left) + (long long )n >= 0LL) && (-13LL + (long long )n) + (long long )space
        >= 0LL) && (7LL - (long long )left) + (long long )n >= 0LL) && (2147483639LL
        - (long long )n) + (long long )space >= 0LL) && (2147483639LL - (long long
        )left) + (long long )space >= 0LL) && (-3LL + (long long )left) - (long long
        )space >= 0LL) && (3LL + (long long )n) - (long long )space >= 0LL) && (2147483655LL
        - (long long )n) - (long long )space >= 0LL) && (2147483655LL - (long long
        )left) - (long long )space >= 0LL) && space == 8) && left % 8 == 3) && right
        % 8 == 7)) || (((((((((((((((3 <= n && 3 <= right) && 5 <= left) && (-9LL
        + (long long )left) + (long long )space >= 0LL) && (-8LL + (long long )left)
        + (long long )n >= 0LL) && (-7LL + (long long )n) + (long long )space >= 0LL)
        && (3LL - (long long )left) + (long long )n >= 0LL) && (2147483643LL - (long
        long )n) + (long long )space >= 0LL) && (2147483643LL - (long long )left)
        + (long long )space >= 0LL) && (-1LL + (long long )left) - (long long )space
        >= 0LL) && (1LL + (long long )n) - (long long )space >= 0LL) && (2147483651LL
        - (long long )n) - (long long )space >= 0LL) && (2147483651LL - (long long
        )left) - (long long )space >= 0LL) && space == 4) && left % 4 == 1) && right
        % 4 == 3)) || (((((((((((((((1 <= right && 2 <= n) && 2 <= left) && (-4LL
        + (long long )n) + (long long )space >= 0LL) && (-4LL + (long long )left)
        + (long long )n >= 0LL) && (-4LL + (long long )left) + (long long )space >=
        0LL) && (1LL - (long long )left) + (long long )n >= 0LL) && (2147483645LL
        - (long long )n) + (long long )space >= 0LL) && (2147483645LL - (long long
        )left) + (long long )space >= 0LL) && (2147483649LL - (long long )n) - (long
        long )space >= 0LL) && (2147483649LL - (long long )left) - (long long )space
        >= 0LL) && (long long )n - (long long )space >= 0LL) && (long long )left -
        (long long )space >= 0LL) && space == 2) && left % 2 == 0) && right % 2 ==
        1))) || (((((((((((((-2147483647 <= n && (2147483646LL + (long long )n) +
        (long long )space >= 0LL) && (2147483647LL + (long long )left) + (long long
        )space >= 0LL) && (4294967295LL + (long long )left) + (long long )n >= 0LL)
        && (2147483646LL - (long long )n) + (long long )space >= 0LL) && (2147483646LL
        - (long long )left) + (long long )space >= 0LL) && (4294967294LL - (long long
        )left) + (long long )n >= 0LL) && (2147483648LL + (long long )n) - (long long
        )space >= 0LL) && (2147483649LL + (long long )left) - (long long )space >=
        0LL) && (4294967295LL + (long long )left) - (long long )n >= 0LL) && (2147483648LL
        - (long long )n) - (long long )space >= 0LL) && (2147483648LL - (long long
        )left) - (long long )space >= 0LL) && 1 == space) && space == 1)
      format: c_expression
