- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: eadf181a-588d-4294-8fc7-1c8c52dd1309
    creation_time: 2025-03-21T01:25:16Z
    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/loops/bubble_sort-1.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c: 121046493a5b65b32f3b8bf8adee655ff03b45acd38f0a8519ee3c99065fa840
      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/loops/bubble_sort-1.c
        line: 20
        column: 3
        function: bubblesort
      value: (4294967295LL - (long long )size) + (long long )t >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 20
        column: 3
        function: bubblesort
      value: (4294967294LL - (long long )size) - (long long )t >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 20
        column: 3
        function: bubblesort
      value: (((((((((((((((((((((((((((((((((((((((((((((((((((1LL - (long long )a)
        + (long long )b >= 0LL && ((((((((((((2 <= b && (-5LL + (long long )a) + (long
        long )b >= 0LL) && (2147483645LL + (long long )a) + (long long )t >= 0LL)
        && (2147483646LL + (long long )b) + (long long )t >= 0LL) && (2147483651LL
        - (long long )a) + (long long )t >= 0LL) && (2147483644LL + (long long )a)
        - (long long )size >= 0LL) && (2147483644LL + (long long )a) - (long long
        )t >= 0LL) && (2147483645LL + (long long )b) - (long long )t >= 0LL) && (2147483650LL
        - (long long )a) - (long long )size >= 0LL) && (2147483650LL - (long long
        )a) - (long long )t >= 0LL) && a == 3) && (((((((((((((((((((((12 <= size
        && b <= 2147483637) && (-15LL + (long long )a) + (long long )size >= 0LL)
        && (-14LL + (long long )b) + (long long )size >= 0LL) && (2147483636LL + (long
        long )size) + (long long )t >= 0LL) && (-10LL - (long long )b) + (long long
        )size >= 0LL) && (-9LL - (long long )a) + (long long )size >= 0LL) && (4294967285LL
        - (long long )b) + (long long )t >= 0LL) && (10LL + (long long )b) - (long
        long )size >= 0LL) && (2147483634LL + (long long )a) - (long long )b >= 0LL)
        && (2147483635LL + (long long )size) - (long long )t >= 0LL) && (2147483640LL
        - (long long )a) - (long long )b >= 0LL) && (4294967284LL - (long long )b)
        - (long long )size >= 0LL) && (4294967284LL - (long long )b) - (long long
        )t >= 0LL) || (((((((((((((11 <= size && b <= 2147483638) && (-14LL + (long
        long )a) + (long long )size >= 0LL) && (-13LL + (long long )b) + (long long
        )size >= 0LL) && (2147483637LL + (long long )size) + (long long )t >= 0LL)
        && (-9LL - (long long )b) + (long long )size >= 0LL) && (-8LL - (long long
        )a) + (long long )size >= 0LL) && (4294967286LL - (long long )b) + (long long
        )t >= 0LL) && (9LL + (long long )b) - (long long )size >= 0LL) && (2147483635LL
        + (long long )a) - (long long )b >= 0LL) && (2147483636LL + (long long )size)
        - (long long )t >= 0LL) && (2147483641LL - (long long )a) - (long long )b
        >= 0LL) && (4294967285LL - (long long )b) - (long long )size >= 0LL) && (4294967285LL
        - (long long )b) - (long long )t >= 0LL)) || (((((((((((((10 <= size && b
        <= 2147483639) && (-13LL + (long long )a) + (long long )size >= 0LL) && (-12LL
        + (long long )b) + (long long )size >= 0LL) && (2147483638LL + (long long
        )size) + (long long )t >= 0LL) && (-8LL - (long long )b) + (long long )size
        >= 0LL) && (-7LL - (long long )a) + (long long )size >= 0LL) && (4294967287LL
        - (long long )b) + (long long )t >= 0LL) && (8LL + (long long )b) - (long
        long )size >= 0LL) && (2147483636LL + (long long )a) - (long long )b >= 0LL)
        && (2147483637LL + (long long )size) - (long long )t >= 0LL) && (2147483642LL
        - (long long )a) - (long long )b >= 0LL) && (4294967286LL - (long long )b)
        - (long long )size >= 0LL) && (4294967286LL - (long long )b) - (long long
        )t >= 0LL)) || (((((((((((((9 <= size && b <= 2147483640) && (-12LL + (long
        long )a) + (long long )size >= 0LL) && (-11LL + (long long )b) + (long long
        )size >= 0LL) && (2147483639LL + (long long )size) + (long long )t >= 0LL)
        && (-7LL - (long long )b) + (long long )size >= 0LL) && (-6LL - (long long
        )a) + (long long )size >= 0LL) && (4294967288LL - (long long )b) + (long long
        )t >= 0LL) && (7LL + (long long )b) - (long long )size >= 0LL) && (2147483637LL
        + (long long )a) - (long long )b >= 0LL) && (2147483638LL + (long long )size)
        - (long long )t >= 0LL) && (2147483643LL - (long long )a) - (long long )b
        >= 0LL) && (4294967287LL - (long long )b) - (long long )size >= 0LL) && (4294967287LL
        - (long long )b) - (long long )t >= 0LL)) || (((((((((((((8 <= size && b <=
        2147483641) && (-11LL + (long long )a) + (long long )size >= 0LL) && (-10LL
        + (long long )b) + (long long )size >= 0LL) && (2147483640LL + (long long
        )size) + (long long )t >= 0LL) && (-6LL - (long long )b) + (long long )size
        >= 0LL) && (-5LL - (long long )a) + (long long )size >= 0LL) && (4294967289LL
        - (long long )b) + (long long )t >= 0LL) && (6LL + (long long )b) - (long
        long )size >= 0LL) && (2147483638LL + (long long )a) - (long long )b >= 0LL)
        && (2147483639LL + (long long )size) - (long long )t >= 0LL) && (2147483644LL
        - (long long )a) - (long long )b >= 0LL) && (4294967288LL - (long long )b)
        - (long long )size >= 0LL) && (4294967288LL - (long long )b) - (long long
        )t >= 0LL)) || (((((((((((((7 <= size && b <= 2147483642) && (-10LL + (long
        long )a) + (long long )size >= 0LL) && (-9LL + (long long )b) + (long long
        )size >= 0LL) && (2147483641LL + (long long )size) + (long long )t >= 0LL)
        && (-5LL - (long long )b) + (long long )size >= 0LL) && (-4LL - (long long
        )a) + (long long )size >= 0LL) && (4294967290LL - (long long )b) + (long long
        )t >= 0LL) && (5LL + (long long )b) - (long long )size >= 0LL) && (2147483639LL
        + (long long )a) - (long long )b >= 0LL) && (2147483640LL + (long long )size)
        - (long long )t >= 0LL) && (2147483645LL - (long long )a) - (long long )b
        >= 0LL) && (4294967289LL - (long long )b) - (long long )size >= 0LL) && (4294967289LL
        - (long long )b) - (long long )t >= 0LL)) || (((((((((((((6 <= size && b <=
        2147483643) && (-9LL + (long long )a) + (long long )size >= 0LL) && (-8LL
        + (long long )b) + (long long )size >= 0LL) && (2147483642LL + (long long
        )size) + (long long )t >= 0LL) && (-4LL - (long long )b) + (long long )size
        >= 0LL) && (-3LL - (long long )a) + (long long )size >= 0LL) && (4294967291LL
        - (long long )b) + (long long )t >= 0LL) && (4LL + (long long )b) - (long
        long )size >= 0LL) && (2147483640LL + (long long )a) - (long long )b >= 0LL)
        && (2147483641LL + (long long )size) - (long long )t >= 0LL) && (2147483646LL
        - (long long )a) - (long long )b >= 0LL) && (4294967290LL - (long long )b)
        - (long long )size >= 0LL) && (4294967290LL - (long long )b) - (long long
        )t >= 0LL)) || (((((((((((((5 <= size && b <= 2147483644) && (-8LL + (long
        long )a) + (long long )size >= 0LL) && (-7LL + (long long )b) + (long long
        )size >= 0LL) && (2147483643LL + (long long )size) + (long long )t >= 0LL)
        && (-3LL - (long long )b) + (long long )size >= 0LL) && (-2LL - (long long
        )a) + (long long )size >= 0LL) && (4294967292LL - (long long )b) + (long long
        )t >= 0LL) && (3LL + (long long )b) - (long long )size >= 0LL) && (2147483641LL
        + (long long )a) - (long long )b >= 0LL) && (2147483642LL + (long long )size)
        - (long long )t >= 0LL) && (2147483647LL - (long long )a) - (long long )b
        >= 0LL) && (4294967291LL - (long long )b) - (long long )size >= 0LL) && (4294967291LL
        - (long long )b) - (long long )t >= 0LL)) || (((((((((((((4 <= size && b <=
        2147483645) && (-7LL + (long long )a) + (long long )size >= 0LL) && (-6LL
        + (long long )b) + (long long )size >= 0LL) && (2147483644LL + (long long
        )size) + (long long )t >= 0LL) && (-2LL - (long long )b) + (long long )size
        >= 0LL) && (-1LL - (long long )a) + (long long )size >= 0LL) && (4294967293LL
        - (long long )b) + (long long )t >= 0LL) && (2LL + (long long )b) - (long
        long )size >= 0LL) && (2147483642LL + (long long )a) - (long long )b >= 0LL)
        && (2147483643LL + (long long )size) - (long long )t >= 0LL) && (2147483648LL
        - (long long )a) - (long long )b >= 0LL) && (4294967292LL - (long long )b)
        - (long long )size >= 0LL) && (4294967292LL - (long long )b) - (long long
        )t >= 0LL))) || (((((((((((((((((((((((((4 <= b && 5 <= a) && 16 <= size)
        && a <= 2147483636) && b <= 2147483635) && (-21LL + (long long )a) + (long
        long )size >= 0LL) && (-20LL + (long long )b) + (long long )size >= 0LL) &&
        (-9LL + (long long )a) + (long long )b >= 0LL) && (2147483632LL + (long long
        )size) + (long long )t >= 0LL) && (2147483643LL + (long long )a) + (long long
        )t >= 0LL) && (2147483644LL + (long long )b) + (long long )t >= 0LL) && (-12LL
        - (long long )b) + (long long )size >= 0LL) && (-11LL - (long long )a) + (long
        long )size >= 0LL) && (4294967283LL - (long long )b) + (long long )t >= 0LL)
        && (4294967284LL - (long long )a) + (long long )t >= 0LL) && (2147483630LL
        + (long long )a) - (long long )b >= 0LL) && (2147483631LL + (long long )size)
        - (long long )t >= 0LL) && (2147483642LL + (long long )a) - (long long )size
        >= 0LL) && (2147483642LL + (long long )a) - (long long )t >= 0LL) && (2147483643LL
        + (long long )b) - (long long )size >= 0LL) && (2147483643LL + (long long
        )b) - (long long )t >= 0LL) && (4294967271LL - (long long )a) - (long long
        )b >= 0LL) && (4294967282LL - (long long )b) - (long long )size >= 0LL) &&
        (4294967282LL - (long long )b) - (long long )t >= 0LL) && (4294967283LL -
        (long long )a) - (long long )size >= 0LL) && (4294967283LL - (long long )a)
        - (long long )t >= 0LL))) || (((((((((((((((((((((((((3 <= b && 4 <= size)
        && b <= 2147483646) && (-7LL + (long long )a) + (long long )size >= 0LL) &&
        (-7LL + (long long )b) + (long long )size >= 0LL) && (-6LL + (long long )a)
        + (long long )b >= 0LL) && (2147483644LL + (long long )size) + (long long
        )t >= 0LL) && (2147483645LL + (long long )a) + (long long )t >= 0LL) && (2147483645LL
        + (long long )b) + (long long )t >= 0LL) && (-1LL - (long long )a) + (long
        long )size >= 0LL) && (-1LL - (long long )b) + (long long )size >= 0LL) &&
        (0LL - (long long )a) + (long long )b >= 0LL) && (2147483651LL - (long long
        )a) + (long long )t >= 0LL) && (4294967294LL - (long long )b) + (long long
        )t >= 0LL) && (1LL + (long long )b) - (long long )size >= 0LL) && (2147483643LL
        + (long long )size) - (long long )t >= 0LL) && (2147483643LL + (long long
        )a) - (long long )b >= 0LL) && (2147483644LL + (long long )a) - (long long
        )size >= 0LL) && (2147483644LL + (long long )a) - (long long )t >= 0LL) &&
        (2147483644LL + (long long )b) - (long long )t >= 0LL) && (2147483649LL -
        (long long )a) - (long long )b >= 0LL) && (2147483650LL - (long long )a) -
        (long long )size >= 0LL) && (2147483650LL - (long long )a) - (long long )t
        >= 0LL) && (4294967293LL - (long long )b) - (long long )size >= 0LL) && (4294967293LL
        - (long long )b) - (long long )t >= 0LL) && a == 3)) || ((((((((((((((((((((((((((4
        <= b && 5 <= a) && 15 <= size) && a <= 2147483637) && b <= 2147483636) &&
        (-20LL + (long long )a) + (long long )size >= 0LL) && (-19LL + (long long
        )b) + (long long )size >= 0LL) && (-9LL + (long long )a) + (long long )b >=
        0LL) && (2147483633LL + (long long )size) + (long long )t >= 0LL) && (2147483643LL
        + (long long )a) + (long long )t >= 0LL) && (2147483644LL + (long long )b)
        + (long long )t >= 0LL) && (-11LL - (long long )b) + (long long )size >= 0LL)
        && (-10LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (4294967284LL - (long long )b) + (long long
        )t >= 0LL) && (4294967285LL - (long long )a) + (long long )t >= 0LL) && (11LL
        + (long long )b) - (long long )size >= 0LL) && (2147483631LL + (long long
        )a) - (long long )b >= 0LL) && (2147483632LL + (long long )size) - (long long
        )t >= 0LL) && (2147483642LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483642LL + (long long )a) - (long long )t >= 0LL) && (2147483643LL +
        (long long )b) - (long long )t >= 0LL) && (4294967273LL - (long long )a) -
        (long long )b >= 0LL) && (4294967283LL - (long long )b) - (long long )size
        >= 0LL) && (4294967283LL - (long long )b) - (long long )t >= 0LL) && (4294967284LL
        - (long long )a) - (long long )size >= 0LL) && (4294967284LL - (long long
        )a) - (long long )t >= 0LL)) || (((((((((((((((((((((((((1 <= b && 13 <= size)
        && b <= 2147483635) && (-15LL + (long long )a) + (long long )size >= 0LL)
        && (-14LL + (long long )b) + (long long )size >= 0LL) && (-3LL + (long long
        )a) + (long long )b >= 0LL) && (2147483635LL + (long long )size) + (long long
        )t >= 0LL) && (2147483646LL + (long long )a) + (long long )t >= 0LL) && (2147483647LL
        + (long long )b) + (long long )t >= 0LL) && (-12LL - (long long )b) + (long
        long )size >= 0LL) && (-11LL - (long long )a) + (long long )size >= 0LL) &&
        (1LL - (long long )a) + (long long )b >= 0LL) && (2147483650LL - (long long
        )a) + (long long )t >= 0LL) && (4294967283LL - (long long )b) + (long long
        )t >= 0LL) && (2147483633LL + (long long )a) - (long long )b >= 0LL) && (2147483634LL
        + (long long )size) - (long long )t >= 0LL) && (2147483645LL + (long long
        )a) - (long long )size >= 0LL) && (2147483645LL + (long long )a) - (long long
        )t >= 0LL) && (2147483646LL + (long long )b) - (long long )size >= 0LL) &&
        (2147483646LL + (long long )b) - (long long )t >= 0LL) && (2147483637LL -
        (long long )a) - (long long )b >= 0LL) && (2147483649LL - (long long )a) -
        (long long )size >= 0LL) && (2147483649LL - (long long )a) - (long long )t
        >= 0LL) && (4294967282LL - (long long )b) - (long long )size >= 0LL) && (4294967282LL
        - (long long )b) - (long long )t >= 0LL) && a == 2)) || ((((((((((((((((((((((((((4
        <= b && 5 <= a) && 14 <= size) && a <= 2147483638) && b <= 2147483637) &&
        (-19LL + (long long )a) + (long long )size >= 0LL) && (-18LL + (long long
        )b) + (long long )size >= 0LL) && (-9LL + (long long )a) + (long long )b >=
        0LL) && (2147483634LL + (long long )size) + (long long )t >= 0LL) && (2147483643LL
        + (long long )a) + (long long )t >= 0LL) && (2147483644LL + (long long )b)
        + (long long )t >= 0LL) && (-10LL - (long long )b) + (long long )size >= 0LL)
        && (-9LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (4294967285LL - (long long )b) + (long long
        )t >= 0LL) && (4294967286LL - (long long )a) + (long long )t >= 0LL) && (10LL
        + (long long )b) - (long long )size >= 0LL) && (2147483632LL + (long long
        )a) - (long long )b >= 0LL) && (2147483633LL + (long long )size) - (long long
        )t >= 0LL) && (2147483642LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483642LL + (long long )a) - (long long )t >= 0LL) && (2147483643LL +
        (long long )b) - (long long )t >= 0LL) && (4294967275LL - (long long )a) -
        (long long )b >= 0LL) && (4294967284LL - (long long )b) - (long long )size
        >= 0LL) && (4294967284LL - (long long )b) - (long long )t >= 0LL) && (4294967285LL
        - (long long )a) - (long long )size >= 0LL) && (4294967285LL - (long long
        )a) - (long long )t >= 0LL)) || ((((((((((((((((((((((((((4 <= b && 5 <= a)
        && 13 <= size) && a <= 2147483639) && b <= 2147483638) && (-18LL + (long long
        )a) + (long long )size >= 0LL) && (-17LL + (long long )b) + (long long )size
        >= 0LL) && (-9LL + (long long )a) + (long long )b >= 0LL) && (2147483635LL
        + (long long )size) + (long long )t >= 0LL) && (2147483643LL + (long long
        )a) + (long long )t >= 0LL) && (2147483644LL + (long long )b) + (long long
        )t >= 0LL) && (-9LL - (long long )b) + (long long )size >= 0LL) && (-8LL -
        (long long )a) + (long long )size >= 0LL) && (1LL - (long long )a) + (long
        long )b >= 0LL) && (4294967286LL - (long long )b) + (long long )t >= 0LL)
        && (4294967287LL - (long long )a) + (long long )t >= 0LL) && (9LL + (long
        long )b) - (long long )size >= 0LL) && (2147483633LL + (long long )a) - (long
        long )b >= 0LL) && (2147483634LL + (long long )size) - (long long )t >= 0LL)
        && (2147483642LL + (long long )a) - (long long )size >= 0LL) && (2147483642LL
        + (long long )a) - (long long )t >= 0LL) && (2147483643LL + (long long )b)
        - (long long )t >= 0LL) && (4294967277LL - (long long )a) - (long long )b
        >= 0LL) && (4294967285LL - (long long )b) - (long long )size >= 0LL) && (4294967285LL
        - (long long )b) - (long long )t >= 0LL) && (4294967286LL - (long long )a)
        - (long long )size >= 0LL) && (4294967286LL - (long long )a) - (long long
        )t >= 0LL)) || (((((((((((((((((((((((((1 <= b && 12 <= size) && b <= 2147483636)
        && (-14LL + (long long )a) + (long long )size >= 0LL) && (-13LL + (long long
        )b) + (long long )size >= 0LL) && (-3LL + (long long )a) + (long long )b >=
        0LL) && (2147483636LL + (long long )size) + (long long )t >= 0LL) && (2147483646LL
        + (long long )a) + (long long )t >= 0LL) && (2147483647LL + (long long )b)
        + (long long )t >= 0LL) && (-11LL - (long long )b) + (long long )size >= 0LL)
        && (-10LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483650LL - (long long )a) + (long long
        )t >= 0LL) && (4294967284LL - (long long )b) + (long long )t >= 0LL) && (11LL
        + (long long )b) - (long long )size >= 0LL) && (2147483634LL + (long long
        )a) - (long long )b >= 0LL) && (2147483635LL + (long long )size) - (long long
        )t >= 0LL) && (2147483645LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483645LL + (long long )a) - (long long )t >= 0LL) && (2147483646LL +
        (long long )b) - (long long )t >= 0LL) && (2147483638LL - (long long )a) -
        (long long )b >= 0LL) && (2147483649LL - (long long )a) - (long long )size
        >= 0LL) && (2147483649LL - (long long )a) - (long long )t >= 0LL) && (4294967283LL
        - (long long )b) - (long long )size >= 0LL) && (4294967283LL - (long long
        )b) - (long long )t >= 0LL) && a == 2)) || ((((((((((((((((((((((((((4 <=
        b && 5 <= a) && 12 <= size) && a <= 2147483640) && b <= 2147483639) && (-17LL
        + (long long )a) + (long long )size >= 0LL) && (-16LL + (long long )b) + (long
        long )size >= 0LL) && (-9LL + (long long )a) + (long long )b >= 0LL) && (2147483636LL
        + (long long )size) + (long long )t >= 0LL) && (2147483643LL + (long long
        )a) + (long long )t >= 0LL) && (2147483644LL + (long long )b) + (long long
        )t >= 0LL) && (-8LL - (long long )b) + (long long )size >= 0LL) && (-7LL -
        (long long )a) + (long long )size >= 0LL) && (1LL - (long long )a) + (long
        long )b >= 0LL) && (4294967287LL - (long long )b) + (long long )t >= 0LL)
        && (4294967288LL - (long long )a) + (long long )t >= 0LL) && (8LL + (long
        long )b) - (long long )size >= 0LL) && (2147483634LL + (long long )a) - (long
        long )b >= 0LL) && (2147483635LL + (long long )size) - (long long )t >= 0LL)
        && (2147483642LL + (long long )a) - (long long )size >= 0LL) && (2147483642LL
        + (long long )a) - (long long )t >= 0LL) && (2147483643LL + (long long )b)
        - (long long )t >= 0LL) && (4294967279LL - (long long )a) - (long long )b
        >= 0LL) && (4294967286LL - (long long )b) - (long long )size >= 0LL) && (4294967286LL
        - (long long )b) - (long long )t >= 0LL) && (4294967287LL - (long long )a)
        - (long long )size >= 0LL) && (4294967287LL - (long long )a) - (long long
        )t >= 0LL)) || (((((((((((((((((((((((((1 <= b && 11 <= size) && b <= 2147483637)
        && (-13LL + (long long )a) + (long long )size >= 0LL) && (-12LL + (long long
        )b) + (long long )size >= 0LL) && (-3LL + (long long )a) + (long long )b >=
        0LL) && (2147483637LL + (long long )size) + (long long )t >= 0LL) && (2147483646LL
        + (long long )a) + (long long )t >= 0LL) && (2147483647LL + (long long )b)
        + (long long )t >= 0LL) && (-10LL - (long long )b) + (long long )size >= 0LL)
        && (-9LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483650LL - (long long )a) + (long long
        )t >= 0LL) && (4294967285LL - (long long )b) + (long long )t >= 0LL) && (10LL
        + (long long )b) - (long long )size >= 0LL) && (2147483635LL + (long long
        )a) - (long long )b >= 0LL) && (2147483636LL + (long long )size) - (long long
        )t >= 0LL) && (2147483645LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483645LL + (long long )a) - (long long )t >= 0LL) && (2147483646LL +
        (long long )b) - (long long )t >= 0LL) && (2147483639LL - (long long )a) -
        (long long )b >= 0LL) && (2147483649LL - (long long )a) - (long long )size
        >= 0LL) && (2147483649LL - (long long )a) - (long long )t >= 0LL) && (4294967284LL
        - (long long )b) - (long long )size >= 0LL) && (4294967284LL - (long long
        )b) - (long long )t >= 0LL) && a == 2)) || ((((((((((((((((((((((((((4 <=
        b && 5 <= a) && 11 <= size) && a <= 2147483641) && b <= 2147483640) && (-16LL
        + (long long )a) + (long long )size >= 0LL) && (-15LL + (long long )b) + (long
        long )size >= 0LL) && (-9LL + (long long )a) + (long long )b >= 0LL) && (2147483637LL
        + (long long )size) + (long long )t >= 0LL) && (2147483643LL + (long long
        )a) + (long long )t >= 0LL) && (2147483644LL + (long long )b) + (long long
        )t >= 0LL) && (-7LL - (long long )b) + (long long )size >= 0LL) && (-6LL -
        (long long )a) + (long long )size >= 0LL) && (1LL - (long long )a) + (long
        long )b >= 0LL) && (4294967288LL - (long long )b) + (long long )t >= 0LL)
        && (4294967289LL - (long long )a) + (long long )t >= 0LL) && (7LL + (long
        long )b) - (long long )size >= 0LL) && (2147483635LL + (long long )a) - (long
        long )b >= 0LL) && (2147483636LL + (long long )size) - (long long )t >= 0LL)
        && (2147483642LL + (long long )a) - (long long )size >= 0LL) && (2147483642LL
        + (long long )a) - (long long )t >= 0LL) && (2147483643LL + (long long )b)
        - (long long )t >= 0LL) && (4294967281LL - (long long )a) - (long long )b
        >= 0LL) && (4294967287LL - (long long )b) - (long long )size >= 0LL) && (4294967287LL
        - (long long )b) - (long long )t >= 0LL) && (4294967288LL - (long long )a)
        - (long long )size >= 0LL) && (4294967288LL - (long long )a) - (long long
        )t >= 0LL)) || (((((((((((((((((((((((((1 <= b && 10 <= size) && b <= 2147483638)
        && (-12LL + (long long )a) + (long long )size >= 0LL) && (-11LL + (long long
        )b) + (long long )size >= 0LL) && (-3LL + (long long )a) + (long long )b >=
        0LL) && (2147483638LL + (long long )size) + (long long )t >= 0LL) && (2147483646LL
        + (long long )a) + (long long )t >= 0LL) && (2147483647LL + (long long )b)
        + (long long )t >= 0LL) && (-9LL - (long long )b) + (long long )size >= 0LL)
        && (-8LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483650LL - (long long )a) + (long long
        )t >= 0LL) && (4294967286LL - (long long )b) + (long long )t >= 0LL) && (9LL
        + (long long )b) - (long long )size >= 0LL) && (2147483636LL + (long long
        )a) - (long long )b >= 0LL) && (2147483637LL + (long long )size) - (long long
        )t >= 0LL) && (2147483645LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483645LL + (long long )a) - (long long )t >= 0LL) && (2147483646LL +
        (long long )b) - (long long )t >= 0LL) && (2147483640LL - (long long )a) -
        (long long )b >= 0LL) && (2147483649LL - (long long )a) - (long long )size
        >= 0LL) && (2147483649LL - (long long )a) - (long long )t >= 0LL) && (4294967285LL
        - (long long )b) - (long long )size >= 0LL) && (4294967285LL - (long long
        )b) - (long long )t >= 0LL) && a == 2)) || ((((((((((((((((((((((((((4 <=
        b && 5 <= a) && 10 <= size) && a <= 2147483642) && b <= 2147483641) && (-15LL
        + (long long )a) + (long long )size >= 0LL) && (-14LL + (long long )b) + (long
        long )size >= 0LL) && (-9LL + (long long )a) + (long long )b >= 0LL) && (2147483638LL
        + (long long )size) + (long long )t >= 0LL) && (2147483643LL + (long long
        )a) + (long long )t >= 0LL) && (2147483644LL + (long long )b) + (long long
        )t >= 0LL) && (-6LL - (long long )b) + (long long )size >= 0LL) && (-5LL -
        (long long )a) + (long long )size >= 0LL) && (1LL - (long long )a) + (long
        long )b >= 0LL) && (4294967289LL - (long long )b) + (long long )t >= 0LL)
        && (4294967290LL - (long long )a) + (long long )t >= 0LL) && (6LL + (long
        long )b) - (long long )size >= 0LL) && (2147483636LL + (long long )a) - (long
        long )b >= 0LL) && (2147483637LL + (long long )size) - (long long )t >= 0LL)
        && (2147483642LL + (long long )a) - (long long )size >= 0LL) && (2147483642LL
        + (long long )a) - (long long )t >= 0LL) && (2147483643LL + (long long )b)
        - (long long )t >= 0LL) && (4294967283LL - (long long )a) - (long long )b
        >= 0LL) && (4294967288LL - (long long )b) - (long long )size >= 0LL) && (4294967288LL
        - (long long )b) - (long long )t >= 0LL) && (4294967289LL - (long long )a)
        - (long long )size >= 0LL) && (4294967289LL - (long long )a) - (long long
        )t >= 0LL)) || (((((((((((((((((((((((((1 <= b && 9 <= size) && b <= 2147483639)
        && (-11LL + (long long )a) + (long long )size >= 0LL) && (-10LL + (long long
        )b) + (long long )size >= 0LL) && (-3LL + (long long )a) + (long long )b >=
        0LL) && (2147483639LL + (long long )size) + (long long )t >= 0LL) && (2147483646LL
        + (long long )a) + (long long )t >= 0LL) && (2147483647LL + (long long )b)
        + (long long )t >= 0LL) && (-8LL - (long long )b) + (long long )size >= 0LL)
        && (-7LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483650LL - (long long )a) + (long long
        )t >= 0LL) && (4294967287LL - (long long )b) + (long long )t >= 0LL) && (8LL
        + (long long )b) - (long long )size >= 0LL) && (2147483637LL + (long long
        )a) - (long long )b >= 0LL) && (2147483638LL + (long long )size) - (long long
        )t >= 0LL) && (2147483645LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483645LL + (long long )a) - (long long )t >= 0LL) && (2147483646LL +
        (long long )b) - (long long )t >= 0LL) && (2147483641LL - (long long )a) -
        (long long )b >= 0LL) && (2147483649LL - (long long )a) - (long long )size
        >= 0LL) && (2147483649LL - (long long )a) - (long long )t >= 0LL) && (4294967286LL
        - (long long )b) - (long long )size >= 0LL) && (4294967286LL - (long long
        )b) - (long long )t >= 0LL) && a == 2)) || ((((((((((((((((((((((((((4 <=
        b && 5 <= a) && 9 <= size) && a <= 2147483643) && b <= 2147483642) && (-14LL
        + (long long )a) + (long long )size >= 0LL) && (-13LL + (long long )b) + (long
        long )size >= 0LL) && (-9LL + (long long )a) + (long long )b >= 0LL) && (2147483639LL
        + (long long )size) + (long long )t >= 0LL) && (2147483643LL + (long long
        )a) + (long long )t >= 0LL) && (2147483644LL + (long long )b) + (long long
        )t >= 0LL) && (-5LL - (long long )b) + (long long )size >= 0LL) && (-4LL -
        (long long )a) + (long long )size >= 0LL) && (1LL - (long long )a) + (long
        long )b >= 0LL) && (4294967290LL - (long long )b) + (long long )t >= 0LL)
        && (4294967291LL - (long long )a) + (long long )t >= 0LL) && (5LL + (long
        long )b) - (long long )size >= 0LL) && (2147483637LL + (long long )a) - (long
        long )b >= 0LL) && (2147483638LL + (long long )size) - (long long )t >= 0LL)
        && (2147483642LL + (long long )a) - (long long )size >= 0LL) && (2147483642LL
        + (long long )a) - (long long )t >= 0LL) && (2147483643LL + (long long )b)
        - (long long )t >= 0LL) && (4294967285LL - (long long )a) - (long long )b
        >= 0LL) && (4294967289LL - (long long )b) - (long long )size >= 0LL) && (4294967289LL
        - (long long )b) - (long long )t >= 0LL) && (4294967290LL - (long long )a)
        - (long long )size >= 0LL) && (4294967290LL - (long long )a) - (long long
        )t >= 0LL)) || (((((((((((((((((((((((((1 <= b && 8 <= size) && b <= 2147483640)
        && (-10LL + (long long )a) + (long long )size >= 0LL) && (-9LL + (long long
        )b) + (long long )size >= 0LL) && (-3LL + (long long )a) + (long long )b >=
        0LL) && (2147483640LL + (long long )size) + (long long )t >= 0LL) && (2147483646LL
        + (long long )a) + (long long )t >= 0LL) && (2147483647LL + (long long )b)
        + (long long )t >= 0LL) && (-7LL - (long long )b) + (long long )size >= 0LL)
        && (-6LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483650LL - (long long )a) + (long long
        )t >= 0LL) && (4294967288LL - (long long )b) + (long long )t >= 0LL) && (7LL
        + (long long )b) - (long long )size >= 0LL) && (2147483638LL + (long long
        )a) - (long long )b >= 0LL) && (2147483639LL + (long long )size) - (long long
        )t >= 0LL) && (2147483645LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483645LL + (long long )a) - (long long )t >= 0LL) && (2147483646LL +
        (long long )b) - (long long )t >= 0LL) && (2147483642LL - (long long )a) -
        (long long )b >= 0LL) && (2147483649LL - (long long )a) - (long long )size
        >= 0LL) && (2147483649LL - (long long )a) - (long long )t >= 0LL) && (4294967287LL
        - (long long )b) - (long long )size >= 0LL) && (4294967287LL - (long long
        )b) - (long long )t >= 0LL) && a == 2)) || ((((((((((((((((((((((((((4 <=
        b && 5 <= a) && 8 <= size) && a <= 2147483644) && b <= 2147483643) && (-13LL
        + (long long )a) + (long long )size >= 0LL) && (-12LL + (long long )b) + (long
        long )size >= 0LL) && (-9LL + (long long )a) + (long long )b >= 0LL) && (2147483640LL
        + (long long )size) + (long long )t >= 0LL) && (2147483643LL + (long long
        )a) + (long long )t >= 0LL) && (2147483644LL + (long long )b) + (long long
        )t >= 0LL) && (-4LL - (long long )b) + (long long )size >= 0LL) && (-3LL -
        (long long )a) + (long long )size >= 0LL) && (1LL - (long long )a) + (long
        long )b >= 0LL) && (4294967291LL - (long long )b) + (long long )t >= 0LL)
        && (4294967292LL - (long long )a) + (long long )t >= 0LL) && (4LL + (long
        long )b) - (long long )size >= 0LL) && (2147483638LL + (long long )a) - (long
        long )b >= 0LL) && (2147483639LL + (long long )size) - (long long )t >= 0LL)
        && (2147483642LL + (long long )a) - (long long )size >= 0LL) && (2147483642LL
        + (long long )a) - (long long )t >= 0LL) && (2147483643LL + (long long )b)
        - (long long )t >= 0LL) && (4294967287LL - (long long )a) - (long long )b
        >= 0LL) && (4294967290LL - (long long )b) - (long long )size >= 0LL) && (4294967290LL
        - (long long )b) - (long long )t >= 0LL) && (4294967291LL - (long long )a)
        - (long long )size >= 0LL) && (4294967291LL - (long long )a) - (long long
        )t >= 0LL)) || (((((((((((((((((((((((((1 <= b && 7 <= size) && b <= 2147483641)
        && (-9LL + (long long )a) + (long long )size >= 0LL) && (-8LL + (long long
        )b) + (long long )size >= 0LL) && (-3LL + (long long )a) + (long long )b >=
        0LL) && (2147483641LL + (long long )size) + (long long )t >= 0LL) && (2147483646LL
        + (long long )a) + (long long )t >= 0LL) && (2147483647LL + (long long )b)
        + (long long )t >= 0LL) && (-6LL - (long long )b) + (long long )size >= 0LL)
        && (-5LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483650LL - (long long )a) + (long long
        )t >= 0LL) && (4294967289LL - (long long )b) + (long long )t >= 0LL) && (6LL
        + (long long )b) - (long long )size >= 0LL) && (2147483639LL + (long long
        )a) - (long long )b >= 0LL) && (2147483640LL + (long long )size) - (long long
        )t >= 0LL) && (2147483645LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483645LL + (long long )a) - (long long )t >= 0LL) && (2147483646LL +
        (long long )b) - (long long )t >= 0LL) && (2147483643LL - (long long )a) -
        (long long )b >= 0LL) && (2147483649LL - (long long )a) - (long long )size
        >= 0LL) && (2147483649LL - (long long )a) - (long long )t >= 0LL) && (4294967288LL
        - (long long )b) - (long long )size >= 0LL) && (4294967288LL - (long long
        )b) - (long long )t >= 0LL) && a == 2)) || ((((((((((((((((((((((((((4 <=
        b && 5 <= a) && 7 <= size) && a <= 2147483645) && b <= 2147483644) && (-12LL
        + (long long )a) + (long long )size >= 0LL) && (-11LL + (long long )b) + (long
        long )size >= 0LL) && (-9LL + (long long )a) + (long long )b >= 0LL) && (2147483641LL
        + (long long )size) + (long long )t >= 0LL) && (2147483643LL + (long long
        )a) + (long long )t >= 0LL) && (2147483644LL + (long long )b) + (long long
        )t >= 0LL) && (-3LL - (long long )b) + (long long )size >= 0LL) && (-2LL -
        (long long )a) + (long long )size >= 0LL) && (1LL - (long long )a) + (long
        long )b >= 0LL) && (4294967292LL - (long long )b) + (long long )t >= 0LL)
        && (4294967293LL - (long long )a) + (long long )t >= 0LL) && (3LL + (long
        long )b) - (long long )size >= 0LL) && (2147483639LL + (long long )a) - (long
        long )b >= 0LL) && (2147483640LL + (long long )size) - (long long )t >= 0LL)
        && (2147483642LL + (long long )a) - (long long )size >= 0LL) && (2147483642LL
        + (long long )a) - (long long )t >= 0LL) && (2147483643LL + (long long )b)
        - (long long )t >= 0LL) && (4294967289LL - (long long )a) - (long long )b
        >= 0LL) && (4294967291LL - (long long )b) - (long long )size >= 0LL) && (4294967291LL
        - (long long )b) - (long long )t >= 0LL) && (4294967292LL - (long long )a)
        - (long long )size >= 0LL) && (4294967292LL - (long long )a) - (long long
        )t >= 0LL)) || (((((((((((((((((((((((((1 <= b && 6 <= size) && b <= 2147483642)
        && (-8LL + (long long )a) + (long long )size >= 0LL) && (-7LL + (long long
        )b) + (long long )size >= 0LL) && (-3LL + (long long )a) + (long long )b >=
        0LL) && (2147483642LL + (long long )size) + (long long )t >= 0LL) && (2147483646LL
        + (long long )a) + (long long )t >= 0LL) && (2147483647LL + (long long )b)
        + (long long )t >= 0LL) && (-5LL - (long long )b) + (long long )size >= 0LL)
        && (-4LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483650LL - (long long )a) + (long long
        )t >= 0LL) && (4294967290LL - (long long )b) + (long long )t >= 0LL) && (5LL
        + (long long )b) - (long long )size >= 0LL) && (2147483640LL + (long long
        )a) - (long long )b >= 0LL) && (2147483641LL + (long long )size) - (long long
        )t >= 0LL) && (2147483645LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483645LL + (long long )a) - (long long )t >= 0LL) && (2147483646LL +
        (long long )b) - (long long )t >= 0LL) && (2147483644LL - (long long )a) -
        (long long )b >= 0LL) && (2147483649LL - (long long )a) - (long long )size
        >= 0LL) && (2147483649LL - (long long )a) - (long long )t >= 0LL) && (4294967289LL
        - (long long )b) - (long long )size >= 0LL) && (4294967289LL - (long long
        )b) - (long long )t >= 0LL) && a == 2)) || ((((((((((((((((((((((((((4 <=
        b && 5 <= a) && 6 <= size) && a <= 2147483646) && b <= 2147483645) && (-11LL
        + (long long )a) + (long long )size >= 0LL) && (-10LL + (long long )b) + (long
        long )size >= 0LL) && (-9LL + (long long )a) + (long long )b >= 0LL) && (2147483642LL
        + (long long )size) + (long long )t >= 0LL) && (2147483643LL + (long long
        )a) + (long long )t >= 0LL) && (2147483644LL + (long long )b) + (long long
        )t >= 0LL) && (-2LL - (long long )b) + (long long )size >= 0LL) && (-1LL -
        (long long )a) + (long long )size >= 0LL) && (1LL - (long long )a) + (long
        long )b >= 0LL) && (4294967293LL - (long long )b) + (long long )t >= 0LL)
        && (4294967294LL - (long long )a) + (long long )t >= 0LL) && (2LL + (long
        long )b) - (long long )size >= 0LL) && (2147483640LL + (long long )a) - (long
        long )b >= 0LL) && (2147483641LL + (long long )size) - (long long )t >= 0LL)
        && (2147483642LL + (long long )a) - (long long )size >= 0LL) && (2147483642LL
        + (long long )a) - (long long )t >= 0LL) && (2147483643LL + (long long )b)
        - (long long )t >= 0LL) && (4294967291LL - (long long )a) - (long long )b
        >= 0LL) && (4294967292LL - (long long )b) - (long long )size >= 0LL) && (4294967292LL
        - (long long )b) - (long long )t >= 0LL) && (4294967293LL - (long long )a)
        - (long long )size >= 0LL) && (4294967293LL - (long long )a) - (long long
        )t >= 0LL)) || (((((((((((((((((((((((((1 <= b && 5 <= size) && b <= 2147483643)
        && (-7LL + (long long )a) + (long long )size >= 0LL) && (-6LL + (long long
        )b) + (long long )size >= 0LL) && (-3LL + (long long )a) + (long long )b >=
        0LL) && (2147483643LL + (long long )size) + (long long )t >= 0LL) && (2147483646LL
        + (long long )a) + (long long )t >= 0LL) && (2147483647LL + (long long )b)
        + (long long )t >= 0LL) && (-4LL - (long long )b) + (long long )size >= 0LL)
        && (-3LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483650LL - (long long )a) + (long long
        )t >= 0LL) && (4294967291LL - (long long )b) + (long long )t >= 0LL) && (4LL
        + (long long )b) - (long long )size >= 0LL) && (2147483641LL + (long long
        )a) - (long long )b >= 0LL) && (2147483642LL + (long long )size) - (long long
        )t >= 0LL) && (2147483645LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483645LL + (long long )a) - (long long )t >= 0LL) && (2147483646LL +
        (long long )b) - (long long )t >= 0LL) && (2147483645LL - (long long )a) -
        (long long )b >= 0LL) && (2147483649LL - (long long )a) - (long long )size
        >= 0LL) && (2147483649LL - (long long )a) - (long long )t >= 0LL) && (4294967290LL
        - (long long )b) - (long long )size >= 0LL) && (4294967290LL - (long long
        )b) - (long long )t >= 0LL) && a == 2)) || ((((((((((((((((((((((((((5 <=
        a && 5 <= b) && 6 <= size) && a <= 2147483646) && b <= 2147483646) && (-11LL
        + (long long )a) + (long long )size >= 0LL) && (-11LL + (long long )b) + (long
        long )size >= 0LL) && (-10LL + (long long )a) + (long long )b >= 0LL) && (2147483642LL
        + (long long )size) + (long long )t >= 0LL) && (2147483643LL + (long long
        )a) + (long long )t >= 0LL) && (2147483643LL + (long long )b) + (long long
        )t >= 0LL) && (-1LL - (long long )a) + (long long )size >= 0LL) && (-1LL -
        (long long )b) + (long long )size >= 0LL) && (0LL - (long long )a) + (long
        long )b >= 0LL) && (4294967294LL - (long long )a) + (long long )t >= 0LL)
        && (4294967294LL - (long long )b) + (long long )t >= 0LL) && (1LL + (long
        long )b) - (long long )size >= 0LL) && (2147483641LL + (long long )size) -
        (long long )t >= 0LL) && (2147483641LL + (long long )a) - (long long )b >=
        0LL) && (2147483642LL + (long long )a) - (long long )size >= 0LL) && (2147483642LL
        + (long long )a) - (long long )t >= 0LL) && (2147483642LL + (long long )b)
        - (long long )t >= 0LL) && (4294967292LL - (long long )a) - (long long )b
        >= 0LL) && (4294967293LL - (long long )a) - (long long )size >= 0LL) && (4294967293LL
        - (long long )a) - (long long )t >= 0LL) && (4294967293LL - (long long )b)
        - (long long )size >= 0LL) && (4294967293LL - (long long )b) - (long long
        )t >= 0LL)) || (((((((((((((((((((((((((1 <= b && 4 <= size) && b <= 2147483644)
        && (-6LL + (long long )a) + (long long )size >= 0LL) && (-5LL + (long long
        )b) + (long long )size >= 0LL) && (-3LL + (long long )a) + (long long )b >=
        0LL) && (2147483644LL + (long long )size) + (long long )t >= 0LL) && (2147483646LL
        + (long long )a) + (long long )t >= 0LL) && (2147483647LL + (long long )b)
        + (long long )t >= 0LL) && (-3LL - (long long )b) + (long long )size >= 0LL)
        && (-2LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483650LL - (long long )a) + (long long
        )t >= 0LL) && (4294967292LL - (long long )b) + (long long )t >= 0LL) && (3LL
        + (long long )b) - (long long )size >= 0LL) && (2147483642LL + (long long
        )a) - (long long )b >= 0LL) && (2147483643LL + (long long )size) - (long long
        )t >= 0LL) && (2147483645LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483645LL + (long long )a) - (long long )t >= 0LL) && (2147483646LL +
        (long long )b) - (long long )t >= 0LL) && (2147483646LL - (long long )a) -
        (long long )b >= 0LL) && (2147483649LL - (long long )a) - (long long )size
        >= 0LL) && (2147483649LL - (long long )a) - (long long )t >= 0LL) && (4294967291LL
        - (long long )b) - (long long )size >= 0LL) && (4294967291LL - (long long
        )b) - (long long )t >= 0LL) && a == 2)) || (((((((((((((((((((((((((1 <= b
        && 3 <= size) && b <= 2147483645) && (-5LL + (long long )a) + (long long )size
        >= 0LL) && (-4LL + (long long )b) + (long long )size >= 0LL) && (-3LL + (long
        long )a) + (long long )b >= 0LL) && (2147483645LL + (long long )size) + (long
        long )t >= 0LL) && (2147483646LL + (long long )a) + (long long )t >= 0LL)
        && (2147483647LL + (long long )b) + (long long )t >= 0LL) && (-2LL - (long
        long )b) + (long long )size >= 0LL) && (-1LL - (long long )a) + (long long
        )size >= 0LL) && (1LL - (long long )a) + (long long )b >= 0LL) && (2147483650LL
        - (long long )a) + (long long )t >= 0LL) && (4294967293LL - (long long )b)
        + (long long )t >= 0LL) && (2LL + (long long )b) - (long long )size >= 0LL)
        && (2147483643LL + (long long )a) - (long long )b >= 0LL) && (2147483644LL
        + (long long )size) - (long long )t >= 0LL) && (2147483645LL + (long long
        )a) - (long long )size >= 0LL) && (2147483645LL + (long long )a) - (long long
        )t >= 0LL) && (2147483646LL + (long long )b) - (long long )t >= 0LL) && (2147483647LL
        - (long long )a) - (long long )b >= 0LL) && (2147483649LL - (long long )a)
        - (long long )size >= 0LL) && (2147483649LL - (long long )a) - (long long
        )t >= 0LL) && (4294967292LL - (long long )b) - (long long )size >= 0LL) &&
        (4294967292LL - (long long )b) - (long long )t >= 0LL) && a == 2)) || (((((((((((((((((((((((((3
        <= b && 15 <= size) && b <= 2147483635) && (-19LL + (long long )a) + (long
        long )size >= 0LL) && (-18LL + (long long )b) + (long long )size >= 0LL) &&
        (-7LL + (long long )a) + (long long )b >= 0LL) && (2147483633LL + (long long
        )size) + (long long )t >= 0LL) && (2147483644LL + (long long )a) + (long long
        )t >= 0LL) && (2147483645LL + (long long )b) + (long long )t >= 0LL) && (-12LL
        - (long long )b) + (long long )size >= 0LL) && (-11LL - (long long )a) + (long
        long )size >= 0LL) && (1LL - (long long )a) + (long long )b >= 0LL) && (2147483652LL
        - (long long )a) + (long long )t >= 0LL) && (4294967283LL - (long long )b)
        + (long long )t >= 0LL) && (2147483631LL + (long long )a) - (long long )b
        >= 0LL) && (2147483632LL + (long long )size) - (long long )t >= 0LL) && (2147483643LL
        + (long long )a) - (long long )size >= 0LL) && (2147483643LL + (long long
        )a) - (long long )t >= 0LL) && (2147483644LL + (long long )b) - (long long
        )size >= 0LL) && (2147483644LL + (long long )b) - (long long )t >= 0LL) &&
        (2147483639LL - (long long )a) - (long long )b >= 0LL) && (2147483651LL -
        (long long )a) - (long long )size >= 0LL) && (2147483651LL - (long long )a)
        - (long long )t >= 0LL) && (4294967282LL - (long long )b) - (long long )size
        >= 0LL) && (4294967282LL - (long long )b) - (long long )t >= 0LL) && a ==
        4)) || (((((((((((((((((((((((((2 <= b && 3 <= size) && b <= 2147483646) &&
        (-5LL + (long long )a) + (long long )size >= 0LL) && (-5LL + (long long )b)
        + (long long )size >= 0LL) && (-4LL + (long long )a) + (long long )b >= 0LL)
        && (2147483645LL + (long long )size) + (long long )t >= 0LL) && (2147483646LL
        + (long long )a) + (long long )t >= 0LL) && (2147483646LL + (long long )b)
        + (long long )t >= 0LL) && (-1LL - (long long )a) + (long long )size >= 0LL)
        && (-1LL - (long long )b) + (long long )size >= 0LL) && (0LL - (long long
        )a) + (long long )b >= 0LL) && (2147483650LL - (long long )a) + (long long
        )t >= 0LL) && (4294967294LL - (long long )b) + (long long )t >= 0LL) && (1LL
        + (long long )b) - (long long )size >= 0LL) && (2147483644LL + (long long
        )size) - (long long )t >= 0LL) && (2147483644LL + (long long )a) - (long long
        )b >= 0LL) && (2147483645LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483645LL + (long long )a) - (long long )t >= 0LL) && (2147483645LL +
        (long long )b) - (long long )t >= 0LL) && (2147483648LL - (long long )a) -
        (long long )b >= 0LL) && (2147483649LL - (long long )a) - (long long )size
        >= 0LL) && (2147483649LL - (long long )a) - (long long )t >= 0LL) && (4294967293LL
        - (long long )b) - (long long )size >= 0LL) && (4294967293LL - (long long
        )b) - (long long )t >= 0LL) && a == 2)) || (((((((((((((((((((((((((3 <= b
        && 14 <= size) && b <= 2147483636) && (-18LL + (long long )a) + (long long
        )size >= 0LL) && (-17LL + (long long )b) + (long long )size >= 0LL) && (-7LL
        + (long long )a) + (long long )b >= 0LL) && (2147483634LL + (long long )size)
        + (long long )t >= 0LL) && (2147483644LL + (long long )a) + (long long )t
        >= 0LL) && (2147483645LL + (long long )b) + (long long )t >= 0LL) && (-11LL
        - (long long )b) + (long long )size >= 0LL) && (-10LL - (long long )a) + (long
        long )size >= 0LL) && (1LL - (long long )a) + (long long )b >= 0LL) && (2147483652LL
        - (long long )a) + (long long )t >= 0LL) && (4294967284LL - (long long )b)
        + (long long )t >= 0LL) && (11LL + (long long )b) - (long long )size >= 0LL)
        && (2147483632LL + (long long )a) - (long long )b >= 0LL) && (2147483633LL
        + (long long )size) - (long long )t >= 0LL) && (2147483643LL + (long long
        )a) - (long long )size >= 0LL) && (2147483643LL + (long long )a) - (long long
        )t >= 0LL) && (2147483644LL + (long long )b) - (long long )t >= 0LL) && (2147483640LL
        - (long long )a) - (long long )b >= 0LL) && (2147483651LL - (long long )a)
        - (long long )size >= 0LL) && (2147483651LL - (long long )a) - (long long
        )t >= 0LL) && (4294967283LL - (long long )b) - (long long )size >= 0LL) &&
        (4294967283LL - (long long )b) - (long long )t >= 0LL) && a == 4)) || ((((((((((((((((((((((((((0
        <= b && 12 <= size) && b <= 2147483635) && (-13LL + (long long )a) + (long
        long )size >= 0LL) && (-12LL + (long long )b) + (long long )size >= 0LL) &&
        (-1LL + (long long )a) + (long long )b >= 0LL) && (2147483636LL + (long long
        )size) + (long long )t >= 0LL) && (2147483647LL + (long long )a) + (long long
        )t >= 0LL) && (2147483648LL + (long long )b) + (long long )t >= 0LL) && (-12LL
        - (long long )b) + (long long )size >= 0LL) && (-11LL - (long long )a) + (long
        long )size >= 0LL) && (1LL - (long long )a) + (long long )b >= 0LL) && (2147483649LL
        - (long long )a) + (long long )t >= 0LL) && (4294967283LL - (long long )b)
        + (long long )t >= 0LL) && (2147483634LL + (long long )a) - (long long )b
        >= 0LL) && (2147483635LL + (long long )size) - (long long )t >= 0LL) && (2147483646LL
        + (long long )a) - (long long )size >= 0LL) && (2147483646LL + (long long
        )a) - (long long )t >= 0LL) && (2147483647LL + (long long )b) - (long long
        )size >= 0LL) && (2147483647LL + (long long )b) - (long long )t >= 0LL) &&
        (2147483636LL - (long long )a) - (long long )b >= 0LL) && (2147483648LL -
        (long long )a) - (long long )size >= 0LL) && (2147483648LL - (long long )a)
        - (long long )t >= 0LL) && (4294967282LL - (long long )b) - (long long )size
        >= 0LL) && (4294967282LL - (long long )b) - (long long )t >= 0LL) && 1 ==
        a) && a == 1)) || (((((((((((((((((((((((((3 <= b && 13 <= size) && b <= 2147483637)
        && (-17LL + (long long )a) + (long long )size >= 0LL) && (-16LL + (long long
        )b) + (long long )size >= 0LL) && (-7LL + (long long )a) + (long long )b >=
        0LL) && (2147483635LL + (long long )size) + (long long )t >= 0LL) && (2147483644LL
        + (long long )a) + (long long )t >= 0LL) && (2147483645LL + (long long )b)
        + (long long )t >= 0LL) && (-10LL - (long long )b) + (long long )size >= 0LL)
        && (-9LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483652LL - (long long )a) + (long long
        )t >= 0LL) && (4294967285LL - (long long )b) + (long long )t >= 0LL) && (10LL
        + (long long )b) - (long long )size >= 0LL) && (2147483633LL + (long long
        )a) - (long long )b >= 0LL) && (2147483634LL + (long long )size) - (long long
        )t >= 0LL) && (2147483643LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483643LL + (long long )a) - (long long )t >= 0LL) && (2147483644LL +
        (long long )b) - (long long )t >= 0LL) && (2147483641LL - (long long )a) -
        (long long )b >= 0LL) && (2147483651LL - (long long )a) - (long long )size
        >= 0LL) && (2147483651LL - (long long )a) - (long long )t >= 0LL) && (4294967284LL
        - (long long )b) - (long long )size >= 0LL) && (4294967284LL - (long long
        )b) - (long long )t >= 0LL) && a == 4)) || ((((((((((((((((((((((((((0 <=
        b && 11 <= size) && b <= 2147483636) && (-12LL + (long long )a) + (long long
        )size >= 0LL) && (-11LL + (long long )b) + (long long )size >= 0LL) && (-1LL
        + (long long )a) + (long long )b >= 0LL) && (2147483637LL + (long long )size)
        + (long long )t >= 0LL) && (2147483647LL + (long long )a) + (long long )t
        >= 0LL) && (2147483648LL + (long long )b) + (long long )t >= 0LL) && (-11LL
        - (long long )b) + (long long )size >= 0LL) && (-10LL - (long long )a) + (long
        long )size >= 0LL) && (1LL - (long long )a) + (long long )b >= 0LL) && (2147483649LL
        - (long long )a) + (long long )t >= 0LL) && (4294967284LL - (long long )b)
        + (long long )t >= 0LL) && (11LL + (long long )b) - (long long )size >= 0LL)
        && (2147483635LL + (long long )a) - (long long )b >= 0LL) && (2147483636LL
        + (long long )size) - (long long )t >= 0LL) && (2147483646LL + (long long
        )a) - (long long )size >= 0LL) && (2147483646LL + (long long )a) - (long long
        )t >= 0LL) && (2147483647LL + (long long )b) - (long long )t >= 0LL) && (2147483637LL
        - (long long )a) - (long long )b >= 0LL) && (2147483648LL - (long long )a)
        - (long long )size >= 0LL) && (2147483648LL - (long long )a) - (long long
        )t >= 0LL) && (4294967283LL - (long long )b) - (long long )size >= 0LL) &&
        (4294967283LL - (long long )b) - (long long )t >= 0LL) && 1 == a) && a ==
        1)) || (((((((((((((((((((((((((3 <= b && 12 <= size) && b <= 2147483638)
        && (-16LL + (long long )a) + (long long )size >= 0LL) && (-15LL + (long long
        )b) + (long long )size >= 0LL) && (-7LL + (long long )a) + (long long )b >=
        0LL) && (2147483636LL + (long long )size) + (long long )t >= 0LL) && (2147483644LL
        + (long long )a) + (long long )t >= 0LL) && (2147483645LL + (long long )b)
        + (long long )t >= 0LL) && (-9LL - (long long )b) + (long long )size >= 0LL)
        && (-8LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483652LL - (long long )a) + (long long
        )t >= 0LL) && (4294967286LL - (long long )b) + (long long )t >= 0LL) && (9LL
        + (long long )b) - (long long )size >= 0LL) && (2147483634LL + (long long
        )a) - (long long )b >= 0LL) && (2147483635LL + (long long )size) - (long long
        )t >= 0LL) && (2147483643LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483643LL + (long long )a) - (long long )t >= 0LL) && (2147483644LL +
        (long long )b) - (long long )t >= 0LL) && (2147483642LL - (long long )a) -
        (long long )b >= 0LL) && (2147483651LL - (long long )a) - (long long )size
        >= 0LL) && (2147483651LL - (long long )a) - (long long )t >= 0LL) && (4294967285LL
        - (long long )b) - (long long )size >= 0LL) && (4294967285LL - (long long
        )b) - (long long )t >= 0LL) && a == 4)) || ((((((((((((((((((((((((((0 <=
        b && 10 <= size) && b <= 2147483637) && (-11LL + (long long )a) + (long long
        )size >= 0LL) && (-10LL + (long long )b) + (long long )size >= 0LL) && (-1LL
        + (long long )a) + (long long )b >= 0LL) && (2147483638LL + (long long )size)
        + (long long )t >= 0LL) && (2147483647LL + (long long )a) + (long long )t
        >= 0LL) && (2147483648LL + (long long )b) + (long long )t >= 0LL) && (-10LL
        - (long long )b) + (long long )size >= 0LL) && (-9LL - (long long )a) + (long
        long )size >= 0LL) && (1LL - (long long )a) + (long long )b >= 0LL) && (2147483649LL
        - (long long )a) + (long long )t >= 0LL) && (4294967285LL - (long long )b)
        + (long long )t >= 0LL) && (10LL + (long long )b) - (long long )size >= 0LL)
        && (2147483636LL + (long long )a) - (long long )b >= 0LL) && (2147483637LL
        + (long long )size) - (long long )t >= 0LL) && (2147483646LL + (long long
        )a) - (long long )size >= 0LL) && (2147483646LL + (long long )a) - (long long
        )t >= 0LL) && (2147483647LL + (long long )b) - (long long )t >= 0LL) && (2147483638LL
        - (long long )a) - (long long )b >= 0LL) && (2147483648LL - (long long )a)
        - (long long )size >= 0LL) && (2147483648LL - (long long )a) - (long long
        )t >= 0LL) && (4294967284LL - (long long )b) - (long long )size >= 0LL) &&
        (4294967284LL - (long long )b) - (long long )t >= 0LL) && 1 == a) && a ==
        1)) || (((((((((((((((((((((((((3 <= b && 11 <= size) && b <= 2147483639)
        && (-15LL + (long long )a) + (long long )size >= 0LL) && (-14LL + (long long
        )b) + (long long )size >= 0LL) && (-7LL + (long long )a) + (long long )b >=
        0LL) && (2147483637LL + (long long )size) + (long long )t >= 0LL) && (2147483644LL
        + (long long )a) + (long long )t >= 0LL) && (2147483645LL + (long long )b)
        + (long long )t >= 0LL) && (-8LL - (long long )b) + (long long )size >= 0LL)
        && (-7LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483652LL - (long long )a) + (long long
        )t >= 0LL) && (4294967287LL - (long long )b) + (long long )t >= 0LL) && (8LL
        + (long long )b) - (long long )size >= 0LL) && (2147483635LL + (long long
        )a) - (long long )b >= 0LL) && (2147483636LL + (long long )size) - (long long
        )t >= 0LL) && (2147483643LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483643LL + (long long )a) - (long long )t >= 0LL) && (2147483644LL +
        (long long )b) - (long long )t >= 0LL) && (2147483643LL - (long long )a) -
        (long long )b >= 0LL) && (2147483651LL - (long long )a) - (long long )size
        >= 0LL) && (2147483651LL - (long long )a) - (long long )t >= 0LL) && (4294967286LL
        - (long long )b) - (long long )size >= 0LL) && (4294967286LL - (long long
        )b) - (long long )t >= 0LL) && a == 4)) || ((((((((((((((((((((((((((0 <=
        b && 9 <= size) && b <= 2147483638) && (-10LL + (long long )a) + (long long
        )size >= 0LL) && (-9LL + (long long )b) + (long long )size >= 0LL) && (-1LL
        + (long long )a) + (long long )b >= 0LL) && (2147483639LL + (long long )size)
        + (long long )t >= 0LL) && (2147483647LL + (long long )a) + (long long )t
        >= 0LL) && (2147483648LL + (long long )b) + (long long )t >= 0LL) && (-9LL
        - (long long )b) + (long long )size >= 0LL) && (-8LL - (long long )a) + (long
        long )size >= 0LL) && (1LL - (long long )a) + (long long )b >= 0LL) && (2147483649LL
        - (long long )a) + (long long )t >= 0LL) && (4294967286LL - (long long )b)
        + (long long )t >= 0LL) && (9LL + (long long )b) - (long long )size >= 0LL)
        && (2147483637LL + (long long )a) - (long long )b >= 0LL) && (2147483638LL
        + (long long )size) - (long long )t >= 0LL) && (2147483646LL + (long long
        )a) - (long long )size >= 0LL) && (2147483646LL + (long long )a) - (long long
        )t >= 0LL) && (2147483647LL + (long long )b) - (long long )t >= 0LL) && (2147483639LL
        - (long long )a) - (long long )b >= 0LL) && (2147483648LL - (long long )a)
        - (long long )size >= 0LL) && (2147483648LL - (long long )a) - (long long
        )t >= 0LL) && (4294967285LL - (long long )b) - (long long )size >= 0LL) &&
        (4294967285LL - (long long )b) - (long long )t >= 0LL) && 1 == a) && a ==
        1)) || (((((((((((((((((((((((((3 <= b && 10 <= size) && b <= 2147483640)
        && (-14LL + (long long )a) + (long long )size >= 0LL) && (-13LL + (long long
        )b) + (long long )size >= 0LL) && (-7LL + (long long )a) + (long long )b >=
        0LL) && (2147483638LL + (long long )size) + (long long )t >= 0LL) && (2147483644LL
        + (long long )a) + (long long )t >= 0LL) && (2147483645LL + (long long )b)
        + (long long )t >= 0LL) && (-7LL - (long long )b) + (long long )size >= 0LL)
        && (-6LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483652LL - (long long )a) + (long long
        )t >= 0LL) && (4294967288LL - (long long )b) + (long long )t >= 0LL) && (7LL
        + (long long )b) - (long long )size >= 0LL) && (2147483636LL + (long long
        )a) - (long long )b >= 0LL) && (2147483637LL + (long long )size) - (long long
        )t >= 0LL) && (2147483643LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483643LL + (long long )a) - (long long )t >= 0LL) && (2147483644LL +
        (long long )b) - (long long )t >= 0LL) && (2147483644LL - (long long )a) -
        (long long )b >= 0LL) && (2147483651LL - (long long )a) - (long long )size
        >= 0LL) && (2147483651LL - (long long )a) - (long long )t >= 0LL) && (4294967287LL
        - (long long )b) - (long long )size >= 0LL) && (4294967287LL - (long long
        )b) - (long long )t >= 0LL) && a == 4)) || ((((((((((((((((((((((((((0 <=
        b && 8 <= size) && b <= 2147483639) && (-9LL + (long long )a) + (long long
        )size >= 0LL) && (-8LL + (long long )b) + (long long )size >= 0LL) && (-1LL
        + (long long )a) + (long long )b >= 0LL) && (2147483640LL + (long long )size)
        + (long long )t >= 0LL) && (2147483647LL + (long long )a) + (long long )t
        >= 0LL) && (2147483648LL + (long long )b) + (long long )t >= 0LL) && (-8LL
        - (long long )b) + (long long )size >= 0LL) && (-7LL - (long long )a) + (long
        long )size >= 0LL) && (1LL - (long long )a) + (long long )b >= 0LL) && (2147483649LL
        - (long long )a) + (long long )t >= 0LL) && (4294967287LL - (long long )b)
        + (long long )t >= 0LL) && (8LL + (long long )b) - (long long )size >= 0LL)
        && (2147483638LL + (long long )a) - (long long )b >= 0LL) && (2147483639LL
        + (long long )size) - (long long )t >= 0LL) && (2147483646LL + (long long
        )a) - (long long )size >= 0LL) && (2147483646LL + (long long )a) - (long long
        )t >= 0LL) && (2147483647LL + (long long )b) - (long long )t >= 0LL) && (2147483640LL
        - (long long )a) - (long long )b >= 0LL) && (2147483648LL - (long long )a)
        - (long long )size >= 0LL) && (2147483648LL - (long long )a) - (long long
        )t >= 0LL) && (4294967286LL - (long long )b) - (long long )size >= 0LL) &&
        (4294967286LL - (long long )b) - (long long )t >= 0LL) && 1 == a) && a ==
        1)) || (((((((((((((((((((((((((3 <= b && 9 <= size) && b <= 2147483641) &&
        (-13LL + (long long )a) + (long long )size >= 0LL) && (-12LL + (long long
        )b) + (long long )size >= 0LL) && (-7LL + (long long )a) + (long long )b >=
        0LL) && (2147483639LL + (long long )size) + (long long )t >= 0LL) && (2147483644LL
        + (long long )a) + (long long )t >= 0LL) && (2147483645LL + (long long )b)
        + (long long )t >= 0LL) && (-6LL - (long long )b) + (long long )size >= 0LL)
        && (-5LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483652LL - (long long )a) + (long long
        )t >= 0LL) && (4294967289LL - (long long )b) + (long long )t >= 0LL) && (6LL
        + (long long )b) - (long long )size >= 0LL) && (2147483637LL + (long long
        )a) - (long long )b >= 0LL) && (2147483638LL + (long long )size) - (long long
        )t >= 0LL) && (2147483643LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483643LL + (long long )a) - (long long )t >= 0LL) && (2147483644LL +
        (long long )b) - (long long )t >= 0LL) && (2147483645LL - (long long )a) -
        (long long )b >= 0LL) && (2147483651LL - (long long )a) - (long long )size
        >= 0LL) && (2147483651LL - (long long )a) - (long long )t >= 0LL) && (4294967288LL
        - (long long )b) - (long long )size >= 0LL) && (4294967288LL - (long long
        )b) - (long long )t >= 0LL) && a == 4)) || ((((((((((((((((((((((((((0 <=
        b && 7 <= size) && b <= 2147483640) && (-8LL + (long long )a) + (long long
        )size >= 0LL) && (-7LL + (long long )b) + (long long )size >= 0LL) && (-1LL
        + (long long )a) + (long long )b >= 0LL) && (2147483641LL + (long long )size)
        + (long long )t >= 0LL) && (2147483647LL + (long long )a) + (long long )t
        >= 0LL) && (2147483648LL + (long long )b) + (long long )t >= 0LL) && (-7LL
        - (long long )b) + (long long )size >= 0LL) && (-6LL - (long long )a) + (long
        long )size >= 0LL) && (1LL - (long long )a) + (long long )b >= 0LL) && (2147483649LL
        - (long long )a) + (long long )t >= 0LL) && (4294967288LL - (long long )b)
        + (long long )t >= 0LL) && (7LL + (long long )b) - (long long )size >= 0LL)
        && (2147483639LL + (long long )a) - (long long )b >= 0LL) && (2147483640LL
        + (long long )size) - (long long )t >= 0LL) && (2147483646LL + (long long
        )a) - (long long )size >= 0LL) && (2147483646LL + (long long )a) - (long long
        )t >= 0LL) && (2147483647LL + (long long )b) - (long long )t >= 0LL) && (2147483641LL
        - (long long )a) - (long long )b >= 0LL) && (2147483648LL - (long long )a)
        - (long long )size >= 0LL) && (2147483648LL - (long long )a) - (long long
        )t >= 0LL) && (4294967287LL - (long long )b) - (long long )size >= 0LL) &&
        (4294967287LL - (long long )b) - (long long )t >= 0LL) && 1 == a) && a ==
        1)) || (((((((((((((((((((((((((3 <= b && 8 <= size) && b <= 2147483642) &&
        (-12LL + (long long )a) + (long long )size >= 0LL) && (-11LL + (long long
        )b) + (long long )size >= 0LL) && (-7LL + (long long )a) + (long long )b >=
        0LL) && (2147483640LL + (long long )size) + (long long )t >= 0LL) && (2147483644LL
        + (long long )a) + (long long )t >= 0LL) && (2147483645LL + (long long )b)
        + (long long )t >= 0LL) && (-5LL - (long long )b) + (long long )size >= 0LL)
        && (-4LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483652LL - (long long )a) + (long long
        )t >= 0LL) && (4294967290LL - (long long )b) + (long long )t >= 0LL) && (5LL
        + (long long )b) - (long long )size >= 0LL) && (2147483638LL + (long long
        )a) - (long long )b >= 0LL) && (2147483639LL + (long long )size) - (long long
        )t >= 0LL) && (2147483643LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483643LL + (long long )a) - (long long )t >= 0LL) && (2147483644LL +
        (long long )b) - (long long )t >= 0LL) && (2147483646LL - (long long )a) -
        (long long )b >= 0LL) && (2147483651LL - (long long )a) - (long long )size
        >= 0LL) && (2147483651LL - (long long )a) - (long long )t >= 0LL) && (4294967289LL
        - (long long )b) - (long long )size >= 0LL) && (4294967289LL - (long long
        )b) - (long long )t >= 0LL) && a == 4)) || ((((((((((((((((((((((((((0 <=
        b && 6 <= size) && b <= 2147483641) && (-7LL + (long long )a) + (long long
        )size >= 0LL) && (-6LL + (long long )b) + (long long )size >= 0LL) && (-1LL
        + (long long )a) + (long long )b >= 0LL) && (2147483642LL + (long long )size)
        + (long long )t >= 0LL) && (2147483647LL + (long long )a) + (long long )t
        >= 0LL) && (2147483648LL + (long long )b) + (long long )t >= 0LL) && (-6LL
        - (long long )b) + (long long )size >= 0LL) && (-5LL - (long long )a) + (long
        long )size >= 0LL) && (1LL - (long long )a) + (long long )b >= 0LL) && (2147483649LL
        - (long long )a) + (long long )t >= 0LL) && (4294967289LL - (long long )b)
        + (long long )t >= 0LL) && (6LL + (long long )b) - (long long )size >= 0LL)
        && (2147483640LL + (long long )a) - (long long )b >= 0LL) && (2147483641LL
        + (long long )size) - (long long )t >= 0LL) && (2147483646LL + (long long
        )a) - (long long )size >= 0LL) && (2147483646LL + (long long )a) - (long long
        )t >= 0LL) && (2147483647LL + (long long )b) - (long long )t >= 0LL) && (2147483642LL
        - (long long )a) - (long long )b >= 0LL) && (2147483648LL - (long long )a)
        - (long long )size >= 0LL) && (2147483648LL - (long long )a) - (long long
        )t >= 0LL) && (4294967288LL - (long long )b) - (long long )size >= 0LL) &&
        (4294967288LL - (long long )b) - (long long )t >= 0LL) && 1 == a) && a ==
        1)) || (((((((((((((((((((((((((3 <= b && 7 <= size) && b <= 2147483643) &&
        (-11LL + (long long )a) + (long long )size >= 0LL) && (-10LL + (long long
        )b) + (long long )size >= 0LL) && (-7LL + (long long )a) + (long long )b >=
        0LL) && (2147483641LL + (long long )size) + (long long )t >= 0LL) && (2147483644LL
        + (long long )a) + (long long )t >= 0LL) && (2147483645LL + (long long )b)
        + (long long )t >= 0LL) && (-4LL - (long long )b) + (long long )size >= 0LL)
        && (-3LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483652LL - (long long )a) + (long long
        )t >= 0LL) && (4294967291LL - (long long )b) + (long long )t >= 0LL) && (4LL
        + (long long )b) - (long long )size >= 0LL) && (2147483639LL + (long long
        )a) - (long long )b >= 0LL) && (2147483640LL + (long long )size) - (long long
        )t >= 0LL) && (2147483643LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483643LL + (long long )a) - (long long )t >= 0LL) && (2147483644LL +
        (long long )b) - (long long )t >= 0LL) && (2147483647LL - (long long )a) -
        (long long )b >= 0LL) && (2147483651LL - (long long )a) - (long long )size
        >= 0LL) && (2147483651LL - (long long )a) - (long long )t >= 0LL) && (4294967290LL
        - (long long )b) - (long long )size >= 0LL) && (4294967290LL - (long long
        )b) - (long long )t >= 0LL) && a == 4)) || ((((((((((((((((((((((((((0 <=
        b && 5 <= size) && b <= 2147483642) && (-6LL + (long long )a) + (long long
        )size >= 0LL) && (-5LL + (long long )b) + (long long )size >= 0LL) && (-1LL
        + (long long )a) + (long long )b >= 0LL) && (2147483643LL + (long long )size)
        + (long long )t >= 0LL) && (2147483647LL + (long long )a) + (long long )t
        >= 0LL) && (2147483648LL + (long long )b) + (long long )t >= 0LL) && (-5LL
        - (long long )b) + (long long )size >= 0LL) && (-4LL - (long long )a) + (long
        long )size >= 0LL) && (1LL - (long long )a) + (long long )b >= 0LL) && (2147483649LL
        - (long long )a) + (long long )t >= 0LL) && (4294967290LL - (long long )b)
        + (long long )t >= 0LL) && (5LL + (long long )b) - (long long )size >= 0LL)
        && (2147483641LL + (long long )a) - (long long )b >= 0LL) && (2147483642LL
        + (long long )size) - (long long )t >= 0LL) && (2147483646LL + (long long
        )a) - (long long )size >= 0LL) && (2147483646LL + (long long )a) - (long long
        )t >= 0LL) && (2147483647LL + (long long )b) - (long long )t >= 0LL) && (2147483643LL
        - (long long )a) - (long long )b >= 0LL) && (2147483648LL - (long long )a)
        - (long long )size >= 0LL) && (2147483648LL - (long long )a) - (long long
        )t >= 0LL) && (4294967289LL - (long long )b) - (long long )size >= 0LL) &&
        (4294967289LL - (long long )b) - (long long )t >= 0LL) && 1 == a) && a ==
        1)) || (((((((((((((((((((((((((3 <= b && 6 <= size) && b <= 2147483644) &&
        (-10LL + (long long )a) + (long long )size >= 0LL) && (-9LL + (long long )b)
        + (long long )size >= 0LL) && (-7LL + (long long )a) + (long long )b >= 0LL)
        && (2147483642LL + (long long )size) + (long long )t >= 0LL) && (2147483644LL
        + (long long )a) + (long long )t >= 0LL) && (2147483645LL + (long long )b)
        + (long long )t >= 0LL) && (-3LL - (long long )b) + (long long )size >= 0LL)
        && (-2LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483652LL - (long long )a) + (long long
        )t >= 0LL) && (4294967292LL - (long long )b) + (long long )t >= 0LL) && (3LL
        + (long long )b) - (long long )size >= 0LL) && (2147483640LL + (long long
        )a) - (long long )b >= 0LL) && (2147483641LL + (long long )size) - (long long
        )t >= 0LL) && (2147483643LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483643LL + (long long )a) - (long long )t >= 0LL) && (2147483644LL +
        (long long )b) - (long long )t >= 0LL) && (2147483648LL - (long long )a) -
        (long long )b >= 0LL) && (2147483651LL - (long long )a) - (long long )size
        >= 0LL) && (2147483651LL - (long long )a) - (long long )t >= 0LL) && (4294967291LL
        - (long long )b) - (long long )size >= 0LL) && (4294967291LL - (long long
        )b) - (long long )t >= 0LL) && a == 4)) || ((((((((((((((((((((((((((0 <=
        b && 4 <= size) && b <= 2147483643) && (-5LL + (long long )a) + (long long
        )size >= 0LL) && (-4LL + (long long )b) + (long long )size >= 0LL) && (-1LL
        + (long long )a) + (long long )b >= 0LL) && (2147483644LL + (long long )size)
        + (long long )t >= 0LL) && (2147483647LL + (long long )a) + (long long )t
        >= 0LL) && (2147483648LL + (long long )b) + (long long )t >= 0LL) && (-4LL
        - (long long )b) + (long long )size >= 0LL) && (-3LL - (long long )a) + (long
        long )size >= 0LL) && (1LL - (long long )a) + (long long )b >= 0LL) && (2147483649LL
        - (long long )a) + (long long )t >= 0LL) && (4294967291LL - (long long )b)
        + (long long )t >= 0LL) && (4LL + (long long )b) - (long long )size >= 0LL)
        && (2147483642LL + (long long )a) - (long long )b >= 0LL) && (2147483643LL
        + (long long )size) - (long long )t >= 0LL) && (2147483646LL + (long long
        )a) - (long long )size >= 0LL) && (2147483646LL + (long long )a) - (long long
        )t >= 0LL) && (2147483647LL + (long long )b) - (long long )t >= 0LL) && (2147483644LL
        - (long long )a) - (long long )b >= 0LL) && (2147483648LL - (long long )a)
        - (long long )size >= 0LL) && (2147483648LL - (long long )a) - (long long
        )t >= 0LL) && (4294967290LL - (long long )b) - (long long )size >= 0LL) &&
        (4294967290LL - (long long )b) - (long long )t >= 0LL) && 1 == a) && a ==
        1)) || (((((((((((((((((((((((((3 <= b && 5 <= size) && b <= 2147483645) &&
        (-9LL + (long long )a) + (long long )size >= 0LL) && (-8LL + (long long )b)
        + (long long )size >= 0LL) && (-7LL + (long long )a) + (long long )b >= 0LL)
        && (2147483643LL + (long long )size) + (long long )t >= 0LL) && (2147483644LL
        + (long long )a) + (long long )t >= 0LL) && (2147483645LL + (long long )b)
        + (long long )t >= 0LL) && (-2LL - (long long )b) + (long long )size >= 0LL)
        && (-1LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483652LL - (long long )a) + (long long
        )t >= 0LL) && (4294967293LL - (long long )b) + (long long )t >= 0LL) && (2LL
        + (long long )b) - (long long )size >= 0LL) && (2147483641LL + (long long
        )a) - (long long )b >= 0LL) && (2147483642LL + (long long )size) - (long long
        )t >= 0LL) && (2147483643LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483643LL + (long long )a) - (long long )t >= 0LL) && (2147483644LL +
        (long long )b) - (long long )t >= 0LL) && (2147483649LL - (long long )a) -
        (long long )b >= 0LL) && (2147483651LL - (long long )a) - (long long )size
        >= 0LL) && (2147483651LL - (long long )a) - (long long )t >= 0LL) && (4294967292LL
        - (long long )b) - (long long )size >= 0LL) && (4294967292LL - (long long
        )b) - (long long )t >= 0LL) && a == 4)) || ((((((((((((((((((((((((((0 <=
        b && 3 <= size) && b <= 2147483644) && (-4LL + (long long )a) + (long long
        )size >= 0LL) && (-3LL + (long long )b) + (long long )size >= 0LL) && (-1LL
        + (long long )a) + (long long )b >= 0LL) && (2147483645LL + (long long )size)
        + (long long )t >= 0LL) && (2147483647LL + (long long )a) + (long long )t
        >= 0LL) && (2147483648LL + (long long )b) + (long long )t >= 0LL) && (-3LL
        - (long long )b) + (long long )size >= 0LL) && (-2LL - (long long )a) + (long
        long )size >= 0LL) && (1LL - (long long )a) + (long long )b >= 0LL) && (2147483649LL
        - (long long )a) + (long long )t >= 0LL) && (4294967292LL - (long long )b)
        + (long long )t >= 0LL) && (3LL + (long long )b) - (long long )size >= 0LL)
        && (2147483643LL + (long long )a) - (long long )b >= 0LL) && (2147483644LL
        + (long long )size) - (long long )t >= 0LL) && (2147483646LL + (long long
        )a) - (long long )size >= 0LL) && (2147483646LL + (long long )a) - (long long
        )t >= 0LL) && (2147483647LL + (long long )b) - (long long )t >= 0LL) && (2147483645LL
        - (long long )a) - (long long )b >= 0LL) && (2147483648LL - (long long )a)
        - (long long )size >= 0LL) && (2147483648LL - (long long )a) - (long long
        )t >= 0LL) && (4294967291LL - (long long )b) - (long long )size >= 0LL) &&
        (4294967291LL - (long long )b) - (long long )t >= 0LL) && 1 == a) && a ==
        1)) || (((((((((((((((((((((((((4 <= b && 5 <= size) && b <= 2147483646) &&
        (-9LL + (long long )a) + (long long )size >= 0LL) && (-9LL + (long long )b)
        + (long long )size >= 0LL) && (-8LL + (long long )a) + (long long )b >= 0LL)
        && (2147483643LL + (long long )size) + (long long )t >= 0LL) && (2147483644LL
        + (long long )a) + (long long )t >= 0LL) && (2147483644LL + (long long )b)
        + (long long )t >= 0LL) && (-1LL - (long long )a) + (long long )size >= 0LL)
        && (-1LL - (long long )b) + (long long )size >= 0LL) && (0LL - (long long
        )a) + (long long )b >= 0LL) && (2147483652LL - (long long )a) + (long long
        )t >= 0LL) && (4294967294LL - (long long )b) + (long long )t >= 0LL) && (1LL
        + (long long )b) - (long long )size >= 0LL) && (2147483642LL + (long long
        )size) - (long long )t >= 0LL) && (2147483642LL + (long long )a) - (long long
        )b >= 0LL) && (2147483643LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483643LL + (long long )a) - (long long )t >= 0LL) && (2147483643LL +
        (long long )b) - (long long )t >= 0LL) && (2147483650LL - (long long )a) -
        (long long )b >= 0LL) && (2147483651LL - (long long )a) - (long long )size
        >= 0LL) && (2147483651LL - (long long )a) - (long long )t >= 0LL) && (4294967293LL
        - (long long )b) - (long long )size >= 0LL) && (4294967293LL - (long long
        )b) - (long long )t >= 0LL) && a == 4)) || ((((((((((((((((((((((((((0 <=
        b && 2 <= size) && b <= 2147483645) && (-3LL + (long long )a) + (long long
        )size >= 0LL) && (-2LL + (long long )b) + (long long )size >= 0LL) && (-1LL
        + (long long )a) + (long long )b >= 0LL) && (2147483646LL + (long long )size)
        + (long long )t >= 0LL) && (2147483647LL + (long long )a) + (long long )t
        >= 0LL) && (2147483648LL + (long long )b) + (long long )t >= 0LL) && (-2LL
        - (long long )b) + (long long )size >= 0LL) && (-1LL - (long long )a) + (long
        long )size >= 0LL) && (1LL - (long long )a) + (long long )b >= 0LL) && (2147483649LL
        - (long long )a) + (long long )t >= 0LL) && (4294967293LL - (long long )b)
        + (long long )t >= 0LL) && (2LL + (long long )b) - (long long )size >= 0LL)
        && (2147483644LL + (long long )a) - (long long )b >= 0LL) && (2147483645LL
        + (long long )size) - (long long )t >= 0LL) && (2147483646LL + (long long
        )a) - (long long )size >= 0LL) && (2147483646LL + (long long )a) - (long long
        )t >= 0LL) && (2147483647LL + (long long )b) - (long long )t >= 0LL) && (2147483646LL
        - (long long )a) - (long long )b >= 0LL) && (2147483648LL - (long long )a)
        - (long long )size >= 0LL) && (2147483648LL - (long long )a) - (long long
        )t >= 0LL) && (4294967292LL - (long long )b) - (long long )size >= 0LL) &&
        (4294967292LL - (long long )b) - (long long )t >= 0LL) && 1 == a) && a ==
        1)) || (((((((((((((((((((((((((2 <= b && 14 <= size) && b <= 2147483635)
        && (-17LL + (long long )a) + (long long )size >= 0LL) && (-16LL + (long long
        )b) + (long long )size >= 0LL) && (-5LL + (long long )a) + (long long )b >=
        0LL) && (2147483634LL + (long long )size) + (long long )t >= 0LL) && (2147483645LL
        + (long long )a) + (long long )t >= 0LL) && (2147483646LL + (long long )b)
        + (long long )t >= 0LL) && (-12LL - (long long )b) + (long long )size >= 0LL)
        && (-11LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483651LL - (long long )a) + (long long
        )t >= 0LL) && (4294967283LL - (long long )b) + (long long )t >= 0LL) && (2147483632LL
        + (long long )a) - (long long )b >= 0LL) && (2147483633LL + (long long )size)
        - (long long )t >= 0LL) && (2147483644LL + (long long )a) - (long long )size
        >= 0LL) && (2147483644LL + (long long )a) - (long long )t >= 0LL) && (2147483645LL
        + (long long )b) - (long long )size >= 0LL) && (2147483645LL + (long long
        )b) - (long long )t >= 0LL) && (2147483638LL - (long long )a) - (long long
        )b >= 0LL) && (2147483650LL - (long long )a) - (long long )size >= 0LL) &&
        (2147483650LL - (long long )a) - (long long )t >= 0LL) && (4294967282LL -
        (long long )b) - (long long )size >= 0LL) && (4294967282LL - (long long )b)
        - (long long )t >= 0LL) && a == 3)) || ((((((((((((((((((((((((((1 <= b &&
        2 <= size) && b <= 2147483646) && (-3LL + (long long )a) + (long long )size
        >= 0LL) && (-3LL + (long long )b) + (long long )size >= 0LL) && (-2LL + (long
        long )a) + (long long )b >= 0LL) && (2147483646LL + (long long )size) + (long
        long )t >= 0LL) && (2147483647LL + (long long )a) + (long long )t >= 0LL)
        && (2147483647LL + (long long )b) + (long long )t >= 0LL) && (-1LL - (long
        long )a) + (long long )size >= 0LL) && (-1LL - (long long )b) + (long long
        )size >= 0LL) && (0LL - (long long )a) + (long long )b >= 0LL) && (2147483649LL
        - (long long )a) + (long long )t >= 0LL) && (4294967294LL - (long long )b)
        + (long long )t >= 0LL) && (1LL + (long long )b) - (long long )size >= 0LL)
        && (2147483645LL + (long long )size) - (long long )t >= 0LL) && (2147483645LL
        + (long long )a) - (long long )b >= 0LL) && (2147483646LL + (long long )a)
        - (long long )size >= 0LL) && (2147483646LL + (long long )a) - (long long
        )t >= 0LL) && (2147483646LL + (long long )b) - (long long )t >= 0LL) && (2147483647LL
        - (long long )a) - (long long )b >= 0LL) && (2147483648LL - (long long )a)
        - (long long )size >= 0LL) && (2147483648LL - (long long )a) - (long long
        )t >= 0LL) && (4294967293LL - (long long )b) - (long long )size >= 0LL) &&
        (4294967293LL - (long long )b) - (long long )t >= 0LL) && 1 == a) && a ==
        1)) || (((((((((((((((((((((((((2 <= b && 13 <= size) && b <= 2147483636)
        && (-16LL + (long long )a) + (long long )size >= 0LL) && (-15LL + (long long
        )b) + (long long )size >= 0LL) && (-5LL + (long long )a) + (long long )b >=
        0LL) && (2147483635LL + (long long )size) + (long long )t >= 0LL) && (2147483645LL
        + (long long )a) + (long long )t >= 0LL) && (2147483646LL + (long long )b)
        + (long long )t >= 0LL) && (-11LL - (long long )b) + (long long )size >= 0LL)
        && (-10LL - (long long )a) + (long long )size >= 0LL) && (1LL - (long long
        )a) + (long long )b >= 0LL) && (2147483651LL - (long long )a) + (long long
        )t >= 0LL) && (4294967284LL - (long long )b) + (long long )t >= 0LL) && (11LL
        + (long long )b) - (long long )size >= 0LL) && (2147483633LL + (long long
        )a) - (long long )b >= 0LL) && (2147483634LL + (long long )size) - (long long
        )t >= 0LL) && (2147483644LL + (long long )a) - (long long )size >= 0LL) &&
        (2147483644LL + (long long )a) - (long long )t >= 0LL) && (2147483645LL +
        (long long )b) - (long long )t >= 0LL) && (2147483639LL - (long long )a) -
        (long long )b >= 0LL) && (2147483650LL - (long long )a) - (long long )size
        >= 0LL) && (2147483650LL - (long long )a) - (long long )t >= 0LL) && (4294967283LL
        - (long long )b) - (long long )size >= 0LL) && (4294967283LL - (long long
        )b) - (long long )t >= 0LL) && a == 3)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 76
        column: 5
        function: q1
      value: 2 <= argc
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 76
        column: 5
        function: q1
      value: (2147483646LL + (long long )argc) + (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 76
        column: 5
        function: q1
      value: (2147483646LL + (long long )argc) + (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 76
        column: 5
        function: q1
      value: (4294967296LL + (long long )r) + (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 76
        column: 5
        function: q1
      value: (2147483645LL - (long long )N) + (long long )argc >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 76
        column: 5
        function: q1
      value: (4294967295LL - (long long )N) + (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 76
        column: 5
        function: q1
      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/loops/bubble_sort-1.c
        line: 76
        column: 5
        function: q1
      value: (4294967295LL - (long long )r) + (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 76
        column: 5
        function: q1
      value: (2147483645LL + (long long )argc) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 76
        column: 5
        function: q1
      value: (2147483645LL + (long long )argc) - (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 76
        column: 5
        function: q1
      value: (4294967295LL + (long long )r) - (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 76
        column: 5
        function: q1
      value: (4294967294LL - (long long )N) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 76
        column: 5
        function: q1
      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/loops/bubble_sort-1.c
        line: 76
        column: 5
        function: q1
      value: (4294967294LL - (long long )r) - (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 76
        column: 5
        function: q1
      value: (((long long )N - (long long )i >= 0LL && a[r] == temp) && (((((((((((((((((((((((-2147483640
        <= r && 4 <= N) && 4 <= i) && (-8LL + (long long )N) + (long long )i >= 0LL)
        && (-6LL + (long long )argc) + (long long )i >= 0LL) && (-6LL + (long long
        )N) + (long long )argc >= 0LL) && (2147483644LL + (long long )N) + (long long
        )r >= 0LL) && (2147483644LL + (long long )N) + (long long )temp >= 0LL) &&
        (2147483644LL + (long long )i) + (long long )r >= 0LL) && (2147483644LL +
        (long long )i) + (long long )temp >= 0LL) && (2147483643LL - (long long )N)
        + (long long )i >= 0LL) && (4294967295LL - (long long )i) + (long long )r
        >= 0LL) && (4294967295LL - (long long )i) + (long long )temp >= 0LL) && (2147483643LL
        + (long long )N) - (long long )r >= 0LL) && (2147483643LL + (long long )N)
        - (long long )temp >= 0LL) && (2147483643LL + (long long )i) - (long long
        )r >= 0LL) && (2147483643LL + (long long )i) - (long long )temp >= 0LL) &&
        (2147483645LL + (long long )argc) - (long long )i >= 0LL) && (4294967294LL
        - (long long )N) - (long long )i >= 0LL) && (4294967294LL - (long long )i)
        - (long long )r >= 0LL) && (4294967294LL - (long long )i) - (long long )temp
        >= 0LL) || (((((((((((((((((((((-2147483642 <= r && 3 <= N) && r <= 2147483646)
        && (-6LL + (long long )N) + (long long )i >= 0LL) && (-5LL + (long long )argc)
        + (long long )i >= 0LL) && (-5LL + (long long )N) + (long long )argc >= 0LL)
        && (2147483645LL + (long long )N) + (long long )r >= 0LL) && (2147483645LL
        + (long long )N) + (long long )temp >= 0LL) && (2147483645LL + (long long
        )i) + (long long )r >= 0LL) && (2147483645LL + (long long )i) + (long long
        )temp >= 0LL) && (2147483644LL - (long long )N) + (long long )i >= 0LL) &&
        (2147483651LL - (long long )i) + (long long )r >= 0LL) && (2147483651LL -
        (long long )i) + (long long )temp >= 0LL) && (1LL + (long long )argc) - (long
        long )i >= 0LL) && (2147483644LL + (long long )N) - (long long )r >= 0LL)
        && (2147483644LL + (long long )N) - (long long )temp >= 0LL) && (2147483644LL
        + (long long )i) - (long long )r >= 0LL) && (2147483644LL + (long long )i)
        - (long long )temp >= 0LL) && (2147483650LL - (long long )N) - (long long
        )i >= 0LL) && (2147483650LL - (long long )i) - (long long )r >= 0LL) && (2147483650LL
        - (long long )i) - (long long )temp >= 0LL) && i == 3)) || (((((((((((((((((((((-2147483644
        <= r && 2 <= N) && r <= 2147483646) && (-4LL + (long long )argc) + (long long
        )i >= 0LL) && (-4LL + (long long )N) + (long long )argc >= 0LL) && (-4LL +
        (long long )N) + (long long )i >= 0LL) && (2147483646LL + (long long )N) +
        (long long )r >= 0LL) && (2147483646LL + (long long )N) + (long long )temp
        >= 0LL) && (2147483646LL + (long long )i) + (long long )r >= 0LL) && (2147483646LL
        + (long long )i) + (long long )temp >= 0LL) && (2147483645LL - (long long
        )N) + (long long )i >= 0LL) && (2147483650LL - (long long )i) + (long long
        )r >= 0LL) && (2147483650LL - (long long )i) + (long long )temp >= 0LL) &&
        (2147483645LL + (long long )N) - (long long )r >= 0LL) && (2147483645LL +
        (long long )N) - (long long )temp >= 0LL) && (2147483645LL + (long long )i)
        - (long long )r >= 0LL) && (2147483645LL + (long long )i) - (long long )temp
        >= 0LL) && (2147483649LL - (long long )N) - (long long )i >= 0LL) && (2147483649LL
        - (long long )i) - (long long )r >= 0LL) && (2147483649LL - (long long )i)
        - (long long )temp >= 0LL) && (long long )argc - (long long )i >= 0LL) &&
        i == 2)) || (((((((((((((((((((((-2147483646 <= r && 1 <= N) && r <= 2147483646)
        && (-3LL + (long long )argc) + (long long )i >= 0LL) && (-3LL + (long long
        )N) + (long long )argc >= 0LL) && (-2LL + (long long )N) + (long long )i >=
        0LL) && (2147483647LL + (long long )N) + (long long )r >= 0LL) && (2147483647LL
        + (long long )N) + (long long )temp >= 0LL) && (2147483647LL + (long long
        )i) + (long long )r >= 0LL) && (2147483647LL + (long long )i) + (long long
        )temp >= 0LL) && (2147483646LL - (long long )N) + (long long )i >= 0LL) &&
        (2147483649LL - (long long )i) + (long long )r >= 0LL) && (2147483649LL -
        (long long )i) + (long long )temp >= 0LL) && (-1LL + (long long )argc) - (long
        long )i >= 0LL) && (2147483646LL + (long long )N) - (long long )r >= 0LL)
        && (2147483646LL + (long long )N) - (long long )temp >= 0LL) && (2147483646LL
        + (long long )i) - (long long )r >= 0LL) && (2147483646LL + (long long )i)
        - (long long )temp >= 0LL) && (2147483648LL - (long long )N) - (long long
        )i >= 0LL) && (2147483648LL - (long long )i) - (long long )r >= 0LL) && (2147483648LL
        - (long long )i) - (long long )temp >= 0LL) && i == 1))) || (((((((((((((((((((((-2LL
        + (long long )argc) + (long long )i >= 0LL && (2147483646LL + (long long )N)
        + (long long )argc >= 0LL) && (2147483648LL + (long long )N) + (long long
        )i >= 0LL) && (2147483648LL + (long long )i) + (long long )r >= 0LL) && (2147483648LL
        + (long long )i) + (long long )temp >= 0LL) && (4294967296LL + (long long
        )N) + (long long )r >= 0LL) && (4294967296LL + (long long )N) + (long long
        )temp >= 0LL) && (2147483647LL - (long long )N) + (long long )i >= 0LL) &&
        (2147483648LL - (long long )i) + (long long )r >= 0LL) && (2147483648LL -
        (long long )i) + (long long )temp >= 0LL) && (-2LL + (long long )argc) - (long
        long )i >= 0LL) && (2147483647LL + (long long )i) - (long long )r >= 0LL)
        && (2147483647LL + (long long )i) - (long long )temp >= 0LL) && (2147483648LL
        + (long long )N) - (long long )i >= 0LL) && (4294967295LL + (long long )N)
        - (long long )r >= 0LL) && (4294967295LL + (long long )N) - (long long )temp
        >= 0LL) && (2147483647LL - (long long )N) - (long long )i >= 0LL) && (2147483647LL
        - (long long )i) - (long long )r >= 0LL) && (2147483647LL - (long long )i)
        - (long long )temp >= 0LL) && 0 == i) && i == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 18
        column: 2
        function: bubblesort
      value: (4294967295LL - (long long )size) + (long long )t >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 18
        column: 2
        function: bubblesort
      value: (4294967294LL - (long long )size) - (long long )t >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 18
        column: 2
        function: bubblesort
      value: (((((-2LL - (long long )b) + (long long )size >= 0LL && (0LL - (long
        long )a) + (long long )size >= 0LL) && (2LL - (long long )a) + (long long
        )b >= 0LL) && (-2LL + (long long )a) - (long long )b >= 0LL) && (((((((((((((((((((((((3
        <= size && (-6LL + (long long )a) + (long long )size >= 0LL) && (-4LL + (long
        long )a) + (long long )b >= 0LL) && (-4LL + (long long )b) + (long long )size
        >= 0LL) && (2147483645LL + (long long )size) + (long long )t >= 0LL) && (2147483645LL
        + (long long )a) + (long long )t >= 0LL) && (2147483647LL + (long long )b)
        + (long long )t >= 0LL) && (2147483649LL - (long long )b) + (long long )t
        >= 0LL) && (2147483651LL - (long long )a) + (long long )t >= 0LL) && (2147483644LL
        + (long long )size) - (long long )t >= 0LL) && (2147483644LL + (long long
        )a) - (long long )size >= 0LL) && (2147483644LL + (long long )a) - (long long
        )t >= 0LL) && (2147483646LL + (long long )b) - (long long )size >= 0LL) &&
        (2147483646LL + (long long )b) - (long long )t >= 0LL) && (4LL - (long long
        )a) - (long long )b >= 0LL) && (2147483648LL - (long long )b) - (long long
        )size >= 0LL) && (2147483648LL - (long long )b) - (long long )t >= 0LL) &&
        (2147483650LL - (long long )a) - (long long )size >= 0LL) && (2147483650LL
        - (long long )a) - (long long )t >= 0LL) && a == 3) && b == 1) || (((((((((((((((((((((3
        <= b && 5 <= size) && 5 <= a) && b <= 2147483645) && (-10LL + (long long )a)
        + (long long )size >= 0LL) && (-8LL + (long long )a) + (long long )b >= 0LL)
        && (-8LL + (long long )b) + (long long )size >= 0LL) && (2147483643LL + (long
        long )size) + (long long )t >= 0LL) && (2147483643LL + (long long )a) + (long
        long )t >= 0LL) && (2147483645LL + (long long )b) + (long long )t >= 0LL)
        && (4294967293LL - (long long )b) + (long long )t >= 0LL) && (4294967295LL
        - (long long )a) + (long long )t >= 0LL) && (2147483642LL + (long long )size)
        - (long long )t >= 0LL) && (2147483642LL + (long long )a) - (long long )size
        >= 0LL) && (2147483642LL + (long long )a) - (long long )t >= 0LL) && (2147483644LL
        + (long long )b) - (long long )size >= 0LL) && (2147483644LL + (long long
        )b) - (long long )t >= 0LL) && (4294967292LL - (long long )a) - (long long
        )b >= 0LL) && (4294967292LL - (long long )b) - (long long )size >= 0LL) &&
        (4294967292LL - (long long )b) - (long long )t >= 0LL) && (4294967294LL -
        (long long )a) - (long long )size >= 0LL) && (4294967294LL - (long long )a)
        - (long long )t >= 0LL)) || ((((((((((((((((((((2 <= size && (-4LL + (long
        long )a) + (long long )size >= 0LL) && (-2LL + (long long )a) + (long long
        )b >= 0LL) && (-2LL + (long long )b) + (long long )size >= 0LL) && (2147483646LL
        + (long long )size) + (long long )t >= 0LL) && (2147483646LL + (long long
        )a) + (long long )t >= 0LL) && (2147483648LL + (long long )b) + (long long
        )t >= 0LL) && (2147483648LL - (long long )b) + (long long )t >= 0LL) && (2147483650LL
        - (long long )a) + (long long )t >= 0LL) && (2147483645LL + (long long )size)
        - (long long )t >= 0LL) && (2147483645LL + (long long )a) - (long long )size
        >= 0LL) && (2147483645LL + (long long )a) - (long long )t >= 0LL) && (2147483647LL
        + (long long )b) - (long long )size >= 0LL) && (2147483647LL + (long long
        )b) - (long long )t >= 0LL) && (2LL - (long long )a) - (long long )b >= 0LL)
        && (2147483647LL - (long long )b) - (long long )size >= 0LL) && (2147483647LL
        - (long long )b) - (long long )t >= 0LL) && (2147483649LL - (long long )a)
        - (long long )size >= 0LL) && (2147483649LL - (long long )a) - (long long
        )t >= 0LL) && a == 2) && b == 0)) || ((((((((((((((((((((4 <= size && (-8LL
        + (long long )a) + (long long )size >= 0LL) && (-6LL + (long long )a) + (long
        long )b >= 0LL) && (-6LL + (long long )b) + (long long )size >= 0LL) && (2147483644LL
        + (long long )size) + (long long )t >= 0LL) && (2147483644LL + (long long
        )a) + (long long )t >= 0LL) && (2147483646LL + (long long )b) + (long long
        )t >= 0LL) && (2147483650LL - (long long )b) + (long long )t >= 0LL) && (2147483652LL
        - (long long )a) + (long long )t >= 0LL) && (2147483643LL + (long long )size)
        - (long long )t >= 0LL) && (2147483643LL + (long long )a) - (long long )size
        >= 0LL) && (2147483643LL + (long long )a) - (long long )t >= 0LL) && (2147483645LL
        + (long long )b) - (long long )size >= 0LL) && (2147483645LL + (long long
        )b) - (long long )t >= 0LL) && (6LL - (long long )a) - (long long )b >= 0LL)
        && (2147483649LL - (long long )b) - (long long )size >= 0LL) && (2147483649LL
        - (long long )b) - (long long )t >= 0LL) && (2147483651LL - (long long )a)
        - (long long )size >= 0LL) && (2147483651LL - (long long )a) - (long long
        )t >= 0LL) && a == 4) && b == 2))) || ((((((((((((((((((((((((2147483647LL
        + (long long )a) + (long long )size >= 0LL && (2147483647LL + (long long )a)
        + (long long )b >= 0LL) && (2147483647LL + (long long )a) + (long long )t
        >= 0LL) && (4294967296LL + (long long )size) + (long long )t >= 0LL) && (4294967296LL
        + (long long )b) + (long long )size >= 0LL) && (4294967296LL + (long long
        )b) + (long long )t >= 0LL) && (2147483649LL - (long long )a) + (long long
        )size >= 0LL) && (2147483649LL - (long long )a) + (long long )b >= 0LL) &&
        (2147483649LL - (long long )a) + (long long )t >= 0LL) && (4294967295LL -
        (long long )b) + (long long )size >= 0LL) && (4294967295LL - (long long )b)
        + (long long )t >= 0LL) && (2147483646LL + (long long )a) - (long long )size
        >= 0LL) && (2147483646LL + (long long )a) - (long long )b >= 0LL) && (2147483646LL
        + (long long )a) - (long long )t >= 0LL) && (4294967295LL + (long long )size)
        - (long long )t >= 0LL) && (4294967295LL + (long long )b) - (long long )size
        >= 0LL) && (4294967295LL + (long long )b) - (long long )t >= 0LL) && (2147483648LL
        - (long long )a) - (long long )size >= 0LL) && (2147483648LL - (long long
        )a) - (long long )b >= 0LL) && (2147483648LL - (long long )a) - (long long
        )t >= 0LL) && (4294967294LL - (long long )b) - (long long )size >= 0LL) &&
        (4294967294LL - (long long )b) - (long long )t >= 0LL) && 1 == a) && a ==
        1)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 74
        column: 4
        function: q1
      value: 2 <= argc
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 74
        column: 4
        function: q1
      value: (2147483646LL + (long long )argc) + (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 74
        column: 4
        function: q1
      value: (2147483646LL + (long long )argc) + (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 74
        column: 4
        function: q1
      value: (4294967296LL + (long long )r) + (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 74
        column: 4
        function: q1
      value: (2147483645LL - (long long )N) + (long long )argc >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 74
        column: 4
        function: q1
      value: (4294967295LL - (long long )N) + (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 74
        column: 4
        function: q1
      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/loops/bubble_sort-1.c
        line: 74
        column: 4
        function: q1
      value: (4294967295LL - (long long )r) + (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 74
        column: 4
        function: q1
      value: (2147483645LL + (long long )argc) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 74
        column: 4
        function: q1
      value: (2147483645LL + (long long )argc) - (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 74
        column: 4
        function: q1
      value: (4294967295LL + (long long )r) - (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 74
        column: 4
        function: q1
      value: (4294967294LL - (long long )N) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 74
        column: 4
        function: q1
      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/loops/bubble_sort-1.c
        line: 74
        column: 4
        function: q1
      value: (4294967294LL - (long long )r) - (long long )temp >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loops/bubble_sort-1.c
        line: 74
        column: 4
        function: q1
      value: ((long long )N - (long long )i >= 0LL && ((((((((((((((((((((((4 <= N
        && 4 <= i) && (-8LL + (long long )N) + (long long )i >= 0LL) && (-6LL + (long
        long )argc) + (long long )i >= 0LL) && (-6LL + (long long )N) + (long long
        )argc >= 0LL) && (2147483644LL + (long long )N) + (long long )r >= 0LL) &&
        (2147483644LL + (long long )N) + (long long )temp >= 0LL) && (2147483644LL
        + (long long )i) + (long long )r >= 0LL) && (2147483644LL + (long long )i)
        + (long long )temp >= 0LL) && (2147483643LL - (long long )N) + (long long
        )i >= 0LL) && (4294967295LL - (long long )i) + (long long )r >= 0LL) && (4294967295LL
        - (long long )i) + (long long )temp >= 0LL) && (2147483643LL + (long long
        )N) - (long long )r >= 0LL) && (2147483643LL + (long long )N) - (long long
        )temp >= 0LL) && (2147483643LL + (long long )i) - (long long )r >= 0LL) &&
        (2147483643LL + (long long )i) - (long long )temp >= 0LL) && (2147483645LL
        + (long long )argc) - (long long )i >= 0LL) && (4294967294LL - (long long
        )N) - (long long )i >= 0LL) && (4294967294LL - (long long )i) - (long long
        )r >= 0LL) && (4294967294LL - (long long )i) - (long long )temp >= 0LL) ||
        (((((((((((((((((((3 <= N && (-6LL + (long long )N) + (long long )i >= 0LL)
        && (-5LL + (long long )argc) + (long long )i >= 0LL) && (-5LL + (long long
        )N) + (long long )argc >= 0LL) && (2147483645LL + (long long )N) + (long long
        )r >= 0LL) && (2147483645LL + (long long )N) + (long long )temp >= 0LL) &&
        (2147483645LL + (long long )i) + (long long )r >= 0LL) && (2147483645LL +
        (long long )i) + (long long )temp >= 0LL) && (2147483644LL - (long long )N)
        + (long long )i >= 0LL) && (2147483651LL - (long long )i) + (long long )r
        >= 0LL) && (2147483651LL - (long long )i) + (long long )temp >= 0LL) && (1LL
        + (long long )argc) - (long long )i >= 0LL) && (2147483644LL + (long long
        )N) - (long long )r >= 0LL) && (2147483644LL + (long long )N) - (long long
        )temp >= 0LL) && (2147483644LL + (long long )i) - (long long )r >= 0LL) &&
        (2147483644LL + (long long )i) - (long long )temp >= 0LL) && (2147483650LL
        - (long long )N) - (long long )i >= 0LL) && (2147483650LL - (long long )i)
        - (long long )r >= 0LL) && (2147483650LL - (long long )i) - (long long )temp
        >= 0LL) && i == 3)) || (((((((((((((((((((2 <= N && (-4LL + (long long )argc)
        + (long long )i >= 0LL) && (-4LL + (long long )N) + (long long )argc >= 0LL)
        && (-4LL + (long long )N) + (long long )i >= 0LL) && (2147483646LL + (long
        long )N) + (long long )r >= 0LL) && (2147483646LL + (long long )N) + (long
        long )temp >= 0LL) && (2147483646LL + (long long )i) + (long long )r >= 0LL)
        && (2147483646LL + (long long )i) + (long long )temp >= 0LL) && (2147483645LL
        - (long long )N) + (long long )i >= 0LL) && (2147483650LL - (long long )i)
        + (long long )r >= 0LL) && (2147483650LL - (long long )i) + (long long )temp
        >= 0LL) && (2147483645LL + (long long )N) - (long long )r >= 0LL) && (2147483645LL
        + (long long )N) - (long long )temp >= 0LL) && (2147483645LL + (long long
        )i) - (long long )r >= 0LL) && (2147483645LL + (long long )i) - (long long
        )temp >= 0LL) && (2147483649LL - (long long )N) - (long long )i >= 0LL) &&
        (2147483649LL - (long long )i) - (long long )r >= 0LL) && (2147483649LL -
        (long long )i) - (long long )temp >= 0LL) && (long long )argc - (long long
        )i >= 0LL) && i == 2)) || (((((((((((((((((((1 <= N && (-3LL + (long long
        )argc) + (long long )i >= 0LL) && (-3LL + (long long )N) + (long long )argc
        >= 0LL) && (-2LL + (long long )N) + (long long )i >= 0LL) && (2147483647LL
        + (long long )N) + (long long )r >= 0LL) && (2147483647LL + (long long )N)
        + (long long )temp >= 0LL) && (2147483647LL + (long long )i) + (long long
        )r >= 0LL) && (2147483647LL + (long long )i) + (long long )temp >= 0LL) &&
        (2147483646LL - (long long )N) + (long long )i >= 0LL) && (2147483649LL -
        (long long )i) + (long long )r >= 0LL) && (2147483649LL - (long long )i) +
        (long long )temp >= 0LL) && (-1LL + (long long )argc) - (long long )i >= 0LL)
        && (2147483646LL + (long long )N) - (long long )r >= 0LL) && (2147483646LL
        + (long long )N) - (long long )temp >= 0LL) && (2147483646LL + (long long
        )i) - (long long )r >= 0LL) && (2147483646LL + (long long )i) - (long long
        )temp >= 0LL) && (2147483648LL - (long long )N) - (long long )i >= 0LL) &&
        (2147483648LL - (long long )i) - (long long )r >= 0LL) && (2147483648LL -
        (long long )i) - (long long )temp >= 0LL) && i == 1))) || (((((((((((((((((((((-2LL
        + (long long )argc) + (long long )i >= 0LL && (2147483646LL + (long long )N)
        + (long long )argc >= 0LL) && (2147483648LL + (long long )N) + (long long
        )i >= 0LL) && (2147483648LL + (long long )i) + (long long )r >= 0LL) && (2147483648LL
        + (long long )i) + (long long )temp >= 0LL) && (4294967296LL + (long long
        )N) + (long long )r >= 0LL) && (4294967296LL + (long long )N) + (long long
        )temp >= 0LL) && (2147483647LL - (long long )N) + (long long )i >= 0LL) &&
        (2147483648LL - (long long )i) + (long long )r >= 0LL) && (2147483648LL -
        (long long )i) + (long long )temp >= 0LL) && (-2LL + (long long )argc) - (long
        long )i >= 0LL) && (2147483647LL + (long long )i) - (long long )r >= 0LL)
        && (2147483647LL + (long long )i) - (long long )temp >= 0LL) && (2147483648LL
        + (long long )N) - (long long )i >= 0LL) && (4294967295LL + (long long )N)
        - (long long )r >= 0LL) && (4294967295LL + (long long )N) - (long long )temp
        >= 0LL) && (2147483647LL - (long long )N) - (long long )i >= 0LL) && (2147483647LL
        - (long long )i) - (long long )r >= 0LL) && (2147483647LL - (long long )i)
        - (long long )temp >= 0LL) && 0 == i) && i == 0)
      format: c_expression
