- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 0845f9d9-2c03-4fc2-9b17-3ee249531353
    creation_time: 2025-03-22T16:55:56Z
    producer:
      name: Goblint
      version: heads/master-0-g66dff5a90-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp.json'' ''--disable'' ''witness.graphml.enabled''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/termination.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i: 3a0264b09ef9a10d2c073f3c86acc58c99a39f77c61d9fd7b5bb4f2dbe316f76
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(F end) )
  content:
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: 1U <= B
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: A <= 2147483646U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: B <= 2147483646U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: r <= 2147483646U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (-1LL + (long long )A) + (long long )B >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (-1LL + (long long )B) + (long long )q >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (-1LL + (long long )B) + (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (2147483647LL + (long long )B) + (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (2147483648LL + (long long )A) + (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (2147483648LL + (long long )k) + (long long )q >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (2147483648LL + (long long )k) + (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (2147483645LL - (long long )A) + (long long )B >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (2147483646LL - (long long )B) + (long long )q >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (2147483646LL - (long long )B) + (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (2147483647LL - (long long )k) + (long long )q >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (2147483647LL - (long long )k) + (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (4294967294LL - (long long )A) + (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (4294967294LL - (long long )B) + (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (long long )A + (long long )q >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (long long )A + (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (long long )q + (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (2147483645LL + (long long )B) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (2147483646LL + (long long )A) - (long long )B >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (2147483646LL + (long long )B) - (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (2147483647LL + (long long )A) - (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (4294967294LL + (long long )k) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (4294967292LL - (long long )A) - (long long )B >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (4294967292LL - (long long )A) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (4294967292LL - (long long )B) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (4294967293LL - (long long )A) - (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (4294967293LL - (long long )B) - (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (4294967293LL - (long long )k) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: (long long )A - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 25
        column: 5
        function: main
      value: ((-1LL + (long long )b) + (long long )q >= 0LL && (((((((((((((-1LL +
        (long long )B) + (long long )b >= 0LL && (2147483648LL + (long long )b) +
        (long long )k >= 0LL) && (2147483645LL - (long long )A) + (long long )q >=
        0LL) && (2147483646LL - (long long )A) + (long long )r >= 0LL) && (2147483646LL
        - (long long )A) + (long long )b >= 0LL) && (2147483646LL - (long long )B)
        + (long long )b >= 0LL) && (long long )A + (long long )b >= 0LL) && (long
        long )b + (long long )r >= 0LL) && (2147483645LL + (long long )q) - (long
        long )r >= 0LL) && (2147483646LL + (long long )b) - (long long )r >= 0LL)
        && (2147483647LL + (long long )b) - (long long )k >= 0LL) && (((((((((((4294967295LL
        - (long long )b) + (long long )q >= 0LL && (4294967295LL - (long long )b)
        + (long long )r >= 0LL) && (6442450943LL - (long long )b) + (long long )k
        >= 0LL) && (4294967294LL + (long long )B) - (long long )b >= 0LL) && (4294967295LL
        + (long long )A) - (long long )b >= 0LL) && (6442450941LL - (long long )A)
        - (long long )b >= 0LL) && (6442450941LL - (long long )B) - (long long )b
        >= 0LL) && (6442450941LL - (long long )b) - (long long )r >= 0LL) && (6442450942LL
        - (long long )b) - (long long )k >= 0LL) && (((((((((((((((((((((((((((((((((((((q
        <= 7U && b <= 536870911U) && (-4LL + (long long )B) + (long long )c >= 0LL)
        && (-3LL + (long long )A) + (long long )c >= 0LL) && (-3LL + (long long )b)
        + (long long )c >= 0LL) && (-3LL + (long long )c) + (long long )q >= 0LL)
        && (-3LL + (long long )c) + (long long )r >= 0LL) && (2147483645LL + (long
        long )c) + (long long )k >= 0LL) && (3LL - (long long )c) + (long long )q
        >= 0LL) && (3LL - (long long )c) + (long long )r >= 0LL) && (7LL - (long long
        )q) + (long long )r >= 0LL) && (2147483643LL - (long long )A) + (long long
        )c >= 0LL) && (2147483643LL - (long long )B) + (long long )c >= 0LL) && (2147483651LL
        - (long long )c) + (long long )k >= 0LL) && (4294967292LL - (long long )b)
        + (long long )c >= 0LL) && (2LL + (long long )B) - (long long )c >= 0LL) &&
        (3LL + (long long )A) - (long long )c >= 0LL) && (3LL + (long long )b) - (long
        long )c >= 0LL) && (4LL + (long long )c) - (long long )q >= 0LL) && (6LL +
        (long long )B) - (long long )q >= 0LL) && (7LL + (long long )A) - (long long
        )q >= 0LL) && (7LL + (long long )b) - (long long )q >= 0LL) && (2147483643LL
        + (long long )c) - (long long )r >= 0LL) && (2147483644LL + (long long )c)
        - (long long )k >= 0LL) && (2147483655LL + (long long )k) - (long long )q
        >= 0LL) && (10LL - (long long )c) - (long long )q >= 0LL) && (2147483649LL
        - (long long )A) - (long long )c >= 0LL) && (2147483649LL - (long long )B)
        - (long long )c >= 0LL) && (2147483649LL - (long long )c) - (long long )r
        >= 0LL) && (2147483650LL - (long long )c) - (long long )k >= 0LL) && (2147483653LL
        - (long long )A) - (long long )q >= 0LL) && (2147483653LL - (long long )B)
        - (long long )q >= 0LL) && (2147483653LL - (long long )q) - (long long )r
        >= 0LL) && (2147483654LL - (long long )k) - (long long )q >= 0LL) && (4294967298LL
        - (long long )b) - (long long )c >= 0LL) && (4294967301LL - (long long )b)
        - (long long )q >= 0LL) && c == 3) || ((((((((((((((((((((((((((((((((((((q
        <= 3U && b <= 1073741823U) && (-3LL + (long long )B) + (long long )c >= 0LL)
        && (-2LL + (long long )A) + (long long )c >= 0LL) && (-2LL + (long long )b)
        + (long long )c >= 0LL) && (-2LL + (long long )c) + (long long )q >= 0LL)
        && (-2LL + (long long )c) + (long long )r >= 0LL) && (2147483646LL + (long
        long )c) + (long long )k >= 0LL) && (2LL - (long long )c) + (long long )q
        >= 0LL) && (2LL - (long long )c) + (long long )r >= 0LL) && (3LL - (long long
        )q) + (long long )r >= 0LL) && (2147483644LL - (long long )A) + (long long
        )c >= 0LL) && (2147483644LL - (long long )B) + (long long )c >= 0LL) && (2147483650LL
        - (long long )c) + (long long )k >= 0LL) && (4294967293LL - (long long )b)
        + (long long )c >= 0LL) && (1LL + (long long )B) - (long long )c >= 0LL) &&
        (1LL + (long long )c) - (long long )q >= 0LL) && (2LL + (long long )A) - (long
        long )c >= 0LL) && (2LL + (long long )B) - (long long )q >= 0LL) && (2LL +
        (long long )b) - (long long )c >= 0LL) && (3LL + (long long )A) - (long long
        )q >= 0LL) && (3LL + (long long )b) - (long long )q >= 0LL) && (2147483644LL
        + (long long )c) - (long long )r >= 0LL) && (2147483645LL + (long long )c)
        - (long long )k >= 0LL) && (2147483651LL + (long long )k) - (long long )q
        >= 0LL) && (5LL - (long long )c) - (long long )q >= 0LL) && (2147483648LL
        - (long long )A) - (long long )c >= 0LL) && (2147483648LL - (long long )B)
        - (long long )c >= 0LL) && (2147483648LL - (long long )c) - (long long )r
        >= 0LL) && (2147483649LL - (long long )A) - (long long )q >= 0LL) && (2147483649LL
        - (long long )B) - (long long )q >= 0LL) && (2147483649LL - (long long )q)
        - (long long )r >= 0LL) && (2147483649LL - (long long )c) - (long long )k
        >= 0LL) && (2147483650LL - (long long )k) - (long long )q >= 0LL) && (4294967297LL
        - (long long )b) - (long long )q >= 0LL) && (4294967297LL - (long long )b)
        - (long long )c >= 0LL) && c == 2))) || (((((((((((((((((((((((((((((((((((((((((((((b
        <= 2147483646U && (-2LL + (long long )B) + (long long )c >= 0LL) && (-1LL
        + (long long )A) + (long long )c >= 0LL) && (-1LL + (long long )b) + (long
        long )c >= 0LL) && (-1LL + (long long )c) + (long long )q >= 0LL) && (-1LL
        + (long long )c) + (long long )r >= 0LL) && (2147483647LL + (long long )c)
        + (long long )k >= 0LL) && (1LL - (long long )q) + (long long )r >= 0LL) &&
        (1LL - (long long )c) + (long long )q >= 0LL) && (1LL - (long long )c) + (long
        long )r >= 0LL) && (2147483645LL - (long long )A) + (long long )c >= 0LL)
        && (2147483645LL - (long long )B) + (long long )c >= 0LL) && (2147483645LL
        - (long long )b) + (long long )c >= 0LL) && (2147483646LL - (long long )b)
        + (long long )q >= 0LL) && (2147483646LL - (long long )b) + (long long )r
        >= 0LL) && (2147483649LL - (long long )c) + (long long )k >= 0LL) && (4294967294LL
        - (long long )b) + (long long )k >= 0LL) && (1LL + (long long )A) - (long
        long )q >= 0LL) && (1LL + (long long )A) - (long long )c >= 0LL) && (1LL +
        (long long )b) - (long long )q >= 0LL) && (1LL + (long long )b) - (long long
        )c >= 0LL) && (2147483645LL + (long long )B) - (long long )b >= 0LL) && (2147483645LL
        + (long long )c) - (long long )r >= 0LL) && (2147483646LL + (long long )A)
        - (long long )b >= 0LL) && (2147483646LL + (long long )c) - (long long )k
        >= 0LL) && (2147483649LL + (long long )k) - (long long )q >= 0LL) && (2LL
        - (long long )c) - (long long )q >= 0LL) && (2147483647LL - (long long )A)
        - (long long )q >= 0LL) && (2147483647LL - (long long )A) - (long long )c
        >= 0LL) && (2147483647LL - (long long )B) - (long long )q >= 0LL) && (2147483647LL
        - (long long )B) - (long long )c >= 0LL) && (2147483647LL - (long long )q)
        - (long long )r >= 0LL) && (2147483647LL - (long long )b) - (long long )q
        >= 0LL) && (2147483647LL - (long long )b) - (long long )c >= 0LL) && (2147483647LL
        - (long long )c) - (long long )r >= 0LL) && (2147483648LL - (long long )c)
        - (long long )k >= 0LL) && (2147483648LL - (long long )k) - (long long )q
        >= 0LL) && (4294967291LL - (long long )b) - (long long )r >= 0LL) && (4294967292LL
        - (long long )A) - (long long )b >= 0LL) && (4294967292LL - (long long )B)
        - (long long )b >= 0LL) && (4294967293LL - (long long )b) - (long long )k
        >= 0LL) && (long long )B - (long long )q >= 0LL) && (long long )B - (long
        long )c >= 0LL) && (long long )c - (long long )q >= 0LL) && c == 1) && (q
        == 0U || q == 1U)))) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((1U
        <= b && b <= 4294967292U) && (-2LL + (long long )B) + (long long )b >= 0LL)
        && (-1LL + (long long )A) + (long long )b >= 0LL) && (-1LL + (long long )B)
        + (long long )c >= 0LL) && (-1LL + (long long )b) + (long long )r >= 0LL)
        && (-1LL + (long long )b) + (long long )c >= 0LL) && (2147483647LL + (long
        long )b) + (long long )k >= 0LL) && (2147483648LL + (long long )c) + (long
        long )k >= 0LL) && (-1LL - (long long )A) + (long long )b >= 0LL) && (0LL
        - (long long )A) + (long long )r >= 0LL) && (0LL - (long long )B) + (long
        long )b >= 0LL) && (0LL - (long long )q) + (long long )r >= 0LL) && (0LL -
        (long long )c) + (long long )q >= 0LL) && (0LL - (long long )c) + (long long
        )r >= 0LL) && (2147483646LL - (long long )A) + (long long )q >= 0LL) && (2147483646LL
        - (long long )A) + (long long )c >= 0LL) && (2147483646LL - (long long )B)
        + (long long )c >= 0LL) && (2147483646LL - (long long )b) + (long long )r
        >= 0LL) && (2147483648LL - (long long )c) + (long long )k >= 0LL) && (4294967292LL
        - (long long )b) + (long long )q >= 0LL) && (4294967292LL - (long long )b)
        + (long long )c >= 0LL) && (6442450940LL - (long long )b) + (long long )k
        >= 0LL) && (long long )A + (long long )c >= 0LL) && (long long )c + (long
        long )q >= 0LL) && (long long )c + (long long )r >= 0LL) && (-1LL + (long
        long )B) - (long long )q >= 0LL) && (-1LL + (long long )B) - (long long )c
        >= 0LL) && (-1LL + (long long )b) - (long long )q >= 0LL) && (-1LL + (long
        long )b) - (long long )r >= 0LL) && (-1LL + (long long )b) - (long long )c
        >= 0LL) && (2147483646LL + (long long )A) - (long long )b >= 0LL) && (2147483646LL
        + (long long )q) - (long long )r >= 0LL) && (2147483646LL + (long long )b)
        - (long long )k >= 0LL) && (2147483646LL + (long long )c) - (long long )r
        >= 0LL) && (2147483647LL + (long long )c) - (long long )k >= 0LL) && (2147483648LL
        + (long long )k) - (long long )q >= 0LL) && (4294967291LL + (long long )B)
        - (long long )b >= 0LL) && (0LL - (long long )c) - (long long )q >= 0LL) &&
        (2147483646LL - (long long )A) - (long long )q >= 0LL) && (2147483646LL -
        (long long )A) - (long long )c >= 0LL) && (2147483646LL - (long long )B) -
        (long long )q >= 0LL) && (2147483646LL - (long long )B) - (long long )c >=
        0LL) && (2147483646LL - (long long )q) - (long long )r >= 0LL) && (2147483646LL
        - (long long )c) - (long long )r >= 0LL) && (2147483647LL - (long long )c)
        - (long long )k >= 0LL) && (2147483647LL - (long long )k) - (long long )q
        >= 0LL) && (4294967292LL - (long long )b) - (long long )q >= 0LL) && (4294967292LL
        - (long long )b) - (long long )c >= 0LL) && (6442450938LL - (long long )A)
        - (long long )b >= 0LL) && (6442450938LL - (long long )B) - (long long )b
        >= 0LL) && (6442450938LL - (long long )b) - (long long )r >= 0LL) && (6442450939LL
        - (long long )b) - (long long )k >= 0LL) && (long long )A - (long long )q
        >= 0LL) && (long long )A - (long long )c >= 0LL) && (long long )c - (long
        long )q >= 0LL) && 0 == c) && 0U == q) && A == r) && q == 0U) && c == 0)))
        || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((4 <= c && b <=
        268435455U) && (-5LL + (long long )B) + (long long )c >= 0LL) && (-4LL + (long
        long )A) + (long long )c >= 0LL) && (-4LL + (long long )b) + (long long )c
        >= 0LL) && (-4LL + (long long )c) + (long long )q >= 0LL) && (-4LL + (long
        long )c) + (long long )r >= 0LL) && (-1LL + (long long )B) + (long long )b
        >= 0LL) && (2147483644LL + (long long )c) + (long long )k >= 0LL) && (2147483648LL
        + (long long )b) + (long long )k >= 0LL) && (2147483642LL - (long long )A)
        + (long long )c >= 0LL) && (2147483642LL - (long long )B) + (long long )c
        >= 0LL) && (2147483646LL - (long long )A) + (long long )q >= 0LL) && (2147483646LL
        - (long long )A) + (long long )r >= 0LL) && (2147483646LL - (long long )A)
        + (long long )b >= 0LL) && (2147483646LL - (long long )B) + (long long )b
        >= 0LL) && (2147483647LL - (long long )c) + (long long )q >= 0LL) && (2147483647LL
        - (long long )c) + (long long )r >= 0LL) && (4294967291LL - (long long )b)
        + (long long )c >= 0LL) && (4294967295LL - (long long )q) + (long long )r
        >= 0LL) && (4294967295LL - (long long )b) + (long long )q >= 0LL) && (4294967295LL
        - (long long )b) + (long long )r >= 0LL) && (4294967295LL - (long long )c)
        + (long long )k >= 0LL) && (6442450943LL - (long long )b) + (long long )k
        >= 0LL) && (long long )A + (long long )b >= 0LL) && (long long )b + (long
        long )q >= 0LL) && (long long )b + (long long )r >= 0LL) && (2147483642LL
        + (long long )c) - (long long )r >= 0LL) && (2147483643LL + (long long )c)
        - (long long )k >= 0LL) && (2147483646LL + (long long )B) - (long long )c
        >= 0LL) && (2147483646LL + (long long )q) - (long long )r >= 0LL) && (2147483646LL
        + (long long )b) - (long long )r >= 0LL) && (2147483647LL + (long long )A)
        - (long long )c >= 0LL) && (2147483647LL + (long long )b) - (long long )c
        >= 0LL) && (2147483647LL + (long long )b) - (long long )k >= 0LL) && (4294967290LL
        + (long long )c) - (long long )q >= 0LL) && (4294967294LL + (long long )B)
        - (long long )q >= 0LL) && (4294967294LL + (long long )B) - (long long )b
        >= 0LL) && (4294967295LL + (long long )A) - (long long )q >= 0LL) && (4294967295LL
        + (long long )A) - (long long )b >= 0LL) && (4294967295LL + (long long )b)
        - (long long )q >= 0LL) && (6442450943LL + (long long )k) - (long long )q
        >= 0LL) && (4294967293LL - (long long )A) - (long long )c >= 0LL) && (4294967293LL
        - (long long )B) - (long long )c >= 0LL) && (4294967293LL - (long long )c)
        - (long long )r >= 0LL) && (4294967294LL - (long long )c) - (long long )k
        >= 0LL) && (6442450941LL - (long long )A) - (long long )q >= 0LL) && (6442450941LL
        - (long long )A) - (long long )b >= 0LL) && (6442450941LL - (long long )B)
        - (long long )q >= 0LL) && (6442450941LL - (long long )B) - (long long )b
        >= 0LL) && (6442450941LL - (long long )q) - (long long )r >= 0LL) && (6442450941LL
        - (long long )b) - (long long )r >= 0LL) && (6442450942LL - (long long )b)
        - (long long )c >= 0LL) && (6442450942LL - (long long )b) - (long long )k
        >= 0LL) && (6442450942LL - (long long )c) - (long long )q >= 0LL) && (6442450942LL
        - (long long )k) - (long long )q >= 0LL) && (8589934590LL - (long long )b)
        - (long long )q >= 0LL)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: 1U <= B
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: A <= 2147483646U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: B <= 2147483646U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: r <= 2147483646U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (-1LL + (long long )B) + (long long )q >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (-1LL + (long long )B) + (long long )c >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483647LL + (long long )B) + (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483648LL + (long long )c) + (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483648LL + (long long )k) + (long long )q >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (0LL - (long long )A) + (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (0LL - (long long )c) + (long long )q >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483645LL - (long long )A) + (long long )B >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483646LL - (long long )A) + (long long )q >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483646LL - (long long )A) + (long long )c >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483646LL - (long long )b) + (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483647LL - (long long )k) + (long long )q >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483648LL - (long long )c) + (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (4294967294LL - (long long )A) + (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (long long )c + (long long )q >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (-1LL + (long long )B) - (long long )q >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (-1LL + (long long )B) - (long long )c >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483645LL + (long long )B) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483646LL + (long long )A) - (long long )b >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483646LL + (long long )B) - (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483646LL + (long long )q) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483646LL + (long long )c) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483647LL + (long long )c) - (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483648LL + (long long )k) - (long long )q >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (4294967294LL + (long long )k) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (0LL - (long long )c) - (long long )q >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483646LL - (long long )A) - (long long )q >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483646LL - (long long )A) - (long long )c >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483646LL - (long long )q) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483646LL - (long long )c) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483647LL - (long long )c) - (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (2147483647LL - (long long )k) - (long long )q >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (4294967292LL - (long long )A) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (4294967293LL - (long long )A) - (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (4294967293LL - (long long )k) - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (long long )A - (long long )r >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (long long )c - (long long )q >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: 0 == c
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: 0U == q
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: A == r
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: q == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: c == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/divbin1-both-t.i
        line: 22
        column: 5
        function: main
      value: (((((((((b <= 4294967292U && (4294967292LL - (long long )b) + (long long
        )q >= 0LL) && (4294967292LL - (long long )b) + (long long )c >= 0LL) && (6442450940LL
        - (long long )b) + (long long )k >= 0LL) && (4294967292LL - (long long )b)
        - (long long )q >= 0LL) && (4294967292LL - (long long )b) - (long long )c
        >= 0LL) && (6442450938LL - (long long )A) - (long long )b >= 0LL) && (6442450938LL
        - (long long )b) - (long long )r >= 0LL) && (6442450939LL - (long long )b)
        - (long long )k >= 0LL) && (((4294967291LL + (long long )B) - (long long )b
        >= 0LL && ((((((((((((((((((((((((((((((((((((((((((8U <= r && 16U <= b) &&
        (-24LL + (long long )A) + (long long )b >= 0LL) && (-24LL + (long long )b)
        + (long long )r >= 0LL) && (-17LL + (long long )B) + (long long )b >= 0LL)
        && (-16LL + (long long )A) + (long long )r >= 0LL) && (-16LL + (long long
        )b) + (long long )q >= 0LL) && (-16LL + (long long )b) + (long long )c >=
        0LL) && (-9LL + (long long )A) + (long long )B >= 0LL) && (-9LL + (long long
        )B) + (long long )r >= 0LL) && (-8LL + (long long )A) + (long long )q >= 0LL)
        && (-8LL + (long long )A) + (long long )c >= 0LL) && (-8LL + (long long )q)
        + (long long )r >= 0LL) && (-8LL + (long long )c) + (long long )r >= 0LL)
        && (2147483632LL + (long long )b) + (long long )k >= 0LL) && (2147483640LL
        + (long long )A) + (long long )k >= 0LL) && (2147483640LL + (long long )k)
        + (long long )r >= 0LL) && (-15LL - (long long )B) + (long long )b >= 0LL)
        && (-8LL - (long long )q) + (long long )r >= 0LL) && (-8LL - (long long )c)
        + (long long )r >= 0LL) && (-7LL - (long long )B) + (long long )r >= 0LL)
        && (2147483630LL - (long long )A) + (long long )b >= 0LL) && (2147483639LL
        - (long long )B) + (long long )q >= 0LL) && (2147483639LL - (long long )B)
        + (long long )c >= 0LL) && (2147483639LL - (long long )k) + (long long )r
        >= 0LL) && (4294967287LL - (long long )B) + (long long )k >= 0LL) && (-16LL
        + (long long )b) - (long long )q >= 0LL) && (-16LL + (long long )b) - (long
        long )c >= 0LL) && (-8LL + (long long )A) - (long long )q >= 0LL) && (-8LL
        + (long long )A) - (long long )c >= 0LL) && (-7LL + (long long )A) - (long
        long )B >= 0LL) && (2147483630LL + (long long )b) - (long long )r >= 0LL)
        && (2147483631LL + (long long )b) - (long long )k >= 0LL) && (2147483639LL
        + (long long )A) - (long long )k >= 0LL) && (2147483639LL - (long long )B)
        - (long long )q >= 0LL) && (2147483639LL - (long long )B) - (long long )c
        >= 0LL) && (4294967285LL - (long long )A) - (long long )B >= 0LL) && (4294967285LL
        - (long long )B) - (long long )r >= 0LL) && (4294967286LL - (long long )B)
        - (long long )k >= 0LL) && (6442450931LL - (long long )B) - (long long )b
        >= 0LL) && b % 16U == 0U) || ((((((((((((((((((((((((((((((((((((((((4U <=
        r && 8U <= b) && (-12LL + (long long )A) + (long long )b >= 0LL) && (-12LL
        + (long long )b) + (long long )r >= 0LL) && (-9LL + (long long )B) + (long
        long )b >= 0LL) && (-8LL + (long long )A) + (long long )r >= 0LL) && (-8LL
        + (long long )b) + (long long )q >= 0LL) && (-8LL + (long long )b) + (long
        long )c >= 0LL) && (-5LL + (long long )A) + (long long )B >= 0LL) && (-5LL
        + (long long )B) + (long long )r >= 0LL) && (-4LL + (long long )A) + (long
        long )q >= 0LL) && (-4LL + (long long )A) + (long long )c >= 0LL) && (-4LL
        + (long long )q) + (long long )r >= 0LL) && (-4LL + (long long )c) + (long
        long )r >= 0LL) && (2147483640LL + (long long )b) + (long long )k >= 0LL)
        && (2147483644LL + (long long )A) + (long long )k >= 0LL) && (2147483644LL
        + (long long )k) + (long long )r >= 0LL) && (-7LL - (long long )B) + (long
        long )b >= 0LL) && (-4LL - (long long )q) + (long long )r >= 0LL) && (-4LL
        - (long long )c) + (long long )r >= 0LL) && (-3LL - (long long )B) + (long
        long )r >= 0LL) && (2147483638LL - (long long )A) + (long long )b >= 0LL)
        && (2147483643LL - (long long )B) + (long long )q >= 0LL) && (2147483643LL
        - (long long )B) + (long long )c >= 0LL) && (2147483643LL - (long long )k)
        + (long long )r >= 0LL) && (4294967291LL - (long long )B) + (long long )k
        >= 0LL) && (-8LL + (long long )b) - (long long )q >= 0LL) && (-8LL + (long
        long )b) - (long long )c >= 0LL) && (-4LL + (long long )A) - (long long )q
        >= 0LL) && (-4LL + (long long )A) - (long long )c >= 0LL) && (-3LL + (long
        long )A) - (long long )B >= 0LL) && (2147483638LL + (long long )b) - (long
        long )r >= 0LL) && (2147483639LL + (long long )b) - (long long )k >= 0LL)
        && (2147483643LL + (long long )A) - (long long )k >= 0LL) && (2147483643LL
        - (long long )B) - (long long )q >= 0LL) && (2147483643LL - (long long )B)
        - (long long )c >= 0LL) && (4294967289LL - (long long )A) - (long long )B
        >= 0LL) && (4294967289LL - (long long )B) - (long long )r >= 0LL) && (4294967290LL
        - (long long )B) - (long long )k >= 0LL) && (6442450935LL - (long long )B)
        - (long long )b >= 0LL) && b % 8U == 0U)) || ((((((((((((((((((((((((((((((((((((((((2U
        <= r && 4U <= b) && (-6LL + (long long )A) + (long long )b >= 0LL) && (-6LL
        + (long long )b) + (long long )r >= 0LL) && (-5LL + (long long )B) + (long
        long )b >= 0LL) && (-4LL + (long long )A) + (long long )r >= 0LL) && (-4LL
        + (long long )b) + (long long )q >= 0LL) && (-4LL + (long long )b) + (long
        long )c >= 0LL) && (-3LL + (long long )A) + (long long )B >= 0LL) && (-3LL
        + (long long )B) + (long long )r >= 0LL) && (-2LL + (long long )A) + (long
        long )q >= 0LL) && (-2LL + (long long )A) + (long long )c >= 0LL) && (-2LL
        + (long long )q) + (long long )r >= 0LL) && (-2LL + (long long )c) + (long
        long )r >= 0LL) && (2147483644LL + (long long )b) + (long long )k >= 0LL)
        && (2147483646LL + (long long )A) + (long long )k >= 0LL) && (2147483646LL
        + (long long )k) + (long long )r >= 0LL) && (-3LL - (long long )B) + (long
        long )b >= 0LL) && (-2LL - (long long )q) + (long long )r >= 0LL) && (-2LL
        - (long long )c) + (long long )r >= 0LL) && (-1LL - (long long )B) + (long
        long )r >= 0LL) && (2147483642LL - (long long )A) + (long long )b >= 0LL)
        && (2147483645LL - (long long )B) + (long long )q >= 0LL) && (2147483645LL
        - (long long )B) + (long long )c >= 0LL) && (2147483645LL - (long long )k)
        + (long long )r >= 0LL) && (4294967293LL - (long long )B) + (long long )k
        >= 0LL) && (-4LL + (long long )b) - (long long )q >= 0LL) && (-4LL + (long
        long )b) - (long long )c >= 0LL) && (-2LL + (long long )A) - (long long )q
        >= 0LL) && (-2LL + (long long )A) - (long long )c >= 0LL) && (-1LL + (long
        long )A) - (long long )B >= 0LL) && (2147483642LL + (long long )b) - (long
        long )r >= 0LL) && (2147483643LL + (long long )b) - (long long )k >= 0LL)
        && (2147483645LL + (long long )A) - (long long )k >= 0LL) && (2147483645LL
        - (long long )B) - (long long )q >= 0LL) && (2147483645LL - (long long )B)
        - (long long )c >= 0LL) && (4294967291LL - (long long )A) - (long long )B
        >= 0LL) && (4294967291LL - (long long )B) - (long long )r >= 0LL) && (4294967292LL
        - (long long )B) - (long long )k >= 0LL) && (6442450937LL - (long long )B)
        - (long long )b >= 0LL) && b % 4U == 0U))) || (((((((((((((((((((((((((((((((((((((((((1U
        <= r && 2U <= b) && (-3LL + (long long )A) + (long long )b >= 0LL) && (-3LL
        + (long long )B) + (long long )b >= 0LL) && (-3LL + (long long )b) + (long
        long )r >= 0LL) && (-2LL + (long long )A) + (long long )B >= 0LL) && (-2LL
        + (long long )A) + (long long )r >= 0LL) && (-2LL + (long long )B) + (long
        long )r >= 0LL) && (-2LL + (long long )b) + (long long )q >= 0LL) && (-2LL
        + (long long )b) + (long long )c >= 0LL) && (-1LL + (long long )A) + (long
        long )q >= 0LL) && (-1LL + (long long )A) + (long long )c >= 0LL) && (-1LL
        + (long long )q) + (long long )r >= 0LL) && (-1LL + (long long )c) + (long
        long )r >= 0LL) && (2147483646LL + (long long )b) + (long long )k >= 0LL)
        && (2147483647LL + (long long )A) + (long long )k >= 0LL) && (2147483647LL
        + (long long )k) + (long long )r >= 0LL) && (-1LL - (long long )B) + (long
        long )b >= 0LL) && (-1LL - (long long )q) + (long long )r >= 0LL) && (-1LL
        - (long long )c) + (long long )r >= 0LL) && (0LL - (long long )B) + (long
        long )r >= 0LL) && (2147483644LL - (long long )A) + (long long )b >= 0LL)
        && (2147483646LL - (long long )B) + (long long )q >= 0LL) && (2147483646LL
        - (long long )B) + (long long )c >= 0LL) && (2147483646LL - (long long )k)
        + (long long )r >= 0LL) && (4294967294LL - (long long )B) + (long long )k
        >= 0LL) && (-2LL + (long long )b) - (long long )q >= 0LL) && (-2LL + (long
        long )b) - (long long )c >= 0LL) && (-1LL + (long long )A) - (long long )q
        >= 0LL) && (-1LL + (long long )A) - (long long )c >= 0LL) && (2147483644LL
        + (long long )b) - (long long )r >= 0LL) && (2147483645LL + (long long )b)
        - (long long )k >= 0LL) && (2147483646LL + (long long )A) - (long long )k
        >= 0LL) && (2147483646LL + (long long )B) - (long long )b >= 0LL) && (2147483646LL
        - (long long )B) - (long long )q >= 0LL) && (2147483646LL - (long long )B)
        - (long long )c >= 0LL) && (4294967292LL - (long long )A) - (long long )B
        >= 0LL) && (4294967292LL - (long long )B) - (long long )r >= 0LL) && (4294967293LL
        - (long long )B) - (long long )k >= 0LL) && (6442450938LL - (long long )B)
        - (long long )b >= 0LL) && (long long )A - (long long )B >= 0LL) && b % 2U
        == 0U))) || (((((((((((((((((((((((((((((((((((((((((((((((((1U <= b && b
        <= 2147483646U) && (-2LL + (long long )B) + (long long )b >= 0LL) && (-1LL
        + (long long )A) + (long long )B >= 0LL) && (-1LL + (long long )A) + (long
        long )b >= 0LL) && (-1LL + (long long )B) + (long long )r >= 0LL) && (-1LL
        + (long long )b) + (long long )q >= 0LL) && (-1LL + (long long )b) + (long
        long )r >= 0LL) && (-1LL + (long long )b) + (long long )c >= 0LL) && (2147483647LL
        + (long long )b) + (long long )k >= 0LL) && (2147483648LL + (long long )A)
        + (long long )k >= 0LL) && (2147483648LL + (long long )k) + (long long )r
        >= 0LL) && (0LL - (long long )B) + (long long )b >= 0LL) && (0LL - (long long
        )q) + (long long )r >= 0LL) && (0LL - (long long )c) + (long long )r >= 0LL)
        && (2147483645LL - (long long )A) + (long long )b >= 0LL) && (2147483646LL
        - (long long )B) + (long long )q >= 0LL) && (2147483646LL - (long long )B)
        + (long long )r >= 0LL) && (2147483646LL - (long long )B) + (long long )c
        >= 0LL) && (2147483646LL - (long long )b) + (long long )q >= 0LL) && (2147483646LL
        - (long long )b) + (long long )c >= 0LL) && (2147483647LL - (long long )k)
        + (long long )r >= 0LL) && (4294967294LL - (long long )B) + (long long )k
        >= 0LL) && (4294967294LL - (long long )b) + (long long )k >= 0LL) && (long
        long )A + (long long )q >= 0LL) && (long long )A + (long long )r >= 0LL) &&
        (long long )A + (long long )c >= 0LL) && (long long )q + (long long )r >=
        0LL) && (long long )c + (long long )r >= 0LL) && (-1LL + (long long )b) -
        (long long )q >= 0LL) && (-1LL + (long long )b) - (long long )c >= 0LL) &&
        (2147483645LL + (long long )b) - (long long )r >= 0LL) && (2147483646LL +
        (long long )A) - (long long )B >= 0LL) && (2147483646LL + (long long )b) -
        (long long )k >= 0LL) && (2147483647LL + (long long )A) - (long long )k >=
        0LL) && (2147483646LL - (long long )B) - (long long )q >= 0LL) && (2147483646LL
        - (long long )B) - (long long )c >= 0LL) && (2147483646LL - (long long )b)
        - (long long )q >= 0LL) && (2147483646LL - (long long )b) - (long long )c
        >= 0LL) && (4294967292LL - (long long )A) - (long long )B >= 0LL) && (4294967292LL
        - (long long )A) - (long long )b >= 0LL) && (4294967292LL - (long long )B)
        - (long long )r >= 0LL) && (4294967292LL - (long long )B) - (long long )b
        >= 0LL) && (4294967292LL - (long long )b) - (long long )r >= 0LL) && (4294967293LL
        - (long long )B) - (long long )k >= 0LL) && (4294967293LL - (long long )b)
        - (long long )k >= 0LL) && (long long )A - (long long )q >= 0LL) && (long
        long )A - (long long )c >= 0LL) && (long long )B - (long long )b >= 0LL) &&
        B == b)
      format: c_expression
