- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: d3136a5a-fd93-45d9-9ff3-ec61022963dd
    creation_time: 2025-03-20T23:30:46Z
    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/array-memsafety/diff-alloca-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i: 5cc33a4b6801f9f06dbbb17ff694aba4439c76c6a2b62ec290c2132cc01ea0fe
      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/array-memsafety/diff-alloca-2.i
        line: 549
        column: 2
        function: main
      value: 1 <= Blen
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 549
        column: 2
        function: main
      value: Alen <= 536870910
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 549
        column: 2
        function: main
      value: Blen <= 536870910
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 549
        column: 2
        function: main
      value: (2147483647LL + (long long )Blen) + (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 549
        column: 2
        function: main
      value: (536870909LL - (long long )Alen) + (long long )Blen >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 549
        column: 2
        function: main
      value: (2684354558LL - (long long )Alen) + (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 549
        column: 2
        function: main
      value: (2684354558LL - (long long )Blen) + (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 549
        column: 2
        function: main
      value: (2147483646LL + (long long )Blen) - (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 549
        column: 2
        function: main
      value: (1073741820LL - (long long )Alen) - (long long )Blen >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 549
        column: 2
        function: main
      value: (2684354557LL - (long long )Alen) - (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 549
        column: 2
        function: main
      value: (2684354557LL - (long long )Blen) - (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 549
        column: 2
        function: main
      value: (((((((((((((((((((((1 <= Alen && (-2LL + (long long )Alen) + (long long
        )Blen >= 0LL) && (-1LL + (long long )Alen) + (long long )i >= 0LL) && (-1LL
        + (long long )Blen) + (long long )i >= 0LL) && (2147483647LL + (long long
        )Alen) + (long long )i >= 0LL) && (2147483648LL + (long long )i) + (long long
        )i >= 0LL) && (536870910LL - (long long )Alen) + (long long )i >= 0LL) &&
        (536870910LL - (long long )Blen) + (long long )i >= 0LL) && (2147483648LL
        - (long long )i) + (long long )i >= 0LL) && (-1LL + (long long )Alen) - (long
        long )i >= 0LL) && (-1LL + (long long )Blen) - (long long )i >= 0LL) && (536870909LL
        + (long long )Alen) - (long long )Blen >= 0LL) && (2147483646LL + (long long
        )Alen) - (long long )i >= 0LL) && (2147483647LL + (long long )i) - (long long
        )i >= 0LL) && (536870910LL - (long long )Alen) - (long long )i >= 0LL) &&
        (536870910LL - (long long )Blen) - (long long )i >= 0LL) && (2147483647LL
        - (long long )i) - (long long )i >= 0LL) && 0 == i) && i == 0) || ((((((((((((((((((4
        <= Alen && 4 <= i) && i <= 536870910) && (-8LL + (long long )Alen) + (long
        long )i >= 0LL) && (-5LL + (long long )Alen) + (long long )Blen >= 0LL) &&
        (-5LL + (long long )Blen) + (long long )i >= 0LL) && (2147483644LL + (long
        long )Alen) + (long long )i >= 0LL) && (2147483644LL + (long long )i) + (long
        long )i >= 0LL) && (536870906LL - (long long )Alen) + (long long )i >= 0LL)
        && (536870906LL - (long long )Blen) + (long long )i >= 0LL) && (2684354558LL
        - (long long )i) + (long long )i >= 0LL) && (536870906LL + (long long )Alen)
        - (long long )Blen >= 0LL) && (536870909LL + (long long )Blen) - (long long
        )i >= 0LL) && (2147483643LL + (long long )Alen) - (long long )i >= 0LL) &&
        (2147483643LL + (long long )i) - (long long )i >= 0LL) && (1073741820LL -
        (long long )Alen) - (long long )i >= 0LL) && (1073741820LL - (long long )Blen)
        - (long long )i >= 0LL) && (2684354557LL - (long long )i) - (long long )i
        >= 0LL) && (long long )Alen - (long long )i >= 0LL)) || (((((((((((((((((3
        <= Alen && (-6LL + (long long )Alen) + (long long )i >= 0LL) && (-4LL + (long
        long )Alen) + (long long )Blen >= 0LL) && (-4LL + (long long )Blen) + (long
        long )i >= 0LL) && (2147483645LL + (long long )Alen) + (long long )i >= 0LL)
        && (2147483645LL + (long long )i) + (long long )i >= 0LL) && (536870907LL
        - (long long )Alen) + (long long )i >= 0LL) && (536870907LL - (long long )Blen)
        + (long long )i >= 0LL) && (2147483651LL - (long long )i) + (long long )i
        >= 0LL) && (2LL + (long long )Blen) - (long long )i >= 0LL) && (536870907LL
        + (long long )Alen) - (long long )Blen >= 0LL) && (2147483644LL + (long long
        )Alen) - (long long )i >= 0LL) && (2147483644LL + (long long )i) - (long long
        )i >= 0LL) && (536870913LL - (long long )Alen) - (long long )i >= 0LL) &&
        (536870913LL - (long long )Blen) - (long long )i >= 0LL) && (2147483650LL
        - (long long )i) - (long long )i >= 0LL) && (long long )Alen - (long long
        )i >= 0LL) && i == 3)) || (((((((((((((((((2 <= Alen && (-4LL + (long long
        )Alen) + (long long )i >= 0LL) && (-3LL + (long long )Alen) + (long long )Blen
        >= 0LL) && (-3LL + (long long )Blen) + (long long )i >= 0LL) && (2147483646LL
        + (long long )Alen) + (long long )i >= 0LL) && (2147483646LL + (long long
        )i) + (long long )i >= 0LL) && (536870908LL - (long long )Alen) + (long long
        )i >= 0LL) && (536870908LL - (long long )Blen) + (long long )i >= 0LL) &&
        (2147483650LL - (long long )i) + (long long )i >= 0LL) && (1LL + (long long
        )Blen) - (long long )i >= 0LL) && (536870908LL + (long long )Alen) - (long
        long )Blen >= 0LL) && (2147483645LL + (long long )Alen) - (long long )i >=
        0LL) && (2147483645LL + (long long )i) - (long long )i >= 0LL) && (536870912LL
        - (long long )Alen) - (long long )i >= 0LL) && (536870912LL - (long long )Blen)
        - (long long )i >= 0LL) && (2147483649LL - (long long )i) - (long long )i
        >= 0LL) && (long long )Alen - (long long )i >= 0LL) && i == 2)) || (((((((((((((((((1
        <= Alen && (-2LL + (long long )Alen) + (long long )Blen >= 0LL) && (-2LL +
        (long long )Alen) + (long long )i >= 0LL) && (-2LL + (long long )Blen) + (long
        long )i >= 0LL) && (2147483647LL + (long long )Alen) + (long long )i >= 0LL)
        && (2147483647LL + (long long )i) + (long long )i >= 0LL) && (536870909LL
        - (long long )Alen) + (long long )i >= 0LL) && (536870909LL - (long long )Blen)
        + (long long )i >= 0LL) && (2147483649LL - (long long )i) + (long long )i
        >= 0LL) && (536870909LL + (long long )Alen) - (long long )Blen >= 0LL) &&
        (2147483646LL + (long long )Alen) - (long long )i >= 0LL) && (2147483646LL
        + (long long )i) - (long long )i >= 0LL) && (536870911LL - (long long )Alen)
        - (long long )i >= 0LL) && (536870911LL - (long long )Blen) - (long long )i
        >= 0LL) && (2147483648LL - (long long )i) - (long long )i >= 0LL) && (long
        long )Alen - (long long )i >= 0LL) && (long long )Blen - (long long )i >=
        0LL) && i == 1)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: 1 <= Alen
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: 1 <= Blen
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: 1 <= l2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: Alen <= 536870910
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: Blen <= 536870910
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: l1 <= 536870910
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: l2 <= 536870910
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (-2LL + (long long )Blen) + (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (-1LL + (long long )Blen) + (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (-1LL + (long long )k) + (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (0LL - (long long )Alen) + (long long )l1 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (0LL - (long long )Blen) + (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (536870909LL - (long long )Alen) + (long long )Blen >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (536870909LL - (long long )Alen) + (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (536870909LL - (long long )l1) + (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (536870910LL - (long long )Alen) + (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (536870910LL - (long long )Blen) + (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (536870909LL + (long long )Blen) - (long long )l1 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (536870910LL + (long long )k) - (long long )l1 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (536870910LL + (long long )k) - (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (1073741820LL - (long long )Alen) - (long long )Blen >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (1073741820LL - (long long )Alen) - (long long )l1 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (1073741820LL - (long long )Alen) - (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (1073741820LL - (long long )Blen) - (long long )l1 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (1073741820LL - (long long )Blen) - (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (1073741820LL - (long long )l1) - (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (long long )Alen - (long long )l1 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (long long )Blen - (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (long long )i - (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: Alen == l1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: Blen == l2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 519
        column: 5
        function: diff
      value: (((((((((((((((((((((((((((((((((((((((0 <= j && j <= 536870910) && (-1LL
        + (long long )Blen) + (long long )found >= 0LL) && (-1LL + (long long )Blen)
        + (long long )j >= 0LL) && (-1LL + (long long )found) + (long long )l2 >=
        0LL) && (-1LL + (long long )found) + (long long )j >= 0LL) && (-1LL + (long
        long )j) + (long long )l2 >= 0LL) && (0LL - (long long )k) + (long long )l1
        >= 0LL) && (0LL - (long long )i) + (long long )l1 >= 0LL) && (0LL - (long
        long )found) + (long long )l2 >= 0LL) && (0LL - (long long )j) + (long long
        )l2 >= 0LL) && (1LL - (long long )found) + (long long )k >= 0LL) && (1LL -
        (long long )found) + (long long )j >= 0LL) && (536870910LL - (long long )Alen)
        + (long long )found >= 0LL) && (536870910LL - (long long )Alen) + (long long
        )j >= 0LL) && (536870910LL - (long long )Blen) + (long long )found >= 0LL)
        && (536870910LL - (long long )Blen) + (long long )j >= 0LL) && (536870910LL
        - (long long )j) + (long long )k >= 0LL) && (long long )found + (long long
        )k >= 0LL) && (long long )j + (long long )k >= 0LL) && (536870910LL + (long
        long )found) - (long long )l1 >= 0LL) && (536870910LL + (long long )found)
        - (long long )l2 >= 0LL) && (536870910LL + (long long )found) - (long long
        )j >= 0LL) && (536870910LL + (long long )j) - (long long )l1 >= 0LL) && (536870910LL
        + (long long )j) - (long long )l2 >= 0LL) && (536870911LL - (long long )Alen)
        - (long long )found >= 0LL) && (536870911LL - (long long )Blen) - (long long
        )found >= 0LL) && (536870911LL - (long long )found) - (long long )l1 >= 0LL)
        && (536870911LL - (long long )found) - (long long )l2 >= 0LL) && (536870911LL
        - (long long )found) - (long long )j >= 0LL) && (1073741820LL - (long long
        )Alen) - (long long )j >= 0LL) && (1073741820LL - (long long )Blen) - (long
        long )j >= 0LL) && (1073741820LL - (long long )j) - (long long )l1 >= 0LL)
        && (1073741820LL - (long long )j) - (long long )l2 >= 0LL) && (long long )Alen
        - (long long )k >= 0LL) && (long long )Alen - (long long )i >= 0LL) && (long
        long )Blen - (long long )found >= 0LL) && (long long )Blen - (long long )j
        >= 0LL) && (found == 0 || found == 1)) && ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= k && 3 <= l1) && k <= 3) && (-6LL + (long long )Alen) + (long long )i >=
        0LL) && (-6LL + (long long )Alen) + (long long )l1 >= 0LL) && (-6LL + (long
        long )i) + (long long )l1 >= 0LL) && (-4LL + (long long )Alen) + (long long
        )Blen >= 0LL) && (-4LL + (long long )Alen) + (long long )l2 >= 0LL) && (-4LL
        + (long long )Blen) + (long long )i >= 0LL) && (-4LL + (long long )Blen) +
        (long long )l1 >= 0LL) && (-4LL + (long long )i) + (long long )l2 >= 0LL)
        && (-4LL + (long long )l1) + (long long )l2 >= 0LL) && (-3LL + (long long
        )Alen) + (long long )k >= 0LL) && (-3LL + (long long )Alen) + (long long )found
        >= 0LL) && (-3LL + (long long )Alen) + (long long )j >= 0LL) && (-3LL + (long
        long )k) + (long long )l1 >= 0LL) && (-3LL + (long long )i) + (long long )k
        >= 0LL) && (-3LL + (long long )i) + (long long )j >= 0LL) && (-3LL + (long
        long )found) + (long long )i >= 0LL) && (-3LL + (long long )found) + (long
        long )l1 >= 0LL) && (-3LL + (long long )j) + (long long )l1 >= 0LL) && (-2LL
        - (long long )found) + (long long )i >= 0LL) && (-2LL - (long long )found)
        + (long long )l1 >= 0LL) && (2LL - (long long )k) + (long long )l2 >= 0LL)
        && (2LL - (long long )i) + (long long )l2 >= 0LL) && (3LL - (long long )i)
        + (long long )k >= 0LL) && (3LL - (long long )i) + (long long )j >= 0LL) &&
        (536870907LL - (long long )Alen) + (long long )i >= 0LL) && (536870907LL -
        (long long )Blen) + (long long )i >= 0LL) && (536870907LL - (long long )Blen)
        + (long long )l1 >= 0LL) && (536870907LL - (long long )j) + (long long )l1
        >= 0LL) && (-2LL + (long long )Alen) - (long long )found >= 0LL) && (2LL +
        (long long )Blen) - (long long )k >= 0LL) && (2LL + (long long )Blen) - (long
        long )i >= 0LL) && (3LL + (long long )found) - (long long )k >= 0LL) && (3LL
        + (long long )found) - (long long )i >= 0LL) && (3LL + (long long )j) - (long
        long )k >= 0LL) && (536870907LL + (long long )Alen) - (long long )Blen >=
        0LL) && (536870907LL + (long long )Alen) - (long long )l2 >= 0LL) && (536870907LL
        + (long long )Alen) - (long long )j >= 0LL) && (536870907LL + (long long )i)
        - (long long )l1 >= 0LL) && (536870907LL + (long long )i) - (long long )l2
        >= 0LL) && (536870907LL + (long long )i) - (long long )j >= 0LL) && (536870907LL
        + (long long )l1) - (long long )l2 >= 0LL) && (4LL - (long long )found) -
        (long long )k >= 0LL) && (4LL - (long long )found) - (long long )i >= 0LL)
        && (6LL - (long long )i) - (long long )k >= 0LL) && (536870913LL - (long long
        )Alen) - (long long )k >= 0LL) && (536870913LL - (long long )Alen) - (long
        long )i >= 0LL) && (536870913LL - (long long )Blen) - (long long )k >= 0LL)
        && (536870913LL - (long long )Blen) - (long long )i >= 0LL) && (536870913LL
        - (long long )k) - (long long )l1 >= 0LL) && (536870913LL - (long long )k)
        - (long long )l2 >= 0LL) && (536870913LL - (long long )i) - (long long )l1
        >= 0LL) && (536870913LL - (long long )i) - (long long )l2 >= 0LL) && (536870913LL
        - (long long )i) - (long long )j >= 0LL) && (536870913LL - (long long )j)
        - (long long )k >= 0LL) && i == 3) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((1
        <= l1 && (-2LL + (long long )Alen) + (long long )Blen >= 0LL) && (-2LL + (long
        long )Alen) + (long long )i >= 0LL) && (-2LL + (long long )Alen) + (long long
        )l1 >= 0LL) && (-2LL + (long long )Alen) + (long long )l2 >= 0LL) && (-2LL
        + (long long )Blen) + (long long )i >= 0LL) && (-2LL + (long long )Blen) +
        (long long )l1 >= 0LL) && (-2LL + (long long )i) + (long long )l1 >= 0LL)
        && (-2LL + (long long )i) + (long long )l2 >= 0LL) && (-2LL + (long long )l1)
        + (long long )l2 >= 0LL) && (-1LL + (long long )Alen) + (long long )k >= 0LL)
        && (-1LL + (long long )Alen) + (long long )found >= 0LL) && (-1LL + (long
        long )Alen) + (long long )j >= 0LL) && (-1LL + (long long )k) + (long long
        )l1 >= 0LL) && (-1LL + (long long )i) + (long long )k >= 0LL) && (-1LL + (long
        long )i) + (long long )j >= 0LL) && (-1LL + (long long )found) + (long long
        )i >= 0LL) && (-1LL + (long long )found) + (long long )l1 >= 0LL) && (-1LL
        + (long long )j) + (long long )l1 >= 0LL) && (0LL - (long long )k) + (long
        long )l2 >= 0LL) && (0LL - (long long )i) + (long long )l2 >= 0LL) && (0LL
        - (long long )found) + (long long )i >= 0LL) && (0LL - (long long )found)
        + (long long )l1 >= 0LL) && (1LL - (long long )i) + (long long )k >= 0LL)
        && (1LL - (long long )i) + (long long )j >= 0LL) && (536870909LL - (long long
        )Alen) + (long long )i >= 0LL) && (536870909LL - (long long )Blen) + (long
        long )i >= 0LL) && (536870909LL - (long long )Blen) + (long long )l1 >= 0LL)
        && (536870909LL - (long long )j) + (long long )l1 >= 0LL) && (1LL + (long
        long )found) - (long long )k >= 0LL) && (1LL + (long long )found) - (long
        long )i >= 0LL) && (1LL + (long long )j) - (long long )k >= 0LL) && (536870909LL
        + (long long )Alen) - (long long )Blen >= 0LL) && (536870909LL + (long long
        )Alen) - (long long )l2 >= 0LL) && (536870909LL + (long long )Alen) - (long
        long )j >= 0LL) && (536870909LL + (long long )i) - (long long )l1 >= 0LL)
        && (536870909LL + (long long )i) - (long long )l2 >= 0LL) && (536870909LL
        + (long long )i) - (long long )j >= 0LL) && (536870909LL + (long long )l1)
        - (long long )l2 >= 0LL) && (2LL - (long long )i) - (long long )k >= 0LL)
        && (2LL - (long long )found) - (long long )k >= 0LL) && (2LL - (long long
        )found) - (long long )i >= 0LL) && (536870911LL - (long long )Alen) - (long
        long )k >= 0LL) && (536870911LL - (long long )Alen) - (long long )i >= 0LL)
        && (536870911LL - (long long )Blen) - (long long )k >= 0LL) && (536870911LL
        - (long long )Blen) - (long long )i >= 0LL) && (536870911LL - (long long )k)
        - (long long )l1 >= 0LL) && (536870911LL - (long long )k) - (long long )l2
        >= 0LL) && (536870911LL - (long long )i) - (long long )l1 >= 0LL) && (536870911LL
        - (long long )i) - (long long )l2 >= 0LL) && (536870911LL - (long long )i)
        - (long long )j >= 0LL) && (536870911LL - (long long )j) - (long long )k >=
        0LL) && (long long )Alen - (long long )found >= 0LL) && (long long )Blen -
        (long long )k >= 0LL) && (long long )Blen - (long long )i >= 0LL) && i ==
        1) && (k == 0 || k == 1))) || (((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= k && 4 <= i) && 4 <= l1) && i <= 536870910) && (-8LL + (long long )Alen)
        + (long long )i >= 0LL) && (-8LL + (long long )Alen) + (long long )l1 >= 0LL)
        && (-8LL + (long long )i) + (long long )l1 >= 0LL) && (-5LL + (long long )Alen)
        + (long long )Blen >= 0LL) && (-5LL + (long long )Alen) + (long long )l2 >=
        0LL) && (-5LL + (long long )Blen) + (long long )i >= 0LL) && (-5LL + (long
        long )Blen) + (long long )l1 >= 0LL) && (-5LL + (long long )i) + (long long
        )l2 >= 0LL) && (-5LL + (long long )l1) + (long long )l2 >= 0LL) && (-4LL +
        (long long )Alen) + (long long )k >= 0LL) && (-4LL + (long long )Alen) + (long
        long )found >= 0LL) && (-4LL + (long long )Alen) + (long long )j >= 0LL) &&
        (-4LL + (long long )k) + (long long )l1 >= 0LL) && (-4LL + (long long )i)
        + (long long )k >= 0LL) && (-4LL + (long long )i) + (long long )j >= 0LL)
        && (-4LL + (long long )found) + (long long )i >= 0LL) && (-4LL + (long long
        )found) + (long long )l1 >= 0LL) && (-4LL + (long long )j) + (long long )l1
        >= 0LL) && (-3LL - (long long )found) + (long long )i >= 0LL) && (-3LL - (long
        long )found) + (long long )l1 >= 0LL) && (536870906LL - (long long )Alen)
        + (long long )i >= 0LL) && (536870906LL - (long long )Blen) + (long long )i
        >= 0LL) && (536870906LL - (long long )Blen) + (long long )l1 >= 0LL) && (536870906LL
        - (long long )j) + (long long )l1 >= 0LL) && (536870909LL - (long long )k)
        + (long long )l2 >= 0LL) && (536870909LL - (long long )i) + (long long )l2
        >= 0LL) && (536870910LL - (long long )i) + (long long )k >= 0LL) && (536870910LL
        - (long long )i) + (long long )j >= 0LL) && (-3LL + (long long )Alen) - (long
        long )found >= 0LL) && (536870906LL + (long long )Alen) - (long long )Blen
        >= 0LL) && (536870906LL + (long long )Alen) - (long long )l2 >= 0LL) && (536870906LL
        + (long long )Alen) - (long long )j >= 0LL) && (536870906LL + (long long )i)
        - (long long )l1 >= 0LL) && (536870906LL + (long long )i) - (long long )l2
        >= 0LL) && (536870906LL + (long long )i) - (long long )j >= 0LL) && (536870906LL
        + (long long )l1) - (long long )l2 >= 0LL) && (536870909LL + (long long )Blen)
        - (long long )k >= 0LL) && (536870909LL + (long long )Blen) - (long long )i
        >= 0LL) && (536870910LL + (long long )found) - (long long )k >= 0LL) && (536870910LL
        + (long long )found) - (long long )i >= 0LL) && (536870910LL + (long long
        )j) - (long long )k >= 0LL) && (536870911LL - (long long )found) - (long long
        )k >= 0LL) && (536870911LL - (long long )found) - (long long )i >= 0LL) &&
        (1073741820LL - (long long )Alen) - (long long )k >= 0LL) && (1073741820LL
        - (long long )Alen) - (long long )i >= 0LL) && (1073741820LL - (long long
        )Blen) - (long long )k >= 0LL) && (1073741820LL - (long long )Blen) - (long
        long )i >= 0LL) && (1073741820LL - (long long )k) - (long long )l1 >= 0LL)
        && (1073741820LL - (long long )k) - (long long )l2 >= 0LL) && (1073741820LL
        - (long long )i) - (long long )k >= 0LL) && (1073741820LL - (long long )i)
        - (long long )l1 >= 0LL) && (1073741820LL - (long long )i) - (long long )l2
        >= 0LL) && (1073741820LL - (long long )i) - (long long )j >= 0LL) && (1073741820LL
        - (long long )j) - (long long )k >= 0LL)) || (((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= k && 2 <= l1) && k <= 2) && (-4LL + (long long )Alen) + (long long )i >=
        0LL) && (-4LL + (long long )Alen) + (long long )l1 >= 0LL) && (-4LL + (long
        long )i) + (long long )l1 >= 0LL) && (-3LL + (long long )Alen) + (long long
        )Blen >= 0LL) && (-3LL + (long long )Alen) + (long long )l2 >= 0LL) && (-3LL
        + (long long )Blen) + (long long )i >= 0LL) && (-3LL + (long long )Blen) +
        (long long )l1 >= 0LL) && (-3LL + (long long )i) + (long long )l2 >= 0LL)
        && (-3LL + (long long )l1) + (long long )l2 >= 0LL) && (-2LL + (long long
        )Alen) + (long long )k >= 0LL) && (-2LL + (long long )Alen) + (long long )found
        >= 0LL) && (-2LL + (long long )Alen) + (long long )j >= 0LL) && (-2LL + (long
        long )k) + (long long )l1 >= 0LL) && (-2LL + (long long )i) + (long long )k
        >= 0LL) && (-2LL + (long long )i) + (long long )j >= 0LL) && (-2LL + (long
        long )found) + (long long )i >= 0LL) && (-2LL + (long long )found) + (long
        long )l1 >= 0LL) && (-2LL + (long long )j) + (long long )l1 >= 0LL) && (-1LL
        - (long long )found) + (long long )i >= 0LL) && (-1LL - (long long )found)
        + (long long )l1 >= 0LL) && (1LL - (long long )k) + (long long )l2 >= 0LL)
        && (1LL - (long long )i) + (long long )l2 >= 0LL) && (2LL - (long long )i)
        + (long long )k >= 0LL) && (2LL - (long long )i) + (long long )j >= 0LL) &&
        (536870908LL - (long long )Alen) + (long long )i >= 0LL) && (536870908LL -
        (long long )Blen) + (long long )i >= 0LL) && (536870908LL - (long long )Blen)
        + (long long )l1 >= 0LL) && (536870908LL - (long long )j) + (long long )l1
        >= 0LL) && (-1LL + (long long )Alen) - (long long )found >= 0LL) && (1LL +
        (long long )Blen) - (long long )k >= 0LL) && (1LL + (long long )Blen) - (long
        long )i >= 0LL) && (2LL + (long long )found) - (long long )k >= 0LL) && (2LL
        + (long long )found) - (long long )i >= 0LL) && (2LL + (long long )j) - (long
        long )k >= 0LL) && (536870908LL + (long long )Alen) - (long long )Blen >=
        0LL) && (536870908LL + (long long )Alen) - (long long )l2 >= 0LL) && (536870908LL
        + (long long )Alen) - (long long )j >= 0LL) && (536870908LL + (long long )i)
        - (long long )l1 >= 0LL) && (536870908LL + (long long )i) - (long long )l2
        >= 0LL) && (536870908LL + (long long )i) - (long long )j >= 0LL) && (536870908LL
        + (long long )l1) - (long long )l2 >= 0LL) && (3LL - (long long )found) -
        (long long )k >= 0LL) && (3LL - (long long )found) - (long long )i >= 0LL)
        && (4LL - (long long )i) - (long long )k >= 0LL) && (536870912LL - (long long
        )Alen) - (long long )k >= 0LL) && (536870912LL - (long long )Alen) - (long
        long )i >= 0LL) && (536870912LL - (long long )Blen) - (long long )k >= 0LL)
        && (536870912LL - (long long )Blen) - (long long )i >= 0LL) && (536870912LL
        - (long long )k) - (long long )l1 >= 0LL) && (536870912LL - (long long )k)
        - (long long )l2 >= 0LL) && (536870912LL - (long long )i) - (long long )l1
        >= 0LL) && (536870912LL - (long long )i) - (long long )l2 >= 0LL) && (536870912LL
        - (long long )i) - (long long )j >= 0LL) && (536870912LL - (long long )j)
        - (long long )k >= 0LL) && i == 2))) || (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((1
        <= l1 && (-2LL + (long long )Alen) + (long long )Blen >= 0LL) && (-2LL + (long
        long )Alen) + (long long )l1 >= 0LL) && (-2LL + (long long )Alen) + (long
        long )l2 >= 0LL) && (-2LL + (long long )Blen) + (long long )l1 >= 0LL) &&
        (-2LL + (long long )l1) + (long long )l2 >= 0LL) && (-1LL + (long long )Alen)
        + (long long )k >= 0LL) && (-1LL + (long long )Alen) + (long long )i >= 0LL)
        && (-1LL + (long long )Blen) + (long long )i >= 0LL) && (-1LL + (long long
        )k) + (long long )l1 >= 0LL) && (-1LL + (long long )i) + (long long )l1 >=
        0LL) && (-1LL + (long long )i) + (long long )l2 >= 0LL) && (2147483647LL +
        (long long )Alen) + (long long )found >= 0LL) && (2147483647LL + (long long
        )Alen) + (long long )j >= 0LL) && (2147483647LL + (long long )Blen) + (long
        long )found >= 0LL) && (2147483647LL + (long long )Blen) + (long long )j >=
        0LL) && (2147483647LL + (long long )found) + (long long )l1 >= 0LL) && (2147483647LL
        + (long long )found) + (long long )l2 >= 0LL) && (2147483647LL + (long long
        )j) + (long long )l1 >= 0LL) && (2147483647LL + (long long )j) + (long long
        )l2 >= 0LL) && (2147483648LL + (long long )i) + (long long )j >= 0LL) && (2147483648LL
        + (long long )found) + (long long )k >= 0LL) && (2147483648LL + (long long
        )found) + (long long )i >= 0LL) && (2147483648LL + (long long )j) + (long
        long )k >= 0LL) && (4294967296LL + (long long )found) + (long long )j >= 0LL)
        && (-1LL - (long long )k) + (long long )l1 >= 0LL) && (-1LL - (long long )k)
        + (long long )l2 >= 0LL) && (-1LL - (long long )i) + (long long )l1 >= 0LL)
        && (-1LL - (long long )i) + (long long )l2 >= 0LL) && (0LL - (long long )i)
        + (long long )k >= 0LL) && (536870909LL - (long long )Blen) + (long long )l1
        >= 0LL) && (536870910LL - (long long )Alen) + (long long )i >= 0LL) && (536870910LL
        - (long long )Blen) + (long long )i >= 0LL) && (2147483646LL - (long long
        )found) + (long long )l1 >= 0LL) && (2147483646LL - (long long )found) + (long
        long )l2 >= 0LL) && (2147483646LL - (long long )j) + (long long )l1 >= 0LL)
        && (2147483646LL - (long long )j) + (long long )l2 >= 0LL) && (2147483647LL
        - (long long )found) + (long long )k >= 0LL) && (2147483647LL - (long long
        )found) + (long long )i >= 0LL) && (2147483647LL - (long long )j) + (long
        long )k >= 0LL) && (2147483648LL - (long long )i) + (long long )j >= 0LL)
        && (2684354558LL - (long long )Alen) + (long long )found >= 0LL) && (2684354558LL
        - (long long )Alen) + (long long )j >= 0LL) && (2684354558LL - (long long
        )Blen) + (long long )found >= 0LL) && (2684354558LL - (long long )Blen) +
        (long long )j >= 0LL) && (4294967295LL - (long long )found) + (long long )j
        >= 0LL) && (long long )i + (long long )k >= 0LL) && (-1LL + (long long )Alen)
        - (long long )k >= 0LL) && (-1LL + (long long )Alen) - (long long )i >= 0LL)
        && (-1LL + (long long )Blen) - (long long )k >= 0LL) && (-1LL + (long long
        )Blen) - (long long )i >= 0LL) && (536870909LL + (long long )Alen) - (long
        long )Blen >= 0LL) && (536870909LL + (long long )Alen) - (long long )l2 >=
        0LL) && (536870909LL + (long long )l1) - (long long )l2 >= 0LL) && (536870910LL
        + (long long )i) - (long long )l1 >= 0LL) && (536870910LL + (long long )i)
        - (long long )l2 >= 0LL) && (2147483646LL + (long long )Alen) - (long long
        )found >= 0LL) && (2147483646LL + (long long )Alen) - (long long )j >= 0LL)
        && (2147483646LL + (long long )Blen) - (long long )found >= 0LL) && (2147483646LL
        + (long long )Blen) - (long long )j >= 0LL) && (2147483647LL + (long long
        )i) - (long long )j >= 0LL) && (2147483648LL + (long long )found) - (long
        long )k >= 0LL) && (2147483648LL + (long long )found) - (long long )i >= 0LL)
        && (2147483648LL + (long long )j) - (long long )k >= 0LL) && (2684354558LL
        + (long long )found) - (long long )l1 >= 0LL) && (2684354558LL + (long long
        )found) - (long long )l2 >= 0LL) && (2684354558LL + (long long )j) - (long
        long )l1 >= 0LL) && (2684354558LL + (long long )j) - (long long )l2 >= 0LL)
        && (4294967295LL + (long long )found) - (long long )j >= 0LL) && (0LL - (long
        long )i) - (long long )k >= 0LL) && (536870910LL - (long long )Alen) - (long
        long )k >= 0LL) && (536870910LL - (long long )Alen) - (long long )i >= 0LL)
        && (536870910LL - (long long )Blen) - (long long )k >= 0LL) && (536870910LL
        - (long long )Blen) - (long long )i >= 0LL) && (536870910LL - (long long )k)
        - (long long )l1 >= 0LL) && (536870910LL - (long long )k) - (long long )l2
        >= 0LL) && (536870910LL - (long long )i) - (long long )l1 >= 0LL) && (536870910LL
        - (long long )i) - (long long )l2 >= 0LL) && (2147483647LL - (long long )i)
        - (long long )j >= 0LL) && (2147483647LL - (long long )found) - (long long
        )k >= 0LL) && (2147483647LL - (long long )found) - (long long )i >= 0LL) &&
        (2147483647LL - (long long )j) - (long long )k >= 0LL) && (2684354557LL -
        (long long )Alen) - (long long )found >= 0LL) && (2684354557LL - (long long
        )Alen) - (long long )j >= 0LL) && (2684354557LL - (long long )Blen) - (long
        long )found >= 0LL) && (2684354557LL - (long long )Blen) - (long long )j >=
        0LL) && (2684354557LL - (long long )found) - (long long )l1 >= 0LL) && (2684354557LL
        - (long long )found) - (long long )l2 >= 0LL) && (2684354557LL - (long long
        )j) - (long long )l1 >= 0LL) && (2684354557LL - (long long )j) - (long long
        )l2 >= 0LL) && (4294967294LL - (long long )found) - (long long )j >= 0LL)
        && 0 == k) && 0 == i) && k == 0) && k == i) && i == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: 1 <= Alen
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: 1 <= Blen
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: 1 <= l2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: Alen <= 536870910
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: Blen <= 536870910
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: l1 <= 536870910
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: l2 <= 536870910
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (-2LL + (long long )Blen) + (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (-1LL + (long long )Blen) + (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (-1LL + (long long )Blen) + (long long )j >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (-1LL + (long long )k) + (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (-1LL + (long long )j) + (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (-1LL - (long long )k) + (long long )l1 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (-1LL - (long long )i) + (long long )l1 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (0LL - (long long )Alen) + (long long )l1 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (0LL - (long long )Blen) + (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (536870909LL - (long long )Alen) + (long long )Blen >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (536870909LL - (long long )Alen) + (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (536870909LL - (long long )l1) + (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (536870910LL - (long long )Alen) + (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (536870910LL - (long long )Alen) + (long long )found >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (536870910LL - (long long )Alen) + (long long )j >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (536870910LL - (long long )Blen) + (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (536870910LL - (long long )Blen) + (long long )found >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (536870910LL - (long long )Blen) + (long long )j >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (long long )found + (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (long long )j + (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (-1LL + (long long )Alen) - (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (-1LL + (long long )Alen) - (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (536870909LL + (long long )Blen) - (long long )l1 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (536870910LL + (long long )k) - (long long )l1 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (536870910LL + (long long )k) - (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (536870910LL + (long long )found) - (long long )l1 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (536870910LL + (long long )found) - (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (536870910LL + (long long )j) - (long long )l1 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (536870910LL + (long long )j) - (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (1073741820LL - (long long )Alen) - (long long )Blen >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (1073741820LL - (long long )Alen) - (long long )l1 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (1073741820LL - (long long )Alen) - (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (1073741820LL - (long long )Blen) - (long long )l1 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (1073741820LL - (long long )Blen) - (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (1073741820LL - (long long )l1) - (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (long long )Alen - (long long )l1 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (long long )Blen - (long long )l2 >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (long long )i - (long long )k >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: Alen == l1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: Blen == l2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 522
        column: 9
        function: diff
      value: (((((((((((((((((((((((((((((((-1LL + (long long )found) + (long long
        )j >= 0LL && (0LL - (long long )found) + (long long )l2 >= 0LL) && (0LL -
        (long long )j) + (long long )l2 >= 0LL) && (1LL - (long long )found) + (long
        long )k >= 0LL) && (1LL - (long long )found) + (long long )j >= 0LL) && (536870911LL
        - (long long )Alen) - (long long )found >= 0LL) && (536870911LL - (long long
        )Blen) - (long long )found >= 0LL) && (536870911LL - (long long )found) -
        (long long )l1 >= 0LL) && (536870911LL - (long long )found) - (long long )l2
        >= 0LL) && (long long )Blen - (long long )found >= 0LL) && (long long )Blen
        - (long long )j >= 0LL) && (found == 0 || found == 1)) && (((((0 <= j && (-2LL
        + (long long )Blen) + (long long )found >= 0LL) && (-2LL + (long long )found)
        + (long long )l2 >= 0LL) && ((((((((((j <= 3 && (3LL - (long long )j) + (long
        long )k >= 0LL) && (3LL + (long long )found) - (long long )j >= 0LL) && (3LL
        - (long long )found) - (long long )j >= 0LL) && (536870913LL - (long long
        )Alen) - (long long )j >= 0LL) && (536870913LL - (long long )Blen) - (long
        long )j >= 0LL) && (536870913LL - (long long )j) - (long long )l1 >= 0LL)
        && (536870913LL - (long long )j) - (long long )l2 >= 0LL) && ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= k && 4 <= l1) && k <= 3) && (-8LL + (long long )Alen) + (long long )l1
        >= 0LL) && (-7LL + (long long )Alen) + (long long )i >= 0LL) && (-7LL + (long
        long )i) + (long long )l1 >= 0LL) && (-5LL + (long long )Alen) + (long long
        )Blen >= 0LL) && (-5LL + (long long )Alen) + (long long )l2 >= 0LL) && (-5LL
        + (long long )Blen) + (long long )l1 >= 0LL) && (-5LL + (long long )l1) +
        (long long )l2 >= 0LL) && (-4LL + (long long )Alen) + (long long )k >= 0LL)
        && (-4LL + (long long )Alen) + (long long )found >= 0LL) && (-4LL + (long
        long )Alen) + (long long )j >= 0LL) && (-4LL + (long long )Blen) + (long long
        )i >= 0LL) && (-4LL + (long long )k) + (long long )l1 >= 0LL) && (-4LL + (long
        long )i) + (long long )l2 >= 0LL) && (-4LL + (long long )found) + (long long
        )l1 >= 0LL) && (-4LL + (long long )j) + (long long )l1 >= 0LL) && (-3LL +
        (long long )i) + (long long )k >= 0LL) && (-3LL + (long long )i) + (long long
        )j >= 0LL) && (-3LL + (long long )found) + (long long )i >= 0LL) && (-3LL
        - (long long )found) + (long long )l1 >= 0LL) && (-2LL - (long long )found)
        + (long long )i >= 0LL) && (-1LL - (long long )j) + (long long )l1 >= 0LL)
        && (2LL - (long long )k) + (long long )l2 >= 0LL) && (2LL - (long long )i)
        + (long long )l2 >= 0LL) && (3LL - (long long )i) + (long long )k >= 0LL)
        && (3LL - (long long )i) + (long long )j >= 0LL) && (536870906LL - (long long
        )Blen) + (long long )l1 >= 0LL) && (536870907LL - (long long )Alen) + (long
        long )i >= 0LL) && (536870907LL - (long long )Blen) + (long long )i >= 0LL)
        && (-3LL + (long long )Alen) - (long long )found >= 0LL) && (-1LL + (long
        long )Alen) - (long long )j >= 0LL) && (2LL + (long long )Blen) - (long long
        )k >= 0LL) && (2LL + (long long )Blen) - (long long )i >= 0LL) && (3LL + (long
        long )found) - (long long )k >= 0LL) && (3LL + (long long )found) - (long
        long )i >= 0LL) && (3LL + (long long )j) - (long long )k >= 0LL) && (536870906LL
        + (long long )Alen) - (long long )Blen >= 0LL) && (536870906LL + (long long
        )Alen) - (long long )l2 >= 0LL) && (536870906LL + (long long )l1) - (long
        long )l2 >= 0LL) && (536870907LL + (long long )i) - (long long )l1 >= 0LL)
        && (536870907LL + (long long )i) - (long long )l2 >= 0LL) && (4LL - (long
        long )found) - (long long )k >= 0LL) && (4LL - (long long )found) - (long
        long )i >= 0LL) && (6LL - (long long )i) - (long long )k >= 0LL) && (6LL -
        (long long )i) - (long long )j >= 0LL) && (6LL - (long long )j) - (long long
        )k >= 0LL) && (536870913LL - (long long )Alen) - (long long )k >= 0LL) &&
        (536870913LL - (long long )Alen) - (long long )i >= 0LL) && (536870913LL -
        (long long )Blen) - (long long )k >= 0LL) && (536870913LL - (long long )Blen)
        - (long long )i >= 0LL) && (536870913LL - (long long )k) - (long long )l1
        >= 0LL) && (536870913LL - (long long )k) - (long long )l2 >= 0LL) && (536870913LL
        - (long long )i) - (long long )l1 >= 0LL) && (536870913LL - (long long )i)
        - (long long )l2 >= 0LL) && (long long )i - (long long )j >= 0LL) && i ==
        3) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((2 <= l1 && (-4LL
        + (long long )Alen) + (long long )l1 >= 0LL) && (-3LL + (long long )Alen)
        + (long long )Blen >= 0LL) && (-3LL + (long long )Alen) + (long long )i >=
        0LL) && (-3LL + (long long )Alen) + (long long )l2 >= 0LL) && (-3LL + (long
        long )Blen) + (long long )l1 >= 0LL) && (-3LL + (long long )i) + (long long
        )l1 >= 0LL) && (-3LL + (long long )l1) + (long long )l2 >= 0LL) && (-2LL +
        (long long )Alen) + (long long )k >= 0LL) && (-2LL + (long long )Alen) + (long
        long )found >= 0LL) && (-2LL + (long long )Alen) + (long long )j >= 0LL) &&
        (-2LL + (long long )Blen) + (long long )i >= 0LL) && (-2LL + (long long )k)
        + (long long )l1 >= 0LL) && (-2LL + (long long )i) + (long long )l2 >= 0LL)
        && (-2LL + (long long )found) + (long long )l1 >= 0LL) && (-2LL + (long long
        )j) + (long long )l1 >= 0LL) && (-1LL + (long long )i) + (long long )k >=
        0LL) && (-1LL + (long long )i) + (long long )j >= 0LL) && (-1LL + (long long
        )found) + (long long )i >= 0LL) && (-1LL - (long long )found) + (long long
        )l1 >= 0LL) && (0LL - (long long )k) + (long long )l2 >= 0LL) && (0LL - (long
        long )i) + (long long )l2 >= 0LL) && (0LL - (long long )found) + (long long
        )i >= 0LL) && (1LL - (long long )i) + (long long )k >= 0LL) && (1LL - (long
        long )i) + (long long )j >= 0LL) && (1LL - (long long )j) + (long long )l1
        >= 0LL) && (536870908LL - (long long )Blen) + (long long )l1 >= 0LL) && (536870909LL
        - (long long )Alen) + (long long )i >= 0LL) && (536870909LL - (long long )Blen)
        + (long long )i >= 0LL) && (-1LL + (long long )Alen) - (long long )found >=
        0LL) && (1LL + (long long )Alen) - (long long )j >= 0LL) && (1LL + (long long
        )found) - (long long )k >= 0LL) && (1LL + (long long )found) - (long long
        )i >= 0LL) && (1LL + (long long )j) - (long long )k >= 0LL) && (2LL + (long
        long )i) - (long long )j >= 0LL) && (536870908LL + (long long )Alen) - (long
        long )Blen >= 0LL) && (536870908LL + (long long )Alen) - (long long )l2 >=
        0LL) && (536870908LL + (long long )l1) - (long long )l2 >= 0LL) && (536870909LL
        + (long long )i) - (long long )l1 >= 0LL) && (536870909LL + (long long )i)
        - (long long )l2 >= 0LL) && (2LL - (long long )i) - (long long )k >= 0LL)
        && (2LL - (long long )found) - (long long )k >= 0LL) && (2LL - (long long
        )found) - (long long )i >= 0LL) && (4LL - (long long )i) - (long long )j >=
        0LL) && (4LL - (long long )j) - (long long )k >= 0LL) && (536870911LL - (long
        long )Alen) - (long long )k >= 0LL) && (536870911LL - (long long )Alen) -
        (long long )i >= 0LL) && (536870911LL - (long long )Blen) - (long long )k
        >= 0LL) && (536870911LL - (long long )Blen) - (long long )i >= 0LL) && (536870911LL
        - (long long )k) - (long long )l1 >= 0LL) && (536870911LL - (long long )k)
        - (long long )l2 >= 0LL) && (536870911LL - (long long )i) - (long long )l1
        >= 0LL) && (536870911LL - (long long )i) - (long long )l2 >= 0LL) && (long
        long )Blen - (long long )k >= 0LL) && (long long )Blen - (long long )i >=
        0LL) && i == 1) && (k == 0 || k == 1)))) || (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= k && 4 <= l1) && k <= 3) && j <= 2) && (-8LL + (long long )Alen) + (long
        long )l1 >= 0LL) && (-7LL + (long long )Alen) + (long long )i >= 0LL) && (-7LL
        + (long long )i) + (long long )l1 >= 0LL) && (-5LL + (long long )Alen) + (long
        long )Blen >= 0LL) && (-5LL + (long long )Alen) + (long long )l2 >= 0LL) &&
        (-5LL + (long long )Blen) + (long long )l1 >= 0LL) && (-5LL + (long long )l1)
        + (long long )l2 >= 0LL) && (-4LL + (long long )Alen) + (long long )k >= 0LL)
        && (-4LL + (long long )Alen) + (long long )found >= 0LL) && (-4LL + (long
        long )Alen) + (long long )j >= 0LL) && (-4LL + (long long )Blen) + (long long
        )i >= 0LL) && (-4LL + (long long )k) + (long long )l1 >= 0LL) && (-4LL + (long
        long )i) + (long long )l2 >= 0LL) && (-4LL + (long long )found) + (long long
        )l1 >= 0LL) && (-4LL + (long long )j) + (long long )l1 >= 0LL) && (-3LL +
        (long long )i) + (long long )k >= 0LL) && (-3LL + (long long )i) + (long long
        )j >= 0LL) && (-3LL + (long long )found) + (long long )i >= 0LL) && (-3LL
        - (long long )found) + (long long )l1 >= 0LL) && (-2LL - (long long )found)
        + (long long )i >= 0LL) && (-2LL - (long long )j) + (long long )l1 >= 0LL)
        && (2LL - (long long )k) + (long long )l2 >= 0LL) && (2LL - (long long )i)
        + (long long )l2 >= 0LL) && (2LL - (long long )j) + (long long )k >= 0LL)
        && (3LL - (long long )i) + (long long )k >= 0LL) && (3LL - (long long )i)
        + (long long )j >= 0LL) && (536870906LL - (long long )Blen) + (long long )l1
        >= 0LL) && (536870907LL - (long long )Alen) + (long long )i >= 0LL) && (536870907LL
        - (long long )Blen) + (long long )i >= 0LL) && (-3LL + (long long )Alen) -
        (long long )found >= 0LL) && (-2LL + (long long )Alen) - (long long )j >=
        0LL) && (-1LL + (long long )i) - (long long )j >= 0LL) && (2LL + (long long
        )Blen) - (long long )k >= 0LL) && (2LL + (long long )Blen) - (long long )i
        >= 0LL) && (2LL + (long long )found) - (long long )j >= 0LL) && (3LL + (long
        long )found) - (long long )k >= 0LL) && (3LL + (long long )found) - (long
        long )i >= 0LL) && (3LL + (long long )j) - (long long )k >= 0LL) && (536870906LL
        + (long long )Alen) - (long long )Blen >= 0LL) && (536870906LL + (long long
        )Alen) - (long long )l2 >= 0LL) && (536870906LL + (long long )l1) - (long
        long )l2 >= 0LL) && (536870907LL + (long long )i) - (long long )l1 >= 0LL)
        && (536870907LL + (long long )i) - (long long )l2 >= 0LL) && (2LL - (long
        long )found) - (long long )j >= 0LL) && (4LL - (long long )found) - (long
        long )k >= 0LL) && (4LL - (long long )found) - (long long )i >= 0LL) && (5LL
        - (long long )i) - (long long )j >= 0LL) && (5LL - (long long )j) - (long
        long )k >= 0LL) && (6LL - (long long )i) - (long long )k >= 0LL) && (536870912LL
        - (long long )Alen) - (long long )j >= 0LL) && (536870912LL - (long long )Blen)
        - (long long )j >= 0LL) && (536870912LL - (long long )j) - (long long )l1
        >= 0LL) && (536870912LL - (long long )j) - (long long )l2 >= 0LL) && (536870913LL
        - (long long )Alen) - (long long )k >= 0LL) && (536870913LL - (long long )Alen)
        - (long long )i >= 0LL) && (536870913LL - (long long )Blen) - (long long )k
        >= 0LL) && (536870913LL - (long long )Blen) - (long long )i >= 0LL) && (536870913LL
        - (long long )k) - (long long )l1 >= 0LL) && (536870913LL - (long long )k)
        - (long long )l2 >= 0LL) && (536870913LL - (long long )i) - (long long )l1
        >= 0LL) && (536870913LL - (long long )i) - (long long )l2 >= 0LL) && i ==
        3)) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((2 <=
        l1 && j <= 2) && (-4LL + (long long )Alen) + (long long )l1 >= 0LL) && (-3LL
        + (long long )Alen) + (long long )Blen >= 0LL) && (-3LL + (long long )Alen)
        + (long long )i >= 0LL) && (-3LL + (long long )Alen) + (long long )l2 >= 0LL)
        && (-3LL + (long long )Blen) + (long long )l1 >= 0LL) && (-3LL + (long long
        )i) + (long long )l1 >= 0LL) && (-3LL + (long long )l1) + (long long )l2 >=
        0LL) && (-2LL + (long long )Alen) + (long long )k >= 0LL) && (-2LL + (long
        long )Alen) + (long long )found >= 0LL) && (-2LL + (long long )Alen) + (long
        long )j >= 0LL) && (-2LL + (long long )Blen) + (long long )i >= 0LL) && (-2LL
        + (long long )k) + (long long )l1 >= 0LL) && (-2LL + (long long )i) + (long
        long )l2 >= 0LL) && (-2LL + (long long )found) + (long long )l1 >= 0LL) &&
        (-2LL + (long long )j) + (long long )l1 >= 0LL) && (-1LL + (long long )i)
        + (long long )k >= 0LL) && (-1LL + (long long )i) + (long long )j >= 0LL)
        && (-1LL + (long long )found) + (long long )i >= 0LL) && (-1LL - (long long
        )found) + (long long )l1 >= 0LL) && (0LL - (long long )k) + (long long )l2
        >= 0LL) && (0LL - (long long )i) + (long long )l2 >= 0LL) && (0LL - (long
        long )found) + (long long )i >= 0LL) && (0LL - (long long )j) + (long long
        )l1 >= 0LL) && (1LL - (long long )i) + (long long )k >= 0LL) && (1LL - (long
        long )i) + (long long )j >= 0LL) && (2LL - (long long )j) + (long long )k
        >= 0LL) && (536870908LL - (long long )Blen) + (long long )l1 >= 0LL) && (536870909LL
        - (long long )Alen) + (long long )i >= 0LL) && (536870909LL - (long long )Blen)
        + (long long )i >= 0LL) && (-1LL + (long long )Alen) - (long long )found >=
        0LL) && (1LL + (long long )i) - (long long )j >= 0LL) && (1LL + (long long
        )found) - (long long )k >= 0LL) && (1LL + (long long )found) - (long long
        )i >= 0LL) && (1LL + (long long )j) - (long long )k >= 0LL) && (2LL + (long
        long )found) - (long long )j >= 0LL) && (536870908LL + (long long )Alen) -
        (long long )Blen >= 0LL) && (536870908LL + (long long )Alen) - (long long
        )l2 >= 0LL) && (536870908LL + (long long )l1) - (long long )l2 >= 0LL) &&
        (536870909LL + (long long )i) - (long long )l1 >= 0LL) && (536870909LL + (long
        long )i) - (long long )l2 >= 0LL) && (2LL - (long long )i) - (long long )k
        >= 0LL) && (2LL - (long long )found) - (long long )k >= 0LL) && (2LL - (long
        long )found) - (long long )i >= 0LL) && (2LL - (long long )found) - (long
        long )j >= 0LL) && (3LL - (long long )i) - (long long )j >= 0LL) && (3LL -
        (long long )j) - (long long )k >= 0LL) && (536870911LL - (long long )Alen)
        - (long long )k >= 0LL) && (536870911LL - (long long )Alen) - (long long )i
        >= 0LL) && (536870911LL - (long long )Blen) - (long long )k >= 0LL) && (536870911LL
        - (long long )Blen) - (long long )i >= 0LL) && (536870911LL - (long long )k)
        - (long long )l1 >= 0LL) && (536870911LL - (long long )k) - (long long )l2
        >= 0LL) && (536870911LL - (long long )i) - (long long )l1 >= 0LL) && (536870911LL
        - (long long )i) - (long long )l2 >= 0LL) && (536870912LL - (long long )Alen)
        - (long long )j >= 0LL) && (536870912LL - (long long )Blen) - (long long )j
        >= 0LL) && (536870912LL - (long long )j) - (long long )l1 >= 0LL) && (536870912LL
        - (long long )j) - (long long )l2 >= 0LL) && (long long )Alen - (long long
        )j >= 0LL) && (long long )Blen - (long long )k >= 0LL) && (long long )Blen
        - (long long )i >= 0LL) && i == 1) && (k == 0 || k == 1)))) || (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= k && 4 <= l1) && k <= 3) && (-8LL + (long long )Alen) + (long long )l1
        >= 0LL) && (-7LL + (long long )Alen) + (long long )i >= 0LL) && (-7LL + (long
        long )i) + (long long )l1 >= 0LL) && (-5LL + (long long )Alen) + (long long
        )Blen >= 0LL) && (-5LL + (long long )Alen) + (long long )l2 >= 0LL) && (-5LL
        + (long long )Blen) + (long long )l1 >= 0LL) && (-5LL + (long long )l1) +
        (long long )l2 >= 0LL) && (-4LL + (long long )Alen) + (long long )k >= 0LL)
        && (-4LL + (long long )Alen) + (long long )found >= 0LL) && (-4LL + (long
        long )Alen) + (long long )j >= 0LL) && (-4LL + (long long )Blen) + (long long
        )i >= 0LL) && (-4LL + (long long )k) + (long long )l1 >= 0LL) && (-4LL + (long
        long )i) + (long long )l2 >= 0LL) && (-4LL + (long long )found) + (long long
        )l1 >= 0LL) && (-4LL + (long long )j) + (long long )l1 >= 0LL) && (-3LL +
        (long long )i) + (long long )k >= 0LL) && (-3LL + (long long )i) + (long long
        )j >= 0LL) && (-3LL + (long long )found) + (long long )i >= 0LL) && (-1LL
        + (long long )Blen) + (long long )found >= 0LL) && (-1LL + (long long )found)
        + (long long )l2 >= 0LL) && (-3LL - (long long )found) + (long long )l1 >=
        0LL) && (-3LL - (long long )j) + (long long )l1 >= 0LL) && (-2LL - (long long
        )found) + (long long )i >= 0LL) && (1LL - (long long )j) + (long long )k >=
        0LL) && (2LL - (long long )k) + (long long )l2 >= 0LL) && (2LL - (long long
        )i) + (long long )l2 >= 0LL) && (3LL - (long long )i) + (long long )k >= 0LL)
        && (3LL - (long long )i) + (long long )j >= 0LL) && (536870906LL - (long long
        )Blen) + (long long )l1 >= 0LL) && (536870907LL - (long long )Alen) + (long
        long )i >= 0LL) && (536870907LL - (long long )Blen) + (long long )i >= 0LL)
        && (-3LL + (long long )Alen) - (long long )found >= 0LL) && (-3LL + (long
        long )Alen) - (long long )j >= 0LL) && (-2LL + (long long )i) - (long long
        )j >= 0LL) && (1LL + (long long )found) - (long long )j >= 0LL) && (2LL +
        (long long )Blen) - (long long )k >= 0LL) && (2LL + (long long )Blen) - (long
        long )i >= 0LL) && (3LL + (long long )found) - (long long )k >= 0LL) && (3LL
        + (long long )found) - (long long )i >= 0LL) && (3LL + (long long )j) - (long
        long )k >= 0LL) && (536870906LL + (long long )Alen) - (long long )Blen >=
        0LL) && (536870906LL + (long long )Alen) - (long long )l2 >= 0LL) && (536870906LL
        + (long long )l1) - (long long )l2 >= 0LL) && (536870907LL + (long long )i)
        - (long long )l1 >= 0LL) && (536870907LL + (long long )i) - (long long )l2
        >= 0LL) && (1LL - (long long )found) - (long long )j >= 0LL) && (4LL - (long
        long )i) - (long long )j >= 0LL) && (4LL - (long long )found) - (long long
        )k >= 0LL) && (4LL - (long long )found) - (long long )i >= 0LL) && (4LL -
        (long long )j) - (long long )k >= 0LL) && (6LL - (long long )i) - (long long
        )k >= 0LL) && (536870911LL - (long long )Alen) - (long long )j >= 0LL) &&
        (536870911LL - (long long )Blen) - (long long )j >= 0LL) && (536870911LL -
        (long long )j) - (long long )l1 >= 0LL) && (536870911LL - (long long )j) -
        (long long )l2 >= 0LL) && (536870913LL - (long long )Alen) - (long long )k
        >= 0LL) && (536870913LL - (long long )Alen) - (long long )i >= 0LL) && (536870913LL
        - (long long )Blen) - (long long )k >= 0LL) && (536870913LL - (long long )Blen)
        - (long long )i >= 0LL) && (536870913LL - (long long )k) - (long long )l1
        >= 0LL) && (536870913LL - (long long )k) - (long long )l2 >= 0LL) && (536870913LL
        - (long long )i) - (long long )l1 >= 0LL) && (536870913LL - (long long )i)
        - (long long )l2 >= 0LL) && i == 3) && (j == 0 || j == 1))) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((2
        <= l1 && (-4LL + (long long )Alen) + (long long )l1 >= 0LL) && (-3LL + (long
        long )Alen) + (long long )Blen >= 0LL) && (-3LL + (long long )Alen) + (long
        long )i >= 0LL) && (-3LL + (long long )Alen) + (long long )l2 >= 0LL) && (-3LL
        + (long long )Blen) + (long long )l1 >= 0LL) && (-3LL + (long long )i) + (long
        long )l1 >= 0LL) && (-3LL + (long long )l1) + (long long )l2 >= 0LL) && (-2LL
        + (long long )Alen) + (long long )k >= 0LL) && (-2LL + (long long )Alen) +
        (long long )found >= 0LL) && (-2LL + (long long )Alen) + (long long )j >=
        0LL) && (-2LL + (long long )Blen) + (long long )i >= 0LL) && (-2LL + (long
        long )k) + (long long )l1 >= 0LL) && (-2LL + (long long )i) + (long long )l2
        >= 0LL) && (-2LL + (long long )found) + (long long )l1 >= 0LL) && (-2LL +
        (long long )j) + (long long )l1 >= 0LL) && (-1LL + (long long )Blen) + (long
        long )found >= 0LL) && (-1LL + (long long )i) + (long long )k >= 0LL) && (-1LL
        + (long long )i) + (long long )j >= 0LL) && (-1LL + (long long )found) + (long
        long )i >= 0LL) && (-1LL + (long long )found) + (long long )l2 >= 0LL) &&
        (-1LL - (long long )found) + (long long )l1 >= 0LL) && (-1LL - (long long
        )j) + (long long )l1 >= 0LL) && (0LL - (long long )k) + (long long )l2 >=
        0LL) && (0LL - (long long )i) + (long long )l2 >= 0LL) && (0LL - (long long
        )found) + (long long )i >= 0LL) && (1LL - (long long )i) + (long long )k >=
        0LL) && (1LL - (long long )i) + (long long )j >= 0LL) && (1LL - (long long
        )j) + (long long )k >= 0LL) && (536870908LL - (long long )Blen) + (long long
        )l1 >= 0LL) && (536870909LL - (long long )Alen) + (long long )i >= 0LL) &&
        (536870909LL - (long long )Blen) + (long long )i >= 0LL) && (-1LL + (long
        long )Alen) - (long long )found >= 0LL) && (-1LL + (long long )Alen) - (long
        long )j >= 0LL) && (1LL + (long long )found) - (long long )k >= 0LL) && (1LL
        + (long long )found) - (long long )i >= 0LL) && (1LL + (long long )found)
        - (long long )j >= 0LL) && (1LL + (long long )j) - (long long )k >= 0LL) &&
        (536870908LL + (long long )Alen) - (long long )Blen >= 0LL) && (536870908LL
        + (long long )Alen) - (long long )l2 >= 0LL) && (536870908LL + (long long
        )l1) - (long long )l2 >= 0LL) && (536870909LL + (long long )i) - (long long
        )l1 >= 0LL) && (536870909LL + (long long )i) - (long long )l2 >= 0LL) && (1LL
        - (long long )found) - (long long )j >= 0LL) && (2LL - (long long )i) - (long
        long )k >= 0LL) && (2LL - (long long )i) - (long long )j >= 0LL) && (2LL -
        (long long )found) - (long long )k >= 0LL) && (2LL - (long long )found) -
        (long long )i >= 0LL) && (2LL - (long long )j) - (long long )k >= 0LL) &&
        (536870911LL - (long long )Alen) - (long long )k >= 0LL) && (536870911LL -
        (long long )Alen) - (long long )i >= 0LL) && (536870911LL - (long long )Alen)
        - (long long )j >= 0LL) && (536870911LL - (long long )Blen) - (long long )k
        >= 0LL) && (536870911LL - (long long )Blen) - (long long )i >= 0LL) && (536870911LL
        - (long long )Blen) - (long long )j >= 0LL) && (536870911LL - (long long )k)
        - (long long )l1 >= 0LL) && (536870911LL - (long long )k) - (long long )l2
        >= 0LL) && (536870911LL - (long long )i) - (long long )l1 >= 0LL) && (536870911LL
        - (long long )i) - (long long )l2 >= 0LL) && (536870911LL - (long long )j)
        - (long long )l1 >= 0LL) && (536870911LL - (long long )j) - (long long )l2
        >= 0LL) && (long long )Blen - (long long )k >= 0LL) && (long long )Blen -
        (long long )i >= 0LL) && (long long )i - (long long )j >= 0LL) && i == 1)
        && (k == 0 || k == 1)) && (j == 0 || j == 1)))) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= k && 4 <= l1) && k <= 3) && (-8LL + (long long )Alen) + (long long )l1
        >= 0LL) && (-7LL + (long long )Alen) + (long long )i >= 0LL) && (-7LL + (long
        long )i) + (long long )l1 >= 0LL) && (-5LL + (long long )Alen) + (long long
        )Blen >= 0LL) && (-5LL + (long long )Alen) + (long long )l2 >= 0LL) && (-5LL
        + (long long )Blen) + (long long )l1 >= 0LL) && (-5LL + (long long )l1) +
        (long long )l2 >= 0LL) && (-4LL + (long long )Alen) + (long long )k >= 0LL)
        && (-4LL + (long long )Alen) + (long long )found >= 0LL) && (-4LL + (long
        long )Alen) + (long long )j >= 0LL) && (-4LL + (long long )Blen) + (long long
        )i >= 0LL) && (-4LL + (long long )k) + (long long )l1 >= 0LL) && (-4LL + (long
        long )i) + (long long )l2 >= 0LL) && (-4LL + (long long )found) + (long long
        )l1 >= 0LL) && (-4LL + (long long )j) + (long long )l1 >= 0LL) && (-3LL +
        (long long )i) + (long long )k >= 0LL) && (-3LL + (long long )i) + (long long
        )j >= 0LL) && (-3LL + (long long )found) + (long long )i >= 0LL) && (-1LL
        + (long long )Blen) + (long long )found >= 0LL) && (-1LL + (long long )found)
        + (long long )l2 >= 0LL) && (-4LL - (long long )found) + (long long )l1 >=
        0LL) && (-4LL - (long long )j) + (long long )l1 >= 0LL) && (-3LL - (long long
        )found) + (long long )i >= 0LL) && (-1LL - (long long )found) + (long long
        )l2 >= 0LL) && (-1LL - (long long )j) + (long long )l2 >= 0LL) && (0LL - (long
        long )found) + (long long )k >= 0LL) && (0LL - (long long )found) + (long
        long )j >= 0LL) && (0LL - (long long )j) + (long long )k >= 0LL) && (2LL -
        (long long )k) + (long long )l2 >= 0LL) && (2LL - (long long )i) + (long long
        )l2 >= 0LL) && (3LL - (long long )i) + (long long )k >= 0LL) && (3LL - (long
        long )i) + (long long )j >= 0LL) && (536870906LL - (long long )Blen) + (long
        long )l1 >= 0LL) && (536870907LL - (long long )Alen) + (long long )i >= 0LL)
        && (536870907LL - (long long )Blen) + (long long )i >= 0LL) && (long long
        )found + (long long )j >= 0LL) && (-4LL + (long long )Alen) - (long long )found
        >= 0LL) && (-4LL + (long long )Alen) - (long long )j >= 0LL) && (-3LL + (long
        long )i) - (long long )j >= 0LL) && (-1LL + (long long )Blen) - (long long
        )found >= 0LL) && (-1LL + (long long )Blen) - (long long )j >= 0LL) && (2LL
        + (long long )Blen) - (long long )k >= 0LL) && (2LL + (long long )Blen) -
        (long long )i >= 0LL) && (3LL + (long long )found) - (long long )k >= 0LL)
        && (3LL + (long long )found) - (long long )i >= 0LL) && (3LL + (long long
        )j) - (long long )k >= 0LL) && (536870906LL + (long long )Alen) - (long long
        )Blen >= 0LL) && (536870906LL + (long long )Alen) - (long long )l2 >= 0LL)
        && (536870906LL + (long long )l1) - (long long )l2 >= 0LL) && (536870907LL
        + (long long )i) - (long long )l1 >= 0LL) && (536870907LL + (long long )i)
        - (long long )l2 >= 0LL) && (0LL - (long long )found) - (long long )j >= 0LL)
        && (3LL - (long long )i) - (long long )j >= 0LL) && (3LL - (long long )found)
        - (long long )k >= 0LL) && (3LL - (long long )found) - (long long )i >= 0LL)
        && (3LL - (long long )j) - (long long )k >= 0LL) && (6LL - (long long )i)
        - (long long )k >= 0LL) && (536870910LL - (long long )Alen) - (long long )found
        >= 0LL) && (536870910LL - (long long )Alen) - (long long )j >= 0LL) && (536870910LL
        - (long long )Blen) - (long long )found >= 0LL) && (536870910LL - (long long
        )Blen) - (long long )j >= 0LL) && (536870910LL - (long long )found) - (long
        long )l1 >= 0LL) && (536870910LL - (long long )found) - (long long )l2 >=
        0LL) && (536870910LL - (long long )j) - (long long )l1 >= 0LL) && (536870910LL
        - (long long )j) - (long long )l2 >= 0LL) && (536870913LL - (long long )Alen)
        - (long long )k >= 0LL) && (536870913LL - (long long )Alen) - (long long )i
        >= 0LL) && (536870913LL - (long long )Blen) - (long long )k >= 0LL) && (536870913LL
        - (long long )Blen) - (long long )i >= 0LL) && (536870913LL - (long long )k)
        - (long long )l1 >= 0LL) && (536870913LL - (long long )k) - (long long )l2
        >= 0LL) && (536870913LL - (long long )i) - (long long )l1 >= 0LL) && (536870913LL
        - (long long )i) - (long long )l2 >= 0LL) && (long long )found - (long long
        )j >= 0LL) && 0 == found) && 0 == j) && i == 3) && found == 0) && found ==
        j) && j == 0)) || (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((2
        <= l1 && (-4LL + (long long )Alen) + (long long )l1 >= 0LL) && (-3LL + (long
        long )Alen) + (long long )Blen >= 0LL) && (-3LL + (long long )Alen) + (long
        long )i >= 0LL) && (-3LL + (long long )Alen) + (long long )l2 >= 0LL) && (-3LL
        + (long long )Blen) + (long long )l1 >= 0LL) && (-3LL + (long long )i) + (long
        long )l1 >= 0LL) && (-3LL + (long long )l1) + (long long )l2 >= 0LL) && (-2LL
        + (long long )Alen) + (long long )k >= 0LL) && (-2LL + (long long )Alen) +
        (long long )found >= 0LL) && (-2LL + (long long )Alen) + (long long )j >=
        0LL) && (-2LL + (long long )Blen) + (long long )i >= 0LL) && (-2LL + (long
        long )k) + (long long )l1 >= 0LL) && (-2LL + (long long )i) + (long long )l2
        >= 0LL) && (-2LL + (long long )found) + (long long )l1 >= 0LL) && (-2LL +
        (long long )j) + (long long )l1 >= 0LL) && (-1LL + (long long )Blen) + (long
        long )found >= 0LL) && (-1LL + (long long )i) + (long long )k >= 0LL) && (-1LL
        + (long long )i) + (long long )j >= 0LL) && (-1LL + (long long )found) + (long
        long )i >= 0LL) && (-1LL + (long long )found) + (long long )l2 >= 0LL) &&
        (-2LL - (long long )found) + (long long )l1 >= 0LL) && (-2LL - (long long
        )j) + (long long )l1 >= 0LL) && (-1LL - (long long )found) + (long long )i
        >= 0LL) && (-1LL - (long long )found) + (long long )l2 >= 0LL) && (-1LL -
        (long long )j) + (long long )l2 >= 0LL) && (0LL - (long long )k) + (long long
        )l2 >= 0LL) && (0LL - (long long )i) + (long long )l2 >= 0LL) && (0LL - (long
        long )found) + (long long )k >= 0LL) && (0LL - (long long )found) + (long
        long )j >= 0LL) && (0LL - (long long )j) + (long long )k >= 0LL) && (1LL -
        (long long )i) + (long long )k >= 0LL) && (1LL - (long long )i) + (long long
        )j >= 0LL) && (536870908LL - (long long )Blen) + (long long )l1 >= 0LL) &&
        (536870909LL - (long long )Alen) + (long long )i >= 0LL) && (536870909LL -
        (long long )Blen) + (long long )i >= 0LL) && (long long )found + (long long
        )j >= 0LL) && (-2LL + (long long )Alen) - (long long )found >= 0LL) && (-2LL
        + (long long )Alen) - (long long )j >= 0LL) && (-1LL + (long long )Blen) -
        (long long )found >= 0LL) && (-1LL + (long long )Blen) - (long long )j >=
        0LL) && (-1LL + (long long )i) - (long long )j >= 0LL) && (1LL + (long long
        )found) - (long long )k >= 0LL) && (1LL + (long long )found) - (long long
        )i >= 0LL) && (1LL + (long long )j) - (long long )k >= 0LL) && (536870908LL
        + (long long )Alen) - (long long )Blen >= 0LL) && (536870908LL + (long long
        )Alen) - (long long )l2 >= 0LL) && (536870908LL + (long long )l1) - (long
        long )l2 >= 0LL) && (536870909LL + (long long )i) - (long long )l1 >= 0LL)
        && (536870909LL + (long long )i) - (long long )l2 >= 0LL) && (0LL - (long
        long )found) - (long long )j >= 0LL) && (1LL - (long long )i) - (long long
        )j >= 0LL) && (1LL - (long long )found) - (long long )k >= 0LL) && (1LL -
        (long long )found) - (long long )i >= 0LL) && (1LL - (long long )j) - (long
        long )k >= 0LL) && (2LL - (long long )i) - (long long )k >= 0LL) && (536870910LL
        - (long long )Alen) - (long long )found >= 0LL) && (536870910LL - (long long
        )Alen) - (long long )j >= 0LL) && (536870910LL - (long long )Blen) - (long
        long )found >= 0LL) && (536870910LL - (long long )Blen) - (long long )j >=
        0LL) && (536870910LL - (long long )found) - (long long )l1 >= 0LL) && (536870910LL
        - (long long )found) - (long long )l2 >= 0LL) && (536870910LL - (long long
        )j) - (long long )l1 >= 0LL) && (536870910LL - (long long )j) - (long long
        )l2 >= 0LL) && (536870911LL - (long long )Alen) - (long long )k >= 0LL) &&
        (536870911LL - (long long )Alen) - (long long )i >= 0LL) && (536870911LL -
        (long long )Blen) - (long long )k >= 0LL) && (536870911LL - (long long )Blen)
        - (long long )i >= 0LL) && (536870911LL - (long long )k) - (long long )l1
        >= 0LL) && (536870911LL - (long long )k) - (long long )l2 >= 0LL) && (536870911LL
        - (long long )i) - (long long )l1 >= 0LL) && (536870911LL - (long long )i)
        - (long long )l2 >= 0LL) && (long long )Blen - (long long )k >= 0LL) && (long
        long )Blen - (long long )i >= 0LL) && (long long )found - (long long )j >=
        0LL) && 0 == found) && 0 == j) && i == 1) && found == 0) && found == j) &&
        j == 0) && (k == 0 || k == 1))) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= k && 0 <= j) && 4 <= i) && 5 <= l1) && i <= 536870909) && j <= 536870910)
        && (-10LL + (long long )Alen) + (long long )l1 >= 0LL) && (-9LL + (long long
        )Alen) + (long long )i >= 0LL) && (-9LL + (long long )i) + (long long )l1
        >= 0LL) && (-6LL + (long long )Alen) + (long long )Blen >= 0LL) && (-6LL +
        (long long )Alen) + (long long )l2 >= 0LL) && (-6LL + (long long )Blen) +
        (long long )l1 >= 0LL) && (-6LL + (long long )l1) + (long long )l2 >= 0LL)
        && (-5LL + (long long )Alen) + (long long )k >= 0LL) && (-5LL + (long long
        )Alen) + (long long )found >= 0LL) && (-5LL + (long long )Alen) + (long long
        )j >= 0LL) && (-5LL + (long long )Blen) + (long long )i >= 0LL) && (-5LL +
        (long long )k) + (long long )l1 >= 0LL) && (-5LL + (long long )i) + (long
        long )l2 >= 0LL) && (-5LL + (long long )found) + (long long )l1 >= 0LL) &&
        (-5LL + (long long )j) + (long long )l1 >= 0LL) && (-4LL + (long long )i)
        + (long long )k >= 0LL) && (-4LL + (long long )i) + (long long )j >= 0LL)
        && (-4LL + (long long )found) + (long long )i >= 0LL) && (-2LL + (long long
        )Blen) + (long long )found >= 0LL) && (-2LL + (long long )found) + (long long
        )l2 >= 0LL) && (-1LL + (long long )found) + (long long )j >= 0LL) && (-4LL
        - (long long )found) + (long long )l1 >= 0LL) && (-3LL - (long long )found)
        + (long long )i >= 0LL) && (0LL - (long long )found) + (long long )l2 >= 0LL)
        && (0LL - (long long )j) + (long long )l2 >= 0LL) && (1LL - (long long )found)
        + (long long )k >= 0LL) && (1LL - (long long )found) + (long long )j >= 0LL)
        && (536870905LL - (long long )Blen) + (long long )l1 >= 0LL) && (536870905LL
        - (long long )j) + (long long )l1 >= 0LL) && (536870906LL - (long long )Alen)
        + (long long )i >= 0LL) && (536870906LL - (long long )Blen) + (long long )i
        >= 0LL) && (536870908LL - (long long )k) + (long long )l2 >= 0LL) && (536870908LL
        - (long long )i) + (long long )l2 >= 0LL) && (536870909LL - (long long )i)
        + (long long )k >= 0LL) && (536870909LL - (long long )i) + (long long )j >=
        0LL) && (536870910LL - (long long )j) + (long long )k >= 0LL) && (-4LL + (long
        long )Alen) - (long long )found >= 0LL) && (536870905LL + (long long )Alen)
        - (long long )Blen >= 0LL) && (536870905LL + (long long )Alen) - (long long
        )l2 >= 0LL) && (536870905LL + (long long )Alen) - (long long )j >= 0LL) &&
        (536870905LL + (long long )l1) - (long long )l2 >= 0LL) && (536870906LL +
        (long long )i) - (long long )l1 >= 0LL) && (536870906LL + (long long )i) -
        (long long )l2 >= 0LL) && (536870906LL + (long long )i) - (long long )j >=
        0LL) && (536870908LL + (long long )Blen) - (long long )k >= 0LL) && (536870908LL
        + (long long )Blen) - (long long )i >= 0LL) && (536870909LL + (long long )found)
        - (long long )k >= 0LL) && (536870909LL + (long long )found) - (long long
        )i >= 0LL) && (536870909LL + (long long )j) - (long long )k >= 0LL) && (536870910LL
        + (long long )found) - (long long )j >= 0LL) && (536870910LL - (long long
        )found) - (long long )k >= 0LL) && (536870910LL - (long long )found) - (long
        long )i >= 0LL) && (536870911LL - (long long )Alen) - (long long )found >=
        0LL) && (536870911LL - (long long )Blen) - (long long )found >= 0LL) && (536870911LL
        - (long long )found) - (long long )l1 >= 0LL) && (536870911LL - (long long
        )found) - (long long )l2 >= 0LL) && (536870911LL - (long long )found) - (long
        long )j >= 0LL) && (1073741818LL - (long long )i) - (long long )k >= 0LL)
        && (1073741819LL - (long long )Alen) - (long long )k >= 0LL) && (1073741819LL
        - (long long )Alen) - (long long )i >= 0LL) && (1073741819LL - (long long
        )Blen) - (long long )k >= 0LL) && (1073741819LL - (long long )Blen) - (long
        long )i >= 0LL) && (1073741819LL - (long long )k) - (long long )l1 >= 0LL)
        && (1073741819LL - (long long )k) - (long long )l2 >= 0LL) && (1073741819LL
        - (long long )i) - (long long )l1 >= 0LL) && (1073741819LL - (long long )i)
        - (long long )l2 >= 0LL) && (1073741819LL - (long long )i) - (long long )j
        >= 0LL) && (1073741819LL - (long long )j) - (long long )k >= 0LL) && (1073741820LL
        - (long long )Alen) - (long long )j >= 0LL) && (1073741820LL - (long long
        )Blen) - (long long )j >= 0LL) && (1073741820LL - (long long )j) - (long long
        )l1 >= 0LL) && (1073741820LL - (long long )j) - (long long )l2 >= 0LL) &&
        (long long )Blen - (long long )found >= 0LL) && (long long )Blen - (long long
        )j >= 0LL) && (found == 0 || found == 1))) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= k && 0 <= j) && 3 <= l1) && k <= 2) && j <= 536870910) && (-6LL + (long
        long )Alen) + (long long )l1 >= 0LL) && (-5LL + (long long )Alen) + (long
        long )i >= 0LL) && (-5LL + (long long )i) + (long long )l1 >= 0LL) && (-4LL
        + (long long )Alen) + (long long )Blen >= 0LL) && (-4LL + (long long )Alen)
        + (long long )l2 >= 0LL) && (-4LL + (long long )Blen) + (long long )l1 >=
        0LL) && (-4LL + (long long )l1) + (long long )l2 >= 0LL) && (-3LL + (long
        long )Alen) + (long long )k >= 0LL) && (-3LL + (long long )Alen) + (long long
        )found >= 0LL) && (-3LL + (long long )Alen) + (long long )j >= 0LL) && (-3LL
        + (long long )Blen) + (long long )i >= 0LL) && (-3LL + (long long )k) + (long
        long )l1 >= 0LL) && (-3LL + (long long )i) + (long long )l2 >= 0LL) && (-3LL
        + (long long )found) + (long long )l1 >= 0LL) && (-3LL + (long long )j) +
        (long long )l1 >= 0LL) && (-2LL + (long long )Blen) + (long long )found >=
        0LL) && (-2LL + (long long )i) + (long long )k >= 0LL) && (-2LL + (long long
        )i) + (long long )j >= 0LL) && (-2LL + (long long )found) + (long long )i
        >= 0LL) && (-2LL + (long long )found) + (long long )l2 >= 0LL) && (-1LL +
        (long long )found) + (long long )j >= 0LL) && (-2LL - (long long )found) +
        (long long )l1 >= 0LL) && (-1LL - (long long )found) + (long long )i >= 0LL)
        && (0LL - (long long )found) + (long long )l2 >= 0LL) && (0LL - (long long
        )j) + (long long )l2 >= 0LL) && (1LL - (long long )k) + (long long )l2 >=
        0LL) && (1LL - (long long )i) + (long long )l2 >= 0LL) && (1LL - (long long
        )found) + (long long )k >= 0LL) && (1LL - (long long )found) + (long long
        )j >= 0LL) && (2LL - (long long )i) + (long long )k >= 0LL) && (2LL - (long
        long )i) + (long long )j >= 0LL) && (536870907LL - (long long )Blen) + (long
        long )l1 >= 0LL) && (536870907LL - (long long )j) + (long long )l1 >= 0LL)
        && (536870908LL - (long long )Alen) + (long long )i >= 0LL) && (536870908LL
        - (long long )Blen) + (long long )i >= 0LL) && (536870910LL - (long long )j)
        + (long long )k >= 0LL) && (-2LL + (long long )Alen) - (long long )found >=
        0LL) && (1LL + (long long )Blen) - (long long )k >= 0LL) && (1LL + (long long
        )Blen) - (long long )i >= 0LL) && (2LL + (long long )found) - (long long )k
        >= 0LL) && (2LL + (long long )found) - (long long )i >= 0LL) && (2LL + (long
        long )j) - (long long )k >= 0LL) && (536870907LL + (long long )Alen) - (long
        long )Blen >= 0LL) && (536870907LL + (long long )Alen) - (long long )l2 >=
        0LL) && (536870907LL + (long long )Alen) - (long long )j >= 0LL) && (536870907LL
        + (long long )l1) - (long long )l2 >= 0LL) && (536870908LL + (long long )i)
        - (long long )l1 >= 0LL) && (536870908LL + (long long )i) - (long long )l2
        >= 0LL) && (536870908LL + (long long )i) - (long long )j >= 0LL) && (536870910LL
        + (long long )found) - (long long )j >= 0LL) && (3LL - (long long )found)
        - (long long )k >= 0LL) && (3LL - (long long )found) - (long long )i >= 0LL)
        && (4LL - (long long )i) - (long long )k >= 0LL) && (536870911LL - (long long
        )Alen) - (long long )found >= 0LL) && (536870911LL - (long long )Blen) - (long
        long )found >= 0LL) && (536870911LL - (long long )found) - (long long )l1
        >= 0LL) && (536870911LL - (long long )found) - (long long )l2 >= 0LL) && (536870911LL
        - (long long )found) - (long long )j >= 0LL) && (536870912LL - (long long
        )Alen) - (long long )k >= 0LL) && (536870912LL - (long long )Alen) - (long
        long )i >= 0LL) && (536870912LL - (long long )Blen) - (long long )k >= 0LL)
        && (536870912LL - (long long )Blen) - (long long )i >= 0LL) && (536870912LL
        - (long long )k) - (long long )l1 >= 0LL) && (536870912LL - (long long )k)
        - (long long )l2 >= 0LL) && (536870912LL - (long long )i) - (long long )l1
        >= 0LL) && (536870912LL - (long long )i) - (long long )l2 >= 0LL) && (536870912LL
        - (long long )i) - (long long )j >= 0LL) && (536870912LL - (long long )j)
        - (long long )k >= 0LL) && (1073741820LL - (long long )Alen) - (long long
        )j >= 0LL) && (1073741820LL - (long long )Blen) - (long long )j >= 0LL) &&
        (1073741820LL - (long long )j) - (long long )l1 >= 0LL) && (1073741820LL -
        (long long )j) - (long long )l2 >= 0LL) && (long long )Blen - (long long )found
        >= 0LL) && (long long )Blen - (long long )j >= 0LL) && i == 2) && (found ==
        0 || found == 1))) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= k && 0 <= j) && 4 <= i) && 5 <= l1) && i <= 536870909) && j <= 3) && (-10LL
        + (long long )Alen) + (long long )l1 >= 0LL) && (-9LL + (long long )Alen)
        + (long long )i >= 0LL) && (-9LL + (long long )i) + (long long )l1 >= 0LL)
        && (-6LL + (long long )Alen) + (long long )Blen >= 0LL) && (-6LL + (long long
        )Alen) + (long long )l2 >= 0LL) && (-6LL + (long long )Blen) + (long long
        )l1 >= 0LL) && (-6LL + (long long )l1) + (long long )l2 >= 0LL) && (-5LL +
        (long long )Alen) + (long long )k >= 0LL) && (-5LL + (long long )Alen) + (long
        long )found >= 0LL) && (-5LL + (long long )Alen) + (long long )j >= 0LL) &&
        (-5LL + (long long )Blen) + (long long )i >= 0LL) && (-5LL + (long long )k)
        + (long long )l1 >= 0LL) && (-5LL + (long long )i) + (long long )l2 >= 0LL)
        && (-5LL + (long long )found) + (long long )l1 >= 0LL) && (-5LL + (long long
        )j) + (long long )l1 >= 0LL) && (-4LL + (long long )i) + (long long )k >=
        0LL) && (-4LL + (long long )i) + (long long )j >= 0LL) && (-4LL + (long long
        )found) + (long long )i >= 0LL) && (-2LL + (long long )Blen) + (long long
        )found >= 0LL) && (-2LL + (long long )found) + (long long )l2 >= 0LL) && (-1LL
        + (long long )found) + (long long )j >= 0LL) && (-4LL - (long long )found)
        + (long long )l1 >= 0LL) && (-3LL - (long long )found) + (long long )i >=
        0LL) && (-2LL - (long long )j) + (long long )l1 >= 0LL) && (0LL - (long long
        )found) + (long long )l2 >= 0LL) && (0LL - (long long )j) + (long long )l2
        >= 0LL) && (1LL - (long long )found) + (long long )k >= 0LL) && (1LL - (long
        long )found) + (long long )j >= 0LL) && (3LL - (long long )j) + (long long
        )k >= 0LL) && (536870905LL - (long long )Blen) + (long long )l1 >= 0LL) &&
        (536870906LL - (long long )Alen) + (long long )i >= 0LL) && (536870906LL -
        (long long )Blen) + (long long )i >= 0LL) && (536870908LL - (long long )k)
        + (long long )l2 >= 0LL) && (536870908LL - (long long )i) + (long long )l2
        >= 0LL) && (536870909LL - (long long )i) + (long long )k >= 0LL) && (536870909LL
        - (long long )i) + (long long )j >= 0LL) && (-4LL + (long long )Alen) - (long
        long )found >= 0LL) && (-2LL + (long long )Alen) - (long long )j >= 0LL) &&
        (-1LL + (long long )i) - (long long )j >= 0LL) && (3LL + (long long )found)
        - (long long )j >= 0LL) && (536870905LL + (long long )Alen) - (long long )Blen
        >= 0LL) && (536870905LL + (long long )Alen) - (long long )l2 >= 0LL) && (536870905LL
        + (long long )l1) - (long long )l2 >= 0LL) && (536870906LL + (long long )i)
        - (long long )l1 >= 0LL) && (536870906LL + (long long )i) - (long long )l2
        >= 0LL) && (536870908LL + (long long )Blen) - (long long )k >= 0LL) && (536870908LL
        + (long long )Blen) - (long long )i >= 0LL) && (536870909LL + (long long )found)
        - (long long )k >= 0LL) && (536870909LL + (long long )found) - (long long
        )i >= 0LL) && (536870909LL + (long long )j) - (long long )k >= 0LL) && (3LL
        - (long long )found) - (long long )j >= 0LL) && (536870910LL - (long long
        )found) - (long long )k >= 0LL) && (536870910LL - (long long )found) - (long
        long )i >= 0LL) && (536870911LL - (long long )Alen) - (long long )found >=
        0LL) && (536870911LL - (long long )Blen) - (long long )found >= 0LL) && (536870911LL
        - (long long )found) - (long long )l1 >= 0LL) && (536870911LL - (long long
        )found) - (long long )l2 >= 0LL) && (536870912LL - (long long )i) - (long
        long )j >= 0LL) && (536870912LL - (long long )j) - (long long )k >= 0LL) &&
        (536870913LL - (long long )Alen) - (long long )j >= 0LL) && (536870913LL -
        (long long )Blen) - (long long )j >= 0LL) && (536870913LL - (long long )j)
        - (long long )l1 >= 0LL) && (536870913LL - (long long )j) - (long long )l2
        >= 0LL) && (1073741818LL - (long long )i) - (long long )k >= 0LL) && (1073741819LL
        - (long long )Alen) - (long long )k >= 0LL) && (1073741819LL - (long long
        )Alen) - (long long )i >= 0LL) && (1073741819LL - (long long )Blen) - (long
        long )k >= 0LL) && (1073741819LL - (long long )Blen) - (long long )i >= 0LL)
        && (1073741819LL - (long long )k) - (long long )l1 >= 0LL) && (1073741819LL
        - (long long )k) - (long long )l2 >= 0LL) && (1073741819LL - (long long )i)
        - (long long )l1 >= 0LL) && (1073741819LL - (long long )i) - (long long )l2
        >= 0LL) && (long long )Blen - (long long )found >= 0LL) && (long long )Blen
        - (long long )j >= 0LL) && (found == 0 || found == 1))) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= j && 1 <= l1) && j <= 536870910) && (-2LL + (long long )Alen) + (long long
        )Blen >= 0LL) && (-2LL + (long long )Alen) + (long long )l1 >= 0LL) && (-2LL
        + (long long )Alen) + (long long )l2 >= 0LL) && (-2LL + (long long )Blen)
        + (long long )l1 >= 0LL) && (-2LL + (long long )Blen) + (long long )found
        >= 0LL) && (-2LL + (long long )l1) + (long long )l2 >= 0LL) && (-2LL + (long
        long )found) + (long long )l2 >= 0LL) && (-1LL + (long long )Alen) + (long
        long )k >= 0LL) && (-1LL + (long long )Alen) + (long long )i >= 0LL) && (-1LL
        + (long long )Alen) + (long long )found >= 0LL) && (-1LL + (long long )Alen)
        + (long long )j >= 0LL) && (-1LL + (long long )Blen) + (long long )i >= 0LL)
        && (-1LL + (long long )k) + (long long )l1 >= 0LL) && (-1LL + (long long )i)
        + (long long )l1 >= 0LL) && (-1LL + (long long )i) + (long long )l2 >= 0LL)
        && (-1LL + (long long )found) + (long long )l1 >= 0LL) && (-1LL + (long long
        )found) + (long long )j >= 0LL) && (-1LL + (long long )j) + (long long )l1
        >= 0LL) && (-1LL - (long long )k) + (long long )l2 >= 0LL) && (-1LL - (long
        long )i) + (long long )l2 >= 0LL) && (0LL - (long long )i) + (long long )k
        >= 0LL) && (0LL - (long long )i) + (long long )j >= 0LL) && (0LL - (long long
        )found) + (long long )l1 >= 0LL) && (0LL - (long long )found) + (long long
        )l2 >= 0LL) && (0LL - (long long )j) + (long long )l2 >= 0LL) && (1LL - (long
        long )found) + (long long )k >= 0LL) && (1LL - (long long )found) + (long
        long )i >= 0LL) && (1LL - (long long )found) + (long long )j >= 0LL) && (536870909LL
        - (long long )Blen) + (long long )l1 >= 0LL) && (536870909LL - (long long
        )j) + (long long )l1 >= 0LL) && (536870910LL - (long long )Alen) + (long long
        )i >= 0LL) && (536870910LL - (long long )Blen) + (long long )i >= 0LL) &&
        (536870910LL - (long long )j) + (long long )k >= 0LL) && (long long )i + (long
        long )k >= 0LL) && (long long )i + (long long )j >= 0LL) && (long long )found
        + (long long )i >= 0LL) && (-1LL + (long long )Blen) - (long long )k >= 0LL)
        && (-1LL + (long long )Blen) - (long long )i >= 0LL) && (536870909LL + (long
        long )Alen) - (long long )Blen >= 0LL) && (536870909LL + (long long )Alen)
        - (long long )l2 >= 0LL) && (536870909LL + (long long )Alen) - (long long
        )j >= 0LL) && (536870909LL + (long long )l1) - (long long )l2 >= 0LL) && (536870910LL
        + (long long )i) - (long long )l1 >= 0LL) && (536870910LL + (long long )i)
        - (long long )l2 >= 0LL) && (536870910LL + (long long )i) - (long long )j
        >= 0LL) && (536870910LL + (long long )found) - (long long )j >= 0LL) && (0LL
        - (long long )i) - (long long )k >= 0LL) && (1LL - (long long )found) - (long
        long )k >= 0LL) && (1LL - (long long )found) - (long long )i >= 0LL) && (536870910LL
        - (long long )Alen) - (long long )k >= 0LL) && (536870910LL - (long long )Alen)
        - (long long )i >= 0LL) && (536870910LL - (long long )Blen) - (long long )k
        >= 0LL) && (536870910LL - (long long )Blen) - (long long )i >= 0LL) && (536870910LL
        - (long long )k) - (long long )l1 >= 0LL) && (536870910LL - (long long )k)
        - (long long )l2 >= 0LL) && (536870910LL - (long long )i) - (long long )l1
        >= 0LL) && (536870910LL - (long long )i) - (long long )l2 >= 0LL) && (536870910LL
        - (long long )i) - (long long )j >= 0LL) && (536870910LL - (long long )j)
        - (long long )k >= 0LL) && (536870911LL - (long long )Alen) - (long long )found
        >= 0LL) && (536870911LL - (long long )Blen) - (long long )found >= 0LL) &&
        (536870911LL - (long long )found) - (long long )l1 >= 0LL) && (536870911LL
        - (long long )found) - (long long )l2 >= 0LL) && (536870911LL - (long long
        )found) - (long long )j >= 0LL) && (1073741820LL - (long long )Alen) - (long
        long )j >= 0LL) && (1073741820LL - (long long )Blen) - (long long )j >= 0LL)
        && (1073741820LL - (long long )j) - (long long )l1 >= 0LL) && (1073741820LL
        - (long long )j) - (long long )l2 >= 0LL) && (long long )Alen - (long long
        )found >= 0LL) && (long long )Blen - (long long )found >= 0LL) && (long long
        )Blen - (long long )j >= 0LL) && (long long )found - (long long )k >= 0LL)
        && (long long )found - (long long )i >= 0LL) && (long long )j - (long long
        )k >= 0LL) && 0 == k) && 0 == i) && k == 0) && k == i) && i == 0) && (found
        == 0 || found == 1))) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= k && 0 <= j) && 3 <= l1) && k <= 2) && j <= 3) && (-6LL + (long long )Alen)
        + (long long )l1 >= 0LL) && (-5LL + (long long )Alen) + (long long )i >= 0LL)
        && (-5LL + (long long )i) + (long long )l1 >= 0LL) && (-4LL + (long long )Alen)
        + (long long )Blen >= 0LL) && (-4LL + (long long )Alen) + (long long )l2 >=
        0LL) && (-4LL + (long long )Blen) + (long long )l1 >= 0LL) && (-4LL + (long
        long )l1) + (long long )l2 >= 0LL) && (-3LL + (long long )Alen) + (long long
        )k >= 0LL) && (-3LL + (long long )Alen) + (long long )found >= 0LL) && (-3LL
        + (long long )Alen) + (long long )j >= 0LL) && (-3LL + (long long )Blen) +
        (long long )i >= 0LL) && (-3LL + (long long )k) + (long long )l1 >= 0LL) &&
        (-3LL + (long long )i) + (long long )l2 >= 0LL) && (-3LL + (long long )found)
        + (long long )l1 >= 0LL) && (-3LL + (long long )j) + (long long )l1 >= 0LL)
        && (-2LL + (long long )Blen) + (long long )found >= 0LL) && (-2LL + (long
        long )i) + (long long )k >= 0LL) && (-2LL + (long long )i) + (long long )j
        >= 0LL) && (-2LL + (long long )found) + (long long )i >= 0LL) && (-2LL + (long
        long )found) + (long long )l2 >= 0LL) && (-1LL + (long long )found) + (long
        long )j >= 0LL) && (-2LL - (long long )found) + (long long )l1 >= 0LL) &&
        (-1LL - (long long )found) + (long long )i >= 0LL) && (0LL - (long long )found)
        + (long long )l2 >= 0LL) && (0LL - (long long )j) + (long long )l1 >= 0LL)
        && (0LL - (long long )j) + (long long )l2 >= 0LL) && (1LL - (long long )k)
        + (long long )l2 >= 0LL) && (1LL - (long long )i) + (long long )l2 >= 0LL)
        && (1LL - (long long )found) + (long long )k >= 0LL) && (1LL - (long long
        )found) + (long long )j >= 0LL) && (2LL - (long long )i) + (long long )k >=
        0LL) && (2LL - (long long )i) + (long long )j >= 0LL) && (3LL - (long long
        )j) + (long long )k >= 0LL) && (536870907LL - (long long )Blen) + (long long
        )l1 >= 0LL) && (536870908LL - (long long )Alen) + (long long )i >= 0LL) &&
        (536870908LL - (long long )Blen) + (long long )i >= 0LL) && (-2LL + (long
        long )Alen) - (long long )found >= 0LL) && (1LL + (long long )Blen) - (long
        long )k >= 0LL) && (1LL + (long long )Blen) - (long long )i >= 0LL) && (1LL
        + (long long )i) - (long long )j >= 0LL) && (2LL + (long long )found) - (long
        long )k >= 0LL) && (2LL + (long long )found) - (long long )i >= 0LL) && (2LL
        + (long long )j) - (long long )k >= 0LL) && (3LL + (long long )found) - (long
        long )j >= 0LL) && (536870907LL + (long long )Alen) - (long long )Blen >=
        0LL) && (536870907LL + (long long )Alen) - (long long )l2 >= 0LL) && (536870907LL
        + (long long )l1) - (long long )l2 >= 0LL) && (536870908LL + (long long )i)
        - (long long )l1 >= 0LL) && (536870908LL + (long long )i) - (long long )l2
        >= 0LL) && (3LL - (long long )found) - (long long )k >= 0LL) && (3LL - (long
        long )found) - (long long )i >= 0LL) && (3LL - (long long )found) - (long
        long )j >= 0LL) && (4LL - (long long )i) - (long long )k >= 0LL) && (5LL -
        (long long )i) - (long long )j >= 0LL) && (5LL - (long long )j) - (long long
        )k >= 0LL) && (536870911LL - (long long )Alen) - (long long )found >= 0LL)
        && (536870911LL - (long long )Blen) - (long long )found >= 0LL) && (536870911LL
        - (long long )found) - (long long )l1 >= 0LL) && (536870911LL - (long long
        )found) - (long long )l2 >= 0LL) && (536870912LL - (long long )Alen) - (long
        long )k >= 0LL) && (536870912LL - (long long )Alen) - (long long )i >= 0LL)
        && (536870912LL - (long long )Blen) - (long long )k >= 0LL) && (536870912LL
        - (long long )Blen) - (long long )i >= 0LL) && (536870912LL - (long long )k)
        - (long long )l1 >= 0LL) && (536870912LL - (long long )k) - (long long )l2
        >= 0LL) && (536870912LL - (long long )i) - (long long )l1 >= 0LL) && (536870912LL
        - (long long )i) - (long long )l2 >= 0LL) && (536870913LL - (long long )Alen)
        - (long long )j >= 0LL) && (536870913LL - (long long )Blen) - (long long )j
        >= 0LL) && (536870913LL - (long long )j) - (long long )l1 >= 0LL) && (536870913LL
        - (long long )j) - (long long )l2 >= 0LL) && (long long )Alen - (long long
        )j >= 0LL) && (long long )Blen - (long long )found >= 0LL) && (long long )Blen
        - (long long )j >= 0LL) && i == 2) && (found == 0 || found == 1))) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= k && 0 <= j) && 4 <= i) && 5 <= l1) && i <= 536870909) && j <= 2) && (-10LL
        + (long long )Alen) + (long long )l1 >= 0LL) && (-9LL + (long long )Alen)
        + (long long )i >= 0LL) && (-9LL + (long long )i) + (long long )l1 >= 0LL)
        && (-6LL + (long long )Alen) + (long long )Blen >= 0LL) && (-6LL + (long long
        )Alen) + (long long )l2 >= 0LL) && (-6LL + (long long )Blen) + (long long
        )l1 >= 0LL) && (-6LL + (long long )l1) + (long long )l2 >= 0LL) && (-5LL +
        (long long )Alen) + (long long )k >= 0LL) && (-5LL + (long long )Alen) + (long
        long )found >= 0LL) && (-5LL + (long long )Alen) + (long long )j >= 0LL) &&
        (-5LL + (long long )Blen) + (long long )i >= 0LL) && (-5LL + (long long )k)
        + (long long )l1 >= 0LL) && (-5LL + (long long )i) + (long long )l2 >= 0LL)
        && (-5LL + (long long )found) + (long long )l1 >= 0LL) && (-5LL + (long long
        )j) + (long long )l1 >= 0LL) && (-4LL + (long long )i) + (long long )k >=
        0LL) && (-4LL + (long long )i) + (long long )j >= 0LL) && (-4LL + (long long
        )found) + (long long )i >= 0LL) && (-2LL + (long long )Blen) + (long long
        )found >= 0LL) && (-2LL + (long long )found) + (long long )l2 >= 0LL) && (-1LL
        + (long long )found) + (long long )j >= 0LL) && (-4LL - (long long )found)
        + (long long )l1 >= 0LL) && (-3LL - (long long )found) + (long long )i >=
        0LL) && (-3LL - (long long )j) + (long long )l1 >= 0LL) && (0LL - (long long
        )found) + (long long )l2 >= 0LL) && (0LL - (long long )j) + (long long )l2
        >= 0LL) && (1LL - (long long )found) + (long long )k >= 0LL) && (1LL - (long
        long )found) + (long long )j >= 0LL) && (2LL - (long long )j) + (long long
        )k >= 0LL) && (536870905LL - (long long )Blen) + (long long )l1 >= 0LL) &&
        (536870906LL - (long long )Alen) + (long long )i >= 0LL) && (536870906LL -
        (long long )Blen) + (long long )i >= 0LL) && (536870908LL - (long long )k)
        + (long long )l2 >= 0LL) && (536870908LL - (long long )i) + (long long )l2
        >= 0LL) && (536870909LL - (long long )i) + (long long )k >= 0LL) && (536870909LL
        - (long long )i) + (long long )j >= 0LL) && (-4LL + (long long )Alen) - (long
        long )found >= 0LL) && (-3LL + (long long )Alen) - (long long )j >= 0LL) &&
        (-2LL + (long long )i) - (long long )j >= 0LL) && (2LL + (long long )found)
        - (long long )j >= 0LL) && (536870905LL + (long long )Alen) - (long long )Blen
        >= 0LL) && (536870905LL + (long long )Alen) - (long long )l2 >= 0LL) && (536870905LL
        + (long long )l1) - (long long )l2 >= 0LL) && (536870906LL + (long long )i)
        - (long long )l1 >= 0LL) && (536870906LL + (long long )i) - (long long )l2
        >= 0LL) && (536870908LL + (long long )Blen) - (long long )k >= 0LL) && (536870908LL
        + (long long )Blen) - (long long )i >= 0LL) && (536870909LL + (long long )found)
        - (long long )k >= 0LL) && (536870909LL + (long long )found) - (long long
        )i >= 0LL) && (536870909LL + (long long )j) - (long long )k >= 0LL) && (2LL
        - (long long )found) - (long long )j >= 0LL) && (536870910LL - (long long
        )found) - (long long )k >= 0LL) && (536870910LL - (long long )found) - (long
        long )i >= 0LL) && (536870911LL - (long long )Alen) - (long long )found >=
        0LL) && (536870911LL - (long long )Blen) - (long long )found >= 0LL) && (536870911LL
        - (long long )i) - (long long )j >= 0LL) && (536870911LL - (long long )found)
        - (long long )l1 >= 0LL) && (536870911LL - (long long )found) - (long long
        )l2 >= 0LL) && (536870911LL - (long long )j) - (long long )k >= 0LL) && (536870912LL
        - (long long )Alen) - (long long )j >= 0LL) && (536870912LL - (long long )Blen)
        - (long long )j >= 0LL) && (536870912LL - (long long )j) - (long long )l1
        >= 0LL) && (536870912LL - (long long )j) - (long long )l2 >= 0LL) && (1073741818LL
        - (long long )i) - (long long )k >= 0LL) && (1073741819LL - (long long )Alen)
        - (long long )k >= 0LL) && (1073741819LL - (long long )Alen) - (long long
        )i >= 0LL) && (1073741819LL - (long long )Blen) - (long long )k >= 0LL) &&
        (1073741819LL - (long long )Blen) - (long long )i >= 0LL) && (1073741819LL
        - (long long )k) - (long long )l1 >= 0LL) && (1073741819LL - (long long )k)
        - (long long )l2 >= 0LL) && (1073741819LL - (long long )i) - (long long )l1
        >= 0LL) && (1073741819LL - (long long )i) - (long long )l2 >= 0LL) && (long
        long )Blen - (long long )found >= 0LL) && (long long )Blen - (long long )j
        >= 0LL) && (found == 0 || found == 1))) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= j && 1 <= l1) && j <= 3) && (-2LL + (long long )Alen) + (long long )Blen
        >= 0LL) && (-2LL + (long long )Alen) + (long long )l1 >= 0LL) && (-2LL + (long
        long )Alen) + (long long )l2 >= 0LL) && (-2LL + (long long )Blen) + (long
        long )l1 >= 0LL) && (-2LL + (long long )Blen) + (long long )found >= 0LL)
        && (-2LL + (long long )l1) + (long long )l2 >= 0LL) && (-2LL + (long long
        )found) + (long long )l2 >= 0LL) && (-1LL + (long long )Alen) + (long long
        )k >= 0LL) && (-1LL + (long long )Alen) + (long long )i >= 0LL) && (-1LL +
        (long long )Alen) + (long long )found >= 0LL) && (-1LL + (long long )Alen)
        + (long long )j >= 0LL) && (-1LL + (long long )Blen) + (long long )i >= 0LL)
        && (-1LL + (long long )k) + (long long )l1 >= 0LL) && (-1LL + (long long )i)
        + (long long )l1 >= 0LL) && (-1LL + (long long )i) + (long long )l2 >= 0LL)
        && (-1LL + (long long )found) + (long long )l1 >= 0LL) && (-1LL + (long long
        )found) + (long long )j >= 0LL) && (-1LL + (long long )j) + (long long )l1
        >= 0LL) && (-1LL - (long long )k) + (long long )l2 >= 0LL) && (-1LL - (long
        long )i) + (long long )l2 >= 0LL) && (0LL - (long long )i) + (long long )k
        >= 0LL) && (0LL - (long long )i) + (long long )j >= 0LL) && (0LL - (long long
        )found) + (long long )l1 >= 0LL) && (0LL - (long long )found) + (long long
        )l2 >= 0LL) && (0LL - (long long )j) + (long long )l2 >= 0LL) && (1LL - (long
        long )found) + (long long )k >= 0LL) && (1LL - (long long )found) + (long
        long )i >= 0LL) && (1LL - (long long )found) + (long long )j >= 0LL) && (2LL
        - (long long )j) + (long long )l1 >= 0LL) && (3LL - (long long )j) + (long
        long )k >= 0LL) && (536870909LL - (long long )Blen) + (long long )l1 >= 0LL)
        && (536870910LL - (long long )Alen) + (long long )i >= 0LL) && (536870910LL
        - (long long )Blen) + (long long )i >= 0LL) && (long long )i + (long long
        )k >= 0LL) && (long long )i + (long long )j >= 0LL) && (long long )found +
        (long long )i >= 0LL) && (-1LL + (long long )Blen) - (long long )k >= 0LL)
        && (-1LL + (long long )Blen) - (long long )i >= 0LL) && (2LL + (long long
        )Alen) - (long long )j >= 0LL) && (3LL + (long long )i) - (long long )j >=
        0LL) && (3LL + (long long )found) - (long long )j >= 0LL) && (536870909LL
        + (long long )Alen) - (long long )Blen >= 0LL) && (536870909LL + (long long
        )Alen) - (long long )l2 >= 0LL) && (536870909LL + (long long )l1) - (long
        long )l2 >= 0LL) && (536870910LL + (long long )i) - (long long )l1 >= 0LL)
        && (536870910LL + (long long )i) - (long long )l2 >= 0LL) && (0LL - (long
        long )i) - (long long )k >= 0LL) && (1LL - (long long )found) - (long long
        )k >= 0LL) && (1LL - (long long )found) - (long long )i >= 0LL) && (3LL -
        (long long )i) - (long long )j >= 0LL) && (3LL - (long long )found) - (long
        long )j >= 0LL) && (3LL - (long long )j) - (long long )k >= 0LL) && (536870910LL
        - (long long )Alen) - (long long )k >= 0LL) && (536870910LL - (long long )Alen)
        - (long long )i >= 0LL) && (536870910LL - (long long )Blen) - (long long )k
        >= 0LL) && (536870910LL - (long long )Blen) - (long long )i >= 0LL) && (536870910LL
        - (long long )k) - (long long )l1 >= 0LL) && (536870910LL - (long long )k)
        - (long long )l2 >= 0LL) && (536870910LL - (long long )i) - (long long )l1
        >= 0LL) && (536870910LL - (long long )i) - (long long )l2 >= 0LL) && (536870911LL
        - (long long )Alen) - (long long )found >= 0LL) && (536870911LL - (long long
        )Blen) - (long long )found >= 0LL) && (536870911LL - (long long )found) -
        (long long )l1 >= 0LL) && (536870911LL - (long long )found) - (long long )l2
        >= 0LL) && (536870913LL - (long long )Alen) - (long long )j >= 0LL) && (536870913LL
        - (long long )Blen) - (long long )j >= 0LL) && (536870913LL - (long long )j)
        - (long long )l1 >= 0LL) && (536870913LL - (long long )j) - (long long )l2
        >= 0LL) && (long long )Alen - (long long )found >= 0LL) && (long long )Blen
        - (long long )found >= 0LL) && (long long )Blen - (long long )j >= 0LL) &&
        (long long )found - (long long )k >= 0LL) && (long long )found - (long long
        )i >= 0LL) && (long long )j - (long long )k >= 0LL) && 0 == k) && 0 == i)
        && k == 0) && k == i) && i == 0) && (found == 0 || found == 1))) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= k && 0 <= j) && 3 <= l1) && k <= 2) && j <= 2) && (-6LL + (long long )Alen)
        + (long long )l1 >= 0LL) && (-5LL + (long long )Alen) + (long long )i >= 0LL)
        && (-5LL + (long long )i) + (long long )l1 >= 0LL) && (-4LL + (long long )Alen)
        + (long long )Blen >= 0LL) && (-4LL + (long long )Alen) + (long long )l2 >=
        0LL) && (-4LL + (long long )Blen) + (long long )l1 >= 0LL) && (-4LL + (long
        long )l1) + (long long )l2 >= 0LL) && (-3LL + (long long )Alen) + (long long
        )k >= 0LL) && (-3LL + (long long )Alen) + (long long )found >= 0LL) && (-3LL
        + (long long )Alen) + (long long )j >= 0LL) && (-3LL + (long long )Blen) +
        (long long )i >= 0LL) && (-3LL + (long long )k) + (long long )l1 >= 0LL) &&
        (-3LL + (long long )i) + (long long )l2 >= 0LL) && (-3LL + (long long )found)
        + (long long )l1 >= 0LL) && (-3LL + (long long )j) + (long long )l1 >= 0LL)
        && (-2LL + (long long )Blen) + (long long )found >= 0LL) && (-2LL + (long
        long )i) + (long long )k >= 0LL) && (-2LL + (long long )i) + (long long )j
        >= 0LL) && (-2LL + (long long )found) + (long long )i >= 0LL) && (-2LL + (long
        long )found) + (long long )l2 >= 0LL) && (-1LL + (long long )found) + (long
        long )j >= 0LL) && (-2LL - (long long )found) + (long long )l1 >= 0LL) &&
        (-1LL - (long long )found) + (long long )i >= 0LL) && (-1LL - (long long )j)
        + (long long )l1 >= 0LL) && (0LL - (long long )found) + (long long )l2 >=
        0LL) && (0LL - (long long )j) + (long long )l2 >= 0LL) && (1LL - (long long
        )k) + (long long )l2 >= 0LL) && (1LL - (long long )i) + (long long )l2 >=
        0LL) && (1LL - (long long )found) + (long long )k >= 0LL) && (1LL - (long
        long )found) + (long long )j >= 0LL) && (2LL - (long long )i) + (long long
        )k >= 0LL) && (2LL - (long long )i) + (long long )j >= 0LL) && (2LL - (long
        long )j) + (long long )k >= 0LL) && (536870907LL - (long long )Blen) + (long
        long )l1 >= 0LL) && (536870908LL - (long long )Alen) + (long long )i >= 0LL)
        && (536870908LL - (long long )Blen) + (long long )i >= 0LL) && (-2LL + (long
        long )Alen) - (long long )found >= 0LL) && (-1LL + (long long )Alen) - (long
        long )j >= 0LL) && (1LL + (long long )Blen) - (long long )k >= 0LL) && (1LL
        + (long long )Blen) - (long long )i >= 0LL) && (2LL + (long long )found) -
        (long long )k >= 0LL) && (2LL + (long long )found) - (long long )i >= 0LL)
        && (2LL + (long long )found) - (long long )j >= 0LL) && (2LL + (long long
        )j) - (long long )k >= 0LL) && (536870907LL + (long long )Alen) - (long long
        )Blen >= 0LL) && (536870907LL + (long long )Alen) - (long long )l2 >= 0LL)
        && (536870907LL + (long long )l1) - (long long )l2 >= 0LL) && (536870908LL
        + (long long )i) - (long long )l1 >= 0LL) && (536870908LL + (long long )i)
        - (long long )l2 >= 0LL) && (2LL - (long long )found) - (long long )j >= 0LL)
        && (3LL - (long long )found) - (long long )k >= 0LL) && (3LL - (long long
        )found) - (long long )i >= 0LL) && (4LL - (long long )i) - (long long )k >=
        0LL) && (4LL - (long long )i) - (long long )j >= 0LL) && (4LL - (long long
        )j) - (long long )k >= 0LL) && (536870911LL - (long long )Alen) - (long long
        )found >= 0LL) && (536870911LL - (long long )Blen) - (long long )found >=
        0LL) && (536870911LL - (long long )found) - (long long )l1 >= 0LL) && (536870911LL
        - (long long )found) - (long long )l2 >= 0LL) && (536870912LL - (long long
        )Alen) - (long long )k >= 0LL) && (536870912LL - (long long )Alen) - (long
        long )i >= 0LL) && (536870912LL - (long long )Alen) - (long long )j >= 0LL)
        && (536870912LL - (long long )Blen) - (long long )k >= 0LL) && (536870912LL
        - (long long )Blen) - (long long )i >= 0LL) && (536870912LL - (long long )Blen)
        - (long long )j >= 0LL) && (536870912LL - (long long )k) - (long long )l1
        >= 0LL) && (536870912LL - (long long )k) - (long long )l2 >= 0LL) && (536870912LL
        - (long long )i) - (long long )l1 >= 0LL) && (536870912LL - (long long )i)
        - (long long )l2 >= 0LL) && (536870912LL - (long long )j) - (long long )l1
        >= 0LL) && (536870912LL - (long long )j) - (long long )l2 >= 0LL) && (long
        long )Blen - (long long )found >= 0LL) && (long long )Blen - (long long )j
        >= 0LL) && (long long )i - (long long )j >= 0LL) && i == 2) && (found == 0
        || found == 1))) || (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= k && 4 <= i) && 5 <= l1) && i <= 536870909) && (-10LL + (long long )Alen)
        + (long long )l1 >= 0LL) && (-9LL + (long long )Alen) + (long long )i >= 0LL)
        && (-9LL + (long long )i) + (long long )l1 >= 0LL) && (-6LL + (long long )Alen)
        + (long long )Blen >= 0LL) && (-6LL + (long long )Alen) + (long long )l2 >=
        0LL) && (-6LL + (long long )Blen) + (long long )l1 >= 0LL) && (-6LL + (long
        long )l1) + (long long )l2 >= 0LL) && (-5LL + (long long )Alen) + (long long
        )k >= 0LL) && (-5LL + (long long )Alen) + (long long )found >= 0LL) && (-5LL
        + (long long )Alen) + (long long )j >= 0LL) && (-5LL + (long long )Blen) +
        (long long )i >= 0LL) && (-5LL + (long long )k) + (long long )l1 >= 0LL) &&
        (-5LL + (long long )i) + (long long )l2 >= 0LL) && (-5LL + (long long )found)
        + (long long )l1 >= 0LL) && (-5LL + (long long )j) + (long long )l1 >= 0LL)
        && (-4LL + (long long )i) + (long long )k >= 0LL) && (-4LL + (long long )i)
        + (long long )j >= 0LL) && (-4LL + (long long )found) + (long long )i >= 0LL)
        && (-1LL + (long long )Blen) + (long long )found >= 0LL) && (-1LL + (long
        long )found) + (long long )l2 >= 0LL) && (-1LL + (long long )found) + (long
        long )j >= 0LL) && (-4LL - (long long )found) + (long long )l1 >= 0LL) &&
        (-4LL - (long long )j) + (long long )l1 >= 0LL) && (-3LL - (long long )found)
        + (long long )i >= 0LL) && (0LL - (long long )found) + (long long )l2 >= 0LL)
        && (0LL - (long long )j) + (long long )l2 >= 0LL) && (1LL - (long long )found)
        + (long long )k >= 0LL) && (1LL - (long long )found) + (long long )j >= 0LL)
        && (1LL - (long long )j) + (long long )k >= 0LL) && (536870905LL - (long long
        )Blen) + (long long )l1 >= 0LL) && (536870906LL - (long long )Alen) + (long
        long )i >= 0LL) && (536870906LL - (long long )Blen) + (long long )i >= 0LL)
        && (536870908LL - (long long )k) + (long long )l2 >= 0LL) && (536870908LL
        - (long long )i) + (long long )l2 >= 0LL) && (536870909LL - (long long )i)
        + (long long )k >= 0LL) && (536870909LL - (long long )i) + (long long )j >=
        0LL) && (-4LL + (long long )Alen) - (long long )found >= 0LL) && (-4LL + (long
        long )Alen) - (long long )j >= 0LL) && (-3LL + (long long )i) - (long long
        )j >= 0LL) && (1LL + (long long )found) - (long long )j >= 0LL) && (536870905LL
        + (long long )Alen) - (long long )Blen >= 0LL) && (536870905LL + (long long
        )Alen) - (long long )l2 >= 0LL) && (536870905LL + (long long )l1) - (long
        long )l2 >= 0LL) && (536870906LL + (long long )i) - (long long )l1 >= 0LL)
        && (536870906LL + (long long )i) - (long long )l2 >= 0LL) && (536870908LL
        + (long long )Blen) - (long long )k >= 0LL) && (536870908LL + (long long )Blen)
        - (long long )i >= 0LL) && (536870909LL + (long long )found) - (long long
        )k >= 0LL) && (536870909LL + (long long )found) - (long long )i >= 0LL) &&
        (536870909LL + (long long )j) - (long long )k >= 0LL) && (1LL - (long long
        )found) - (long long )j >= 0LL) && (536870910LL - (long long )i) - (long long
        )j >= 0LL) && (536870910LL - (long long )found) - (long long )k >= 0LL) &&
        (536870910LL - (long long )found) - (long long )i >= 0LL) && (536870910LL
        - (long long )j) - (long long )k >= 0LL) && (536870911LL - (long long )Alen)
        - (long long )found >= 0LL) && (536870911LL - (long long )Alen) - (long long
        )j >= 0LL) && (536870911LL - (long long )Blen) - (long long )found >= 0LL)
        && (536870911LL - (long long )Blen) - (long long )j >= 0LL) && (536870911LL
        - (long long )found) - (long long )l1 >= 0LL) && (536870911LL - (long long
        )found) - (long long )l2 >= 0LL) && (536870911LL - (long long )j) - (long
        long )l1 >= 0LL) && (536870911LL - (long long )j) - (long long )l2 >= 0LL)
        && (1073741818LL - (long long )i) - (long long )k >= 0LL) && (1073741819LL
        - (long long )Alen) - (long long )k >= 0LL) && (1073741819LL - (long long
        )Alen) - (long long )i >= 0LL) && (1073741819LL - (long long )Blen) - (long
        long )k >= 0LL) && (1073741819LL - (long long )Blen) - (long long )i >= 0LL)
        && (1073741819LL - (long long )k) - (long long )l1 >= 0LL) && (1073741819LL
        - (long long )k) - (long long )l2 >= 0LL) && (1073741819LL - (long long )i)
        - (long long )l1 >= 0LL) && (1073741819LL - (long long )i) - (long long )l2
        >= 0LL) && (long long )Blen - (long long )found >= 0LL) && (long long )Blen
        - (long long )j >= 0LL) && (found == 0 || found == 1)) && (j == 0 || j ==
        1))) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= j && 1 <= l1) && j <= 2) && (-2LL + (long long )Alen) + (long long )Blen
        >= 0LL) && (-2LL + (long long )Alen) + (long long )l1 >= 0LL) && (-2LL + (long
        long )Alen) + (long long )l2 >= 0LL) && (-2LL + (long long )Blen) + (long
        long )l1 >= 0LL) && (-2LL + (long long )Blen) + (long long )found >= 0LL)
        && (-2LL + (long long )l1) + (long long )l2 >= 0LL) && (-2LL + (long long
        )found) + (long long )l2 >= 0LL) && (-1LL + (long long )Alen) + (long long
        )k >= 0LL) && (-1LL + (long long )Alen) + (long long )i >= 0LL) && (-1LL +
        (long long )Alen) + (long long )found >= 0LL) && (-1LL + (long long )Alen)
        + (long long )j >= 0LL) && (-1LL + (long long )Blen) + (long long )i >= 0LL)
        && (-1LL + (long long )k) + (long long )l1 >= 0LL) && (-1LL + (long long )i)
        + (long long )l1 >= 0LL) && (-1LL + (long long )i) + (long long )l2 >= 0LL)
        && (-1LL + (long long )found) + (long long )l1 >= 0LL) && (-1LL + (long long
        )found) + (long long )j >= 0LL) && (-1LL + (long long )j) + (long long )l1
        >= 0LL) && (-1LL - (long long )k) + (long long )l2 >= 0LL) && (-1LL - (long
        long )i) + (long long )l2 >= 0LL) && (0LL - (long long )i) + (long long )k
        >= 0LL) && (0LL - (long long )i) + (long long )j >= 0LL) && (0LL - (long long
        )found) + (long long )l1 >= 0LL) && (0LL - (long long )found) + (long long
        )l2 >= 0LL) && (0LL - (long long )j) + (long long )l2 >= 0LL) && (1LL - (long
        long )found) + (long long )k >= 0LL) && (1LL - (long long )found) + (long
        long )i >= 0LL) && (1LL - (long long )found) + (long long )j >= 0LL) && (1LL
        - (long long )j) + (long long )l1 >= 0LL) && (2LL - (long long )j) + (long
        long )k >= 0LL) && (536870909LL - (long long )Blen) + (long long )l1 >= 0LL)
        && (536870910LL - (long long )Alen) + (long long )i >= 0LL) && (536870910LL
        - (long long )Blen) + (long long )i >= 0LL) && (long long )i + (long long
        )k >= 0LL) && (long long )i + (long long )j >= 0LL) && (long long )found +
        (long long )i >= 0LL) && (-1LL + (long long )Blen) - (long long )k >= 0LL)
        && (-1LL + (long long )Blen) - (long long )i >= 0LL) && (1LL + (long long
        )Alen) - (long long )j >= 0LL) && (2LL + (long long )i) - (long long )j >=
        0LL) && (2LL + (long long )found) - (long long )j >= 0LL) && (536870909LL
        + (long long )Alen) - (long long )Blen >= 0LL) && (536870909LL + (long long
        )Alen) - (long long )l2 >= 0LL) && (536870909LL + (long long )l1) - (long
        long )l2 >= 0LL) && (536870910LL + (long long )i) - (long long )l1 >= 0LL)
        && (536870910LL + (long long )i) - (long long )l2 >= 0LL) && (0LL - (long
        long )i) - (long long )k >= 0LL) && (1LL - (long long )found) - (long long
        )k >= 0LL) && (1LL - (long long )found) - (long long )i >= 0LL) && (2LL -
        (long long )i) - (long long )j >= 0LL) && (2LL - (long long )found) - (long
        long )j >= 0LL) && (2LL - (long long )j) - (long long )k >= 0LL) && (536870910LL
        - (long long )Alen) - (long long )k >= 0LL) && (536870910LL - (long long )Alen)
        - (long long )i >= 0LL) && (536870910LL - (long long )Blen) - (long long )k
        >= 0LL) && (536870910LL - (long long )Blen) - (long long )i >= 0LL) && (536870910LL
        - (long long )k) - (long long )l1 >= 0LL) && (536870910LL - (long long )k)
        - (long long )l2 >= 0LL) && (536870910LL - (long long )i) - (long long )l1
        >= 0LL) && (536870910LL - (long long )i) - (long long )l2 >= 0LL) && (536870911LL
        - (long long )Alen) - (long long )found >= 0LL) && (536870911LL - (long long
        )Blen) - (long long )found >= 0LL) && (536870911LL - (long long )found) -
        (long long )l1 >= 0LL) && (536870911LL - (long long )found) - (long long )l2
        >= 0LL) && (536870912LL - (long long )Alen) - (long long )j >= 0LL) && (536870912LL
        - (long long )Blen) - (long long )j >= 0LL) && (536870912LL - (long long )j)
        - (long long )l1 >= 0LL) && (536870912LL - (long long )j) - (long long )l2
        >= 0LL) && (long long )Alen - (long long )found >= 0LL) && (long long )Blen
        - (long long )found >= 0LL) && (long long )Blen - (long long )j >= 0LL) &&
        (long long )found - (long long )k >= 0LL) && (long long )found - (long long
        )i >= 0LL) && (long long )j - (long long )k >= 0LL) && 0 == k) && 0 == i)
        && k == 0) && k == i) && i == 0) && (found == 0 || found == 1))) || (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= k && 3 <= l1) && k <= 2) && (-6LL + (long long )Alen) + (long long )l1
        >= 0LL) && (-5LL + (long long )Alen) + (long long )i >= 0LL) && (-5LL + (long
        long )i) + (long long )l1 >= 0LL) && (-4LL + (long long )Alen) + (long long
        )Blen >= 0LL) && (-4LL + (long long )Alen) + (long long )l2 >= 0LL) && (-4LL
        + (long long )Blen) + (long long )l1 >= 0LL) && (-4LL + (long long )l1) +
        (long long )l2 >= 0LL) && (-3LL + (long long )Alen) + (long long )k >= 0LL)
        && (-3LL + (long long )Alen) + (long long )found >= 0LL) && (-3LL + (long
        long )Alen) + (long long )j >= 0LL) && (-3LL + (long long )Blen) + (long long
        )i >= 0LL) && (-3LL + (long long )k) + (long long )l1 >= 0LL) && (-3LL + (long
        long )i) + (long long )l2 >= 0LL) && (-3LL + (long long )found) + (long long
        )l1 >= 0LL) && (-3LL + (long long )j) + (long long )l1 >= 0LL) && (-2LL +
        (long long )i) + (long long )k >= 0LL) && (-2LL + (long long )i) + (long long
        )j >= 0LL) && (-2LL + (long long )found) + (long long )i >= 0LL) && (-1LL
        + (long long )Blen) + (long long )found >= 0LL) && (-1LL + (long long )found)
        + (long long )l2 >= 0LL) && (-1LL + (long long )found) + (long long )j >=
        0LL) && (-2LL - (long long )found) + (long long )l1 >= 0LL) && (-2LL - (long
        long )j) + (long long )l1 >= 0LL) && (-1LL - (long long )found) + (long long
        )i >= 0LL) && (0LL - (long long )found) + (long long )l2 >= 0LL) && (0LL -
        (long long )j) + (long long )l2 >= 0LL) && (1LL - (long long )k) + (long long
        )l2 >= 0LL) && (1LL - (long long )i) + (long long )l2 >= 0LL) && (1LL - (long
        long )found) + (long long )k >= 0LL) && (1LL - (long long )found) + (long
        long )j >= 0LL) && (1LL - (long long )j) + (long long )k >= 0LL) && (2LL -
        (long long )i) + (long long )k >= 0LL) && (2LL - (long long )i) + (long long
        )j >= 0LL) && (536870907LL - (long long )Blen) + (long long )l1 >= 0LL) &&
        (536870908LL - (long long )Alen) + (long long )i >= 0LL) && (536870908LL -
        (long long )Blen) + (long long )i >= 0LL) && (-2LL + (long long )Alen) - (long
        long )found >= 0LL) && (-2LL + (long long )Alen) - (long long )j >= 0LL) &&
        (-1LL + (long long )i) - (long long )j >= 0LL) && (1LL + (long long )Blen)
        - (long long )k >= 0LL) && (1LL + (long long )Blen) - (long long )i >= 0LL)
        && (1LL + (long long )found) - (long long )j >= 0LL) && (2LL + (long long
        )found) - (long long )k >= 0LL) && (2LL + (long long )found) - (long long
        )i >= 0LL) && (2LL + (long long )j) - (long long )k >= 0LL) && (536870907LL
        + (long long )Alen) - (long long )Blen >= 0LL) && (536870907LL + (long long
        )Alen) - (long long )l2 >= 0LL) && (536870907LL + (long long )l1) - (long
        long )l2 >= 0LL) && (536870908LL + (long long )i) - (long long )l1 >= 0LL)
        && (536870908LL + (long long )i) - (long long )l2 >= 0LL) && (1LL - (long
        long )found) - (long long )j >= 0LL) && (3LL - (long long )i) - (long long
        )j >= 0LL) && (3LL - (long long )found) - (long long )k >= 0LL) && (3LL -
        (long long )found) - (long long )i >= 0LL) && (3LL - (long long )j) - (long
        long )k >= 0LL) && (4LL - (long long )i) - (long long )k >= 0LL) && (536870911LL
        - (long long )Alen) - (long long )found >= 0LL) && (536870911LL - (long long
        )Alen) - (long long )j >= 0LL) && (536870911LL - (long long )Blen) - (long
        long )found >= 0LL) && (536870911LL - (long long )Blen) - (long long )j >=
        0LL) && (536870911LL - (long long )found) - (long long )l1 >= 0LL) && (536870911LL
        - (long long )found) - (long long )l2 >= 0LL) && (536870911LL - (long long
        )j) - (long long )l1 >= 0LL) && (536870911LL - (long long )j) - (long long
        )l2 >= 0LL) && (536870912LL - (long long )Alen) - (long long )k >= 0LL) &&
        (536870912LL - (long long )Alen) - (long long )i >= 0LL) && (536870912LL -
        (long long )Blen) - (long long )k >= 0LL) && (536870912LL - (long long )Blen)
        - (long long )i >= 0LL) && (536870912LL - (long long )k) - (long long )l1
        >= 0LL) && (536870912LL - (long long )k) - (long long )l2 >= 0LL) && (536870912LL
        - (long long )i) - (long long )l1 >= 0LL) && (536870912LL - (long long )i)
        - (long long )l2 >= 0LL) && (long long )Blen - (long long )found >= 0LL) &&
        (long long )Blen - (long long )j >= 0LL) && i == 2) && (found == 0 || found
        == 1)) && (j == 0 || j == 1))) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= k && 4 <= i) && 5 <= l1) && i <= 536870909) && (-10LL + (long long )Alen)
        + (long long )l1 >= 0LL) && (-9LL + (long long )Alen) + (long long )i >= 0LL)
        && (-9LL + (long long )i) + (long long )l1 >= 0LL) && (-6LL + (long long )Alen)
        + (long long )Blen >= 0LL) && (-6LL + (long long )Alen) + (long long )l2 >=
        0LL) && (-6LL + (long long )Blen) + (long long )l1 >= 0LL) && (-6LL + (long
        long )l1) + (long long )l2 >= 0LL) && (-5LL + (long long )Alen) + (long long
        )k >= 0LL) && (-5LL + (long long )Alen) + (long long )found >= 0LL) && (-5LL
        + (long long )Alen) + (long long )j >= 0LL) && (-5LL + (long long )Blen) +
        (long long )i >= 0LL) && (-5LL + (long long )k) + (long long )l1 >= 0LL) &&
        (-5LL + (long long )i) + (long long )l2 >= 0LL) && (-5LL + (long long )found)
        + (long long )l1 >= 0LL) && (-5LL + (long long )j) + (long long )l1 >= 0LL)
        && (-4LL + (long long )i) + (long long )k >= 0LL) && (-4LL + (long long )i)
        + (long long )j >= 0LL) && (-4LL + (long long )found) + (long long )i >= 0LL)
        && (-1LL + (long long )Blen) + (long long )found >= 0LL) && (-1LL + (long
        long )found) + (long long )l2 >= 0LL) && (-5LL - (long long )found) + (long
        long )l1 >= 0LL) && (-5LL - (long long )j) + (long long )l1 >= 0LL) && (-4LL
        - (long long )found) + (long long )i >= 0LL) && (-1LL - (long long )found)
        + (long long )l2 >= 0LL) && (-1LL - (long long )j) + (long long )l2 >= 0LL)
        && (0LL - (long long )found) + (long long )k >= 0LL) && (0LL - (long long
        )found) + (long long )j >= 0LL) && (0LL - (long long )j) + (long long )k >=
        0LL) && (536870905LL - (long long )Blen) + (long long )l1 >= 0LL) && (536870906LL
        - (long long )Alen) + (long long )i >= 0LL) && (536870906LL - (long long )Blen)
        + (long long )i >= 0LL) && (536870908LL - (long long )k) + (long long )l2
        >= 0LL) && (536870908LL - (long long )i) + (long long )l2 >= 0LL) && (536870909LL
        - (long long )i) + (long long )k >= 0LL) && (536870909LL - (long long )i)
        + (long long )j >= 0LL) && (long long )found + (long long )j >= 0LL) && (-5LL
        + (long long )Alen) - (long long )found >= 0LL) && (-5LL + (long long )Alen)
        - (long long )j >= 0LL) && (-4LL + (long long )i) - (long long )j >= 0LL)
        && (-1LL + (long long )Blen) - (long long )found >= 0LL) && (-1LL + (long
        long )Blen) - (long long )j >= 0LL) && (536870905LL + (long long )Alen) -
        (long long )Blen >= 0LL) && (536870905LL + (long long )Alen) - (long long
        )l2 >= 0LL) && (536870905LL + (long long )l1) - (long long )l2 >= 0LL) &&
        (536870906LL + (long long )i) - (long long )l1 >= 0LL) && (536870906LL + (long
        long )i) - (long long )l2 >= 0LL) && (536870908LL + (long long )Blen) - (long
        long )k >= 0LL) && (536870908LL + (long long )Blen) - (long long )i >= 0LL)
        && (536870909LL + (long long )found) - (long long )k >= 0LL) && (536870909LL
        + (long long )found) - (long long )i >= 0LL) && (536870909LL + (long long
        )j) - (long long )k >= 0LL) && (0LL - (long long )found) - (long long )j >=
        0LL) && (536870909LL - (long long )i) - (long long )j >= 0LL) && (536870909LL
        - (long long )found) - (long long )k >= 0LL) && (536870909LL - (long long
        )found) - (long long )i >= 0LL) && (536870909LL - (long long )j) - (long long
        )k >= 0LL) && (536870910LL - (long long )Alen) - (long long )found >= 0LL)
        && (536870910LL - (long long )Alen) - (long long )j >= 0LL) && (536870910LL
        - (long long )Blen) - (long long )found >= 0LL) && (536870910LL - (long long
        )Blen) - (long long )j >= 0LL) && (536870910LL - (long long )found) - (long
        long )l1 >= 0LL) && (536870910LL - (long long )found) - (long long )l2 >=
        0LL) && (536870910LL - (long long )j) - (long long )l1 >= 0LL) && (536870910LL
        - (long long )j) - (long long )l2 >= 0LL) && (1073741818LL - (long long )i)
        - (long long )k >= 0LL) && (1073741819LL - (long long )Alen) - (long long
        )k >= 0LL) && (1073741819LL - (long long )Alen) - (long long )i >= 0LL) &&
        (1073741819LL - (long long )Blen) - (long long )k >= 0LL) && (1073741819LL
        - (long long )Blen) - (long long )i >= 0LL) && (1073741819LL - (long long
        )k) - (long long )l1 >= 0LL) && (1073741819LL - (long long )k) - (long long
        )l2 >= 0LL) && (1073741819LL - (long long )i) - (long long )l1 >= 0LL) &&
        (1073741819LL - (long long )i) - (long long )l2 >= 0LL) && (long long )found
        - (long long )j >= 0LL) && 0 == found) && 0 == j) && found == 0) && found
        == j) && j == 0)) || (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((1
        <= l1 && (-2LL + (long long )Alen) + (long long )Blen >= 0LL) && (-2LL + (long
        long )Alen) + (long long )l1 >= 0LL) && (-2LL + (long long )Alen) + (long
        long )l2 >= 0LL) && (-2LL + (long long )Blen) + (long long )l1 >= 0LL) &&
        (-2LL + (long long )l1) + (long long )l2 >= 0LL) && (-1LL + (long long )Alen)
        + (long long )k >= 0LL) && (-1LL + (long long )Alen) + (long long )i >= 0LL)
        && (-1LL + (long long )Alen) + (long long )found >= 0LL) && (-1LL + (long
        long )Alen) + (long long )j >= 0LL) && (-1LL + (long long )Blen) + (long long
        )i >= 0LL) && (-1LL + (long long )Blen) + (long long )found >= 0LL) && (-1LL
        + (long long )k) + (long long )l1 >= 0LL) && (-1LL + (long long )i) + (long
        long )l1 >= 0LL) && (-1LL + (long long )i) + (long long )l2 >= 0LL) && (-1LL
        + (long long )found) + (long long )l1 >= 0LL) && (-1LL + (long long )found)
        + (long long )l2 >= 0LL) && (-1LL + (long long )found) + (long long )j >=
        0LL) && (-1LL + (long long )j) + (long long )l1 >= 0LL) && (-1LL - (long long
        )k) + (long long )l2 >= 0LL) && (-1LL - (long long )i) + (long long )l2 >=
        0LL) && (0LL - (long long )i) + (long long )k >= 0LL) && (0LL - (long long
        )i) + (long long )j >= 0LL) && (0LL - (long long )found) + (long long )l1
        >= 0LL) && (0LL - (long long )found) + (long long )l2 >= 0LL) && (0LL - (long
        long )j) + (long long )l1 >= 0LL) && (0LL - (long long )j) + (long long )l2
        >= 0LL) && (1LL - (long long )found) + (long long )k >= 0LL) && (1LL - (long
        long )found) + (long long )i >= 0LL) && (1LL - (long long )found) + (long
        long )j >= 0LL) && (1LL - (long long )j) + (long long )k >= 0LL) && (536870909LL
        - (long long )Blen) + (long long )l1 >= 0LL) && (536870910LL - (long long
        )Alen) + (long long )i >= 0LL) && (536870910LL - (long long )Blen) + (long
        long )i >= 0LL) && (long long )i + (long long )k >= 0LL) && (long long )i
        + (long long )j >= 0LL) && (long long )found + (long long )i >= 0LL) && (-1LL
        + (long long )Blen) - (long long )k >= 0LL) && (-1LL + (long long )Blen) -
        (long long )i >= 0LL) && (1LL + (long long )i) - (long long )j >= 0LL) &&
        (1LL + (long long )found) - (long long )j >= 0LL) && (536870909LL + (long
        long )Alen) - (long long )Blen >= 0LL) && (536870909LL + (long long )Alen)
        - (long long )l2 >= 0LL) && (536870909LL + (long long )l1) - (long long )l2
        >= 0LL) && (536870910LL + (long long )i) - (long long )l1 >= 0LL) && (536870910LL
        + (long long )i) - (long long )l2 >= 0LL) && (0LL - (long long )i) - (long
        long )k >= 0LL) && (1LL - (long long )i) - (long long )j >= 0LL) && (1LL -
        (long long )found) - (long long )k >= 0LL) && (1LL - (long long )found) -
        (long long )i >= 0LL) && (1LL - (long long )found) - (long long )j >= 0LL)
        && (1LL - (long long )j) - (long long )k >= 0LL) && (536870910LL - (long long
        )Alen) - (long long )k >= 0LL) && (536870910LL - (long long )Alen) - (long
        long )i >= 0LL) && (536870910LL - (long long )Blen) - (long long )k >= 0LL)
        && (536870910LL - (long long )Blen) - (long long )i >= 0LL) && (536870910LL
        - (long long )k) - (long long )l1 >= 0LL) && (536870910LL - (long long )k)
        - (long long )l2 >= 0LL) && (536870910LL - (long long )i) - (long long )l1
        >= 0LL) && (536870910LL - (long long )i) - (long long )l2 >= 0LL) && (536870911LL
        - (long long )Alen) - (long long )found >= 0LL) && (536870911LL - (long long
        )Alen) - (long long )j >= 0LL) && (536870911LL - (long long )Blen) - (long
        long )found >= 0LL) && (536870911LL - (long long )Blen) - (long long )j >=
        0LL) && (536870911LL - (long long )found) - (long long )l1 >= 0LL) && (536870911LL
        - (long long )found) - (long long )l2 >= 0LL) && (536870911LL - (long long
        )j) - (long long )l1 >= 0LL) && (536870911LL - (long long )j) - (long long
        )l2 >= 0LL) && (long long )Alen - (long long )found >= 0LL) && (long long
        )Alen - (long long )j >= 0LL) && (long long )Blen - (long long )found >= 0LL)
        && (long long )Blen - (long long )j >= 0LL) && (long long )found - (long long
        )k >= 0LL) && (long long )found - (long long )i >= 0LL) && (long long )j -
        (long long )k >= 0LL) && 0 == k) && 0 == i) && k == 0) && k == i) && i ==
        0) && (found == 0 || found == 1)) && (j == 0 || j == 1))) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= k && 3 <= l1) && k <= 2) && (-6LL + (long long )Alen) + (long long )l1
        >= 0LL) && (-5LL + (long long )Alen) + (long long )i >= 0LL) && (-5LL + (long
        long )i) + (long long )l1 >= 0LL) && (-4LL + (long long )Alen) + (long long
        )Blen >= 0LL) && (-4LL + (long long )Alen) + (long long )l2 >= 0LL) && (-4LL
        + (long long )Blen) + (long long )l1 >= 0LL) && (-4LL + (long long )l1) +
        (long long )l2 >= 0LL) && (-3LL + (long long )Alen) + (long long )k >= 0LL)
        && (-3LL + (long long )Alen) + (long long )found >= 0LL) && (-3LL + (long
        long )Alen) + (long long )j >= 0LL) && (-3LL + (long long )Blen) + (long long
        )i >= 0LL) && (-3LL + (long long )k) + (long long )l1 >= 0LL) && (-3LL + (long
        long )i) + (long long )l2 >= 0LL) && (-3LL + (long long )found) + (long long
        )l1 >= 0LL) && (-3LL + (long long )j) + (long long )l1 >= 0LL) && (-2LL +
        (long long )i) + (long long )k >= 0LL) && (-2LL + (long long )i) + (long long
        )j >= 0LL) && (-2LL + (long long )found) + (long long )i >= 0LL) && (-1LL
        + (long long )Blen) + (long long )found >= 0LL) && (-1LL + (long long )found)
        + (long long )l2 >= 0LL) && (-3LL - (long long )found) + (long long )l1 >=
        0LL) && (-3LL - (long long )j) + (long long )l1 >= 0LL) && (-2LL - (long long
        )found) + (long long )i >= 0LL) && (-1LL - (long long )found) + (long long
        )l2 >= 0LL) && (-1LL - (long long )j) + (long long )l2 >= 0LL) && (0LL - (long
        long )found) + (long long )k >= 0LL) && (0LL - (long long )found) + (long
        long )j >= 0LL) && (0LL - (long long )j) + (long long )k >= 0LL) && (1LL -
        (long long )k) + (long long )l2 >= 0LL) && (1LL - (long long )i) + (long long
        )l2 >= 0LL) && (2LL - (long long )i) + (long long )k >= 0LL) && (2LL - (long
        long )i) + (long long )j >= 0LL) && (536870907LL - (long long )Blen) + (long
        long )l1 >= 0LL) && (536870908LL - (long long )Alen) + (long long )i >= 0LL)
        && (536870908LL - (long long )Blen) + (long long )i >= 0LL) && (long long
        )found + (long long )j >= 0LL) && (-3LL + (long long )Alen) - (long long )found
        >= 0LL) && (-3LL + (long long )Alen) - (long long )j >= 0LL) && (-2LL + (long
        long )i) - (long long )j >= 0LL) && (-1LL + (long long )Blen) - (long long
        )found >= 0LL) && (-1LL + (long long )Blen) - (long long )j >= 0LL) && (1LL
        + (long long )Blen) - (long long )k >= 0LL) && (1LL + (long long )Blen) -
        (long long )i >= 0LL) && (2LL + (long long )found) - (long long )k >= 0LL)
        && (2LL + (long long )found) - (long long )i >= 0LL) && (2LL + (long long
        )j) - (long long )k >= 0LL) && (536870907LL + (long long )Alen) - (long long
        )Blen >= 0LL) && (536870907LL + (long long )Alen) - (long long )l2 >= 0LL)
        && (536870907LL + (long long )l1) - (long long )l2 >= 0LL) && (536870908LL
        + (long long )i) - (long long )l1 >= 0LL) && (536870908LL + (long long )i)
        - (long long )l2 >= 0LL) && (0LL - (long long )found) - (long long )j >= 0LL)
        && (2LL - (long long )i) - (long long )j >= 0LL) && (2LL - (long long )found)
        - (long long )k >= 0LL) && (2LL - (long long )found) - (long long )i >= 0LL)
        && (2LL - (long long )j) - (long long )k >= 0LL) && (4LL - (long long )i)
        - (long long )k >= 0LL) && (536870910LL - (long long )Alen) - (long long )found
        >= 0LL) && (536870910LL - (long long )Alen) - (long long )j >= 0LL) && (536870910LL
        - (long long )Blen) - (long long )found >= 0LL) && (536870910LL - (long long
        )Blen) - (long long )j >= 0LL) && (536870910LL - (long long )found) - (long
        long )l1 >= 0LL) && (536870910LL - (long long )found) - (long long )l2 >=
        0LL) && (536870910LL - (long long )j) - (long long )l1 >= 0LL) && (536870910LL
        - (long long )j) - (long long )l2 >= 0LL) && (536870912LL - (long long )Alen)
        - (long long )k >= 0LL) && (536870912LL - (long long )Alen) - (long long )i
        >= 0LL) && (536870912LL - (long long )Blen) - (long long )k >= 0LL) && (536870912LL
        - (long long )Blen) - (long long )i >= 0LL) && (536870912LL - (long long )k)
        - (long long )l1 >= 0LL) && (536870912LL - (long long )k) - (long long )l2
        >= 0LL) && (536870912LL - (long long )i) - (long long )l1 >= 0LL) && (536870912LL
        - (long long )i) - (long long )l2 >= 0LL) && (long long )found - (long long
        )j >= 0LL) && 0 == found) && 0 == j) && i == 2) && found == 0) && found ==
        j) && j == 0)) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((1
        <= l1 && (-2LL + (long long )Alen) + (long long )Blen >= 0LL) && (-2LL + (long
        long )Alen) + (long long )l1 >= 0LL) && (-2LL + (long long )Alen) + (long
        long )l2 >= 0LL) && (-2LL + (long long )Blen) + (long long )l1 >= 0LL) &&
        (-2LL + (long long )l1) + (long long )l2 >= 0LL) && (-1LL + (long long )Alen)
        + (long long )k >= 0LL) && (-1LL + (long long )Alen) + (long long )i >= 0LL)
        && (-1LL + (long long )Alen) + (long long )found >= 0LL) && (-1LL + (long
        long )Alen) + (long long )j >= 0LL) && (-1LL + (long long )Blen) + (long long
        )i >= 0LL) && (-1LL + (long long )Blen) + (long long )found >= 0LL) && (-1LL
        + (long long )k) + (long long )l1 >= 0LL) && (-1LL + (long long )i) + (long
        long )l1 >= 0LL) && (-1LL + (long long )i) + (long long )l2 >= 0LL) && (-1LL
        + (long long )found) + (long long )l1 >= 0LL) && (-1LL + (long long )found)
        + (long long )l2 >= 0LL) && (-1LL + (long long )j) + (long long )l1 >= 0LL)
        && (-1LL - (long long )k) + (long long )l2 >= 0LL) && (-1LL - (long long )i)
        + (long long )l2 >= 0LL) && (-1LL - (long long )found) + (long long )l1 >=
        0LL) && (-1LL - (long long )found) + (long long )l2 >= 0LL) && (-1LL - (long
        long )j) + (long long )l1 >= 0LL) && (-1LL - (long long )j) + (long long )l2
        >= 0LL) && (0LL - (long long )i) + (long long )k >= 0LL) && (0LL - (long long
        )i) + (long long )j >= 0LL) && (0LL - (long long )found) + (long long )k >=
        0LL) && (0LL - (long long )found) + (long long )i >= 0LL) && (0LL - (long
        long )found) + (long long )j >= 0LL) && (0LL - (long long )j) + (long long
        )k >= 0LL) && (536870909LL - (long long )Blen) + (long long )l1 >= 0LL) &&
        (536870910LL - (long long )Alen) + (long long )i >= 0LL) && (536870910LL -
        (long long )Blen) + (long long )i >= 0LL) && (long long )i + (long long )k
        >= 0LL) && (long long )i + (long long )j >= 0LL) && (long long )found + (long
        long )i >= 0LL) && (long long )found + (long long )j >= 0LL) && (-1LL + (long
        long )Alen) - (long long )found >= 0LL) && (-1LL + (long long )Alen) - (long
        long )j >= 0LL) && (-1LL + (long long )Blen) - (long long )k >= 0LL) && (-1LL
        + (long long )Blen) - (long long )i >= 0LL) && (-1LL + (long long )Blen) -
        (long long )found >= 0LL) && (-1LL + (long long )Blen) - (long long )j >=
        0LL) && (536870909LL + (long long )Alen) - (long long )Blen >= 0LL) && (536870909LL
        + (long long )Alen) - (long long )l2 >= 0LL) && (536870909LL + (long long
        )l1) - (long long )l2 >= 0LL) && (536870910LL + (long long )i) - (long long
        )l1 >= 0LL) && (536870910LL + (long long )i) - (long long )l2 >= 0LL) && (0LL
        - (long long )i) - (long long )k >= 0LL) && (0LL - (long long )i) - (long
        long )j >= 0LL) && (0LL - (long long )found) - (long long )k >= 0LL) && (0LL
        - (long long )found) - (long long )i >= 0LL) && (0LL - (long long )found)
        - (long long )j >= 0LL) && (0LL - (long long )j) - (long long )k >= 0LL) &&
        (536870910LL - (long long )Alen) - (long long )k >= 0LL) && (536870910LL -
        (long long )Alen) - (long long )i >= 0LL) && (536870910LL - (long long )Alen)
        - (long long )found >= 0LL) && (536870910LL - (long long )Alen) - (long long
        )j >= 0LL) && (536870910LL - (long long )Blen) - (long long )k >= 0LL) &&
        (536870910LL - (long long )Blen) - (long long )i >= 0LL) && (536870910LL -
        (long long )Blen) - (long long )found >= 0LL) && (536870910LL - (long long
        )Blen) - (long long )j >= 0LL) && (536870910LL - (long long )k) - (long long
        )l1 >= 0LL) && (536870910LL - (long long )k) - (long long )l2 >= 0LL) && (536870910LL
        - (long long )i) - (long long )l1 >= 0LL) && (536870910LL - (long long )i)
        - (long long )l2 >= 0LL) && (536870910LL - (long long )found) - (long long
        )l1 >= 0LL) && (536870910LL - (long long )found) - (long long )l2 >= 0LL)
        && (536870910LL - (long long )j) - (long long )l1 >= 0LL) && (536870910LL
        - (long long )j) - (long long )l2 >= 0LL) && (long long )i - (long long )j
        >= 0LL) && (long long )found - (long long )k >= 0LL) && (long long )found
        - (long long )i >= 0LL) && (long long )found - (long long )j >= 0LL) && (long
        long )j - (long long )k >= 0LL) && 0 == k) && 0 == i) && 0 == found) && 0
        == j) && k == 0) && k == i) && k == found) && k == j) && i == 0) && i == found)
        && i == j) && found == 0) && found == j) && j == 0)) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= k && 0 <= j) && 4 <= l1) && k <= 3) && j <= 536870910) && (-8LL + (long
        long )Alen) + (long long )l1 >= 0LL) && (-7LL + (long long )Alen) + (long
        long )i >= 0LL) && (-7LL + (long long )i) + (long long )l1 >= 0LL) && (-5LL
        + (long long )Alen) + (long long )Blen >= 0LL) && (-5LL + (long long )Alen)
        + (long long )l2 >= 0LL) && (-5LL + (long long )Blen) + (long long )l1 >=
        0LL) && (-5LL + (long long )l1) + (long long )l2 >= 0LL) && (-4LL + (long
        long )Alen) + (long long )k >= 0LL) && (-4LL + (long long )Alen) + (long long
        )found >= 0LL) && (-4LL + (long long )Alen) + (long long )j >= 0LL) && (-4LL
        + (long long )Blen) + (long long )i >= 0LL) && (-4LL + (long long )k) + (long
        long )l1 >= 0LL) && (-4LL + (long long )i) + (long long )l2 >= 0LL) && (-4LL
        + (long long )found) + (long long )l1 >= 0LL) && (-4LL + (long long )j) +
        (long long )l1 >= 0LL) && (-3LL + (long long )i) + (long long )k >= 0LL) &&
        (-3LL + (long long )i) + (long long )j >= 0LL) && (-3LL + (long long )found)
        + (long long )i >= 0LL) && (-2LL + (long long )Blen) + (long long )found >=
        0LL) && (-2LL + (long long )found) + (long long )l2 >= 0LL) && (-1LL + (long
        long )found) + (long long )j >= 0LL) && (-3LL - (long long )found) + (long
        long )l1 >= 0LL) && (-2LL - (long long )found) + (long long )i >= 0LL) &&
        (0LL - (long long )found) + (long long )l2 >= 0LL) && (0LL - (long long )j)
        + (long long )l2 >= 0LL) && (1LL - (long long )found) + (long long )k >= 0LL)
        && (1LL - (long long )found) + (long long )j >= 0LL) && (2LL - (long long
        )k) + (long long )l2 >= 0LL) && (2LL - (long long )i) + (long long )l2 >=
        0LL) && (3LL - (long long )i) + (long long )k >= 0LL) && (3LL - (long long
        )i) + (long long )j >= 0LL) && (536870906LL - (long long )Blen) + (long long
        )l1 >= 0LL) && (536870906LL - (long long )j) + (long long )l1 >= 0LL) && (536870907LL
        - (long long )Alen) + (long long )i >= 0LL) && (536870907LL - (long long )Blen)
        + (long long )i >= 0LL) && (536870910LL - (long long )j) + (long long )k >=
        0LL) && (-3LL + (long long )Alen) - (long long )found >= 0LL) && (2LL + (long
        long )Blen) - (long long )k >= 0LL) && (2LL + (long long )Blen) - (long long
        )i >= 0LL) && (3LL + (long long )found) - (long long )k >= 0LL) && (3LL +
        (long long )found) - (long long )i >= 0LL) && (3LL + (long long )j) - (long
        long )k >= 0LL) && (536870906LL + (long long )Alen) - (long long )Blen >=
        0LL) && (536870906LL + (long long )Alen) - (long long )l2 >= 0LL) && (536870906LL
        + (long long )Alen) - (long long )j >= 0LL) && (536870906LL + (long long )l1)
        - (long long )l2 >= 0LL) && (536870907LL + (long long )i) - (long long )l1
        >= 0LL) && (536870907LL + (long long )i) - (long long )l2 >= 0LL) && (536870907LL
        + (long long )i) - (long long )j >= 0LL) && (536870910LL + (long long )found)
        - (long long )j >= 0LL) && (4LL - (long long )found) - (long long )k >= 0LL)
        && (4LL - (long long )found) - (long long )i >= 0LL) && (6LL - (long long
        )i) - (long long )k >= 0LL) && (536870911LL - (long long )Alen) - (long long
        )found >= 0LL) && (536870911LL - (long long )Blen) - (long long )found >=
        0LL) && (536870911LL - (long long )found) - (long long )l1 >= 0LL) && (536870911LL
        - (long long )found) - (long long )l2 >= 0LL) && (536870911LL - (long long
        )found) - (long long )j >= 0LL) && (536870913LL - (long long )Alen) - (long
        long )k >= 0LL) && (536870913LL - (long long )Alen) - (long long )i >= 0LL)
        && (536870913LL - (long long )Blen) - (long long )k >= 0LL) && (536870913LL
        - (long long )Blen) - (long long )i >= 0LL) && (536870913LL - (long long )k)
        - (long long )l1 >= 0LL) && (536870913LL - (long long )k) - (long long )l2
        >= 0LL) && (536870913LL - (long long )i) - (long long )l1 >= 0LL) && (536870913LL
        - (long long )i) - (long long )l2 >= 0LL) && (536870913LL - (long long )i)
        - (long long )j >= 0LL) && (536870913LL - (long long )j) - (long long )k >=
        0LL) && (1073741820LL - (long long )Alen) - (long long )j >= 0LL) && (1073741820LL
        - (long long )Blen) - (long long )j >= 0LL) && (1073741820LL - (long long
        )j) - (long long )l1 >= 0LL) && (1073741820LL - (long long )j) - (long long
        )l2 >= 0LL) && (long long )Blen - (long long )found >= 0LL) && (long long
        )Blen - (long long )j >= 0LL) && i == 3) && (found == 0 || found == 1))) ||
        (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        <= j && 2 <= l1) && j <= 536870910) && (-4LL + (long long )Alen) + (long long
        )l1 >= 0LL) && (-3LL + (long long )Alen) + (long long )Blen >= 0LL) && (-3LL
        + (long long )Alen) + (long long )i >= 0LL) && (-3LL + (long long )Alen) +
        (long long )l2 >= 0LL) && (-3LL + (long long )Blen) + (long long )l1 >= 0LL)
        && (-3LL + (long long )i) + (long long )l1 >= 0LL) && (-3LL + (long long )l1)
        + (long long )l2 >= 0LL) && (-2LL + (long long )Alen) + (long long )k >= 0LL)
        && (-2LL + (long long )Alen) + (long long )found >= 0LL) && (-2LL + (long
        long )Alen) + (long long )j >= 0LL) && (-2LL + (long long )Blen) + (long long
        )i >= 0LL) && (-2LL + (long long )Blen) + (long long )found >= 0LL) && (-2LL
        + (long long )k) + (long long )l1 >= 0LL) && (-2LL + (long long )i) + (long
        long )l2 >= 0LL) && (-2LL + (long long )found) + (long long )l1 >= 0LL) &&
        (-2LL + (long long )found) + (long long )l2 >= 0LL) && (-2LL + (long long
        )j) + (long long )l1 >= 0LL) && (-1LL + (long long )i) + (long long )k >=
        0LL) && (-1LL + (long long )i) + (long long )j >= 0LL) && (-1LL + (long long
        )found) + (long long )i >= 0LL) && (-1LL + (long long )found) + (long long
        )j >= 0LL) && (-1LL - (long long )found) + (long long )l1 >= 0LL) && (0LL
        - (long long )k) + (long long )l2 >= 0LL) && (0LL - (long long )i) + (long
        long )l2 >= 0LL) && (0LL - (long long )found) + (long long )i >= 0LL) && (0LL
        - (long long )found) + (long long )l2 >= 0LL) && (0LL - (long long )j) + (long
        long )l2 >= 0LL) && (1LL - (long long )i) + (long long )k >= 0LL) && (1LL
        - (long long )i) + (long long )j >= 0LL) && (1LL - (long long )found) + (long
        long )k >= 0LL) && (1LL - (long long )found) + (long long )j >= 0LL) && (536870908LL
        - (long long )Blen) + (long long )l1 >= 0LL) && (536870908LL - (long long
        )j) + (long long )l1 >= 0LL) && (536870909LL - (long long )Alen) + (long long
        )i >= 0LL) && (536870909LL - (long long )Blen) + (long long )i >= 0LL) &&
        (536870910LL - (long long )j) + (long long )k >= 0LL) && (-1LL + (long long
        )Alen) - (long long )found >= 0LL) && (1LL + (long long )found) - (long long
        )k >= 0LL) && (1LL + (long long )found) - (long long )i >= 0LL) && (1LL +
        (long long )j) - (long long )k >= 0LL) && (536870908LL + (long long )Alen)
        - (long long )Blen >= 0LL) && (536870908LL + (long long )Alen) - (long long
        )l2 >= 0LL) && (536870908LL + (long long )Alen) - (long long )j >= 0LL) &&
        (536870908LL + (long long )l1) - (long long )l2 >= 0LL) && (536870909LL +
        (long long )i) - (long long )l1 >= 0LL) && (536870909LL + (long long )i) -
        (long long )l2 >= 0LL) && (536870909LL + (long long )i) - (long long )j >=
        0LL) && (536870910LL + (long long )found) - (long long )j >= 0LL) && (2LL
        - (long long )i) - (long long )k >= 0LL) && (2LL - (long long )found) - (long
        long )k >= 0LL) && (2LL - (long long )found) - (long long )i >= 0LL) && (536870911LL
        - (long long )Alen) - (long long )k >= 0LL) && (536870911LL - (long long )Alen)
        - (long long )i >= 0LL) && (536870911LL - (long long )Alen) - (long long )found
        >= 0LL) && (536870911LL - (long long )Blen) - (long long )k >= 0LL) && (536870911LL
        - (long long )Blen) - (long long )i >= 0LL) && (536870911LL - (long long )Blen)
        - (long long )found >= 0LL) && (536870911LL - (long long )k) - (long long
        )l1 >= 0LL) && (536870911LL - (long long )k) - (long long )l2 >= 0LL) && (536870911LL
        - (long long )i) - (long long )l1 >= 0LL) && (536870911LL - (long long )i)
        - (long long )l2 >= 0LL) && (536870911LL - (long long )i) - (long long )j
        >= 0LL) && (536870911LL - (long long )found) - (long long )l1 >= 0LL) && (536870911LL
        - (long long )found) - (long long )l2 >= 0LL) && (536870911LL - (long long
        )found) - (long long )j >= 0LL) && (536870911LL - (long long )j) - (long long
        )k >= 0LL) && (1073741820LL - (long long )Alen) - (long long )j >= 0LL) &&
        (1073741820LL - (long long )Blen) - (long long )j >= 0LL) && (1073741820LL
        - (long long )j) - (long long )l1 >= 0LL) && (1073741820LL - (long long )j)
        - (long long )l2 >= 0LL) && (long long )Blen - (long long )k >= 0LL) && (long
        long )Blen - (long long )i >= 0LL) && (long long )Blen - (long long )found
        >= 0LL) && (long long )Blen - (long long )j >= 0LL) && i == 1) && (k == 0
        || k == 1)) && (found == 0 || found == 1))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 554
        column: 2
        function: main
      value: 1 <= Alen
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 554
        column: 2
        function: main
      value: 1 <= i
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 554
        column: 2
        function: main
      value: Alen <= 536870910
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 554
        column: 2
        function: main
      value: Blen <= 536870910
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 554
        column: 2
        function: main
      value: i <= 536870910
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 554
        column: 2
        function: main
      value: (-2LL + (long long )Alen) + (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 554
        column: 2
        function: main
      value: (0LL - (long long )Alen) + (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 554
        column: 2
        function: main
      value: (536870909LL - (long long )Blen) + (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 554
        column: 2
        function: main
      value: (536870909LL + (long long )Alen) - (long long )Blen >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 554
        column: 2
        function: main
      value: (1073741820LL - (long long )Alen) - (long long )Blen >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 554
        column: 2
        function: main
      value: (1073741820LL - (long long )Alen) - (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 554
        column: 2
        function: main
      value: (1073741820LL - (long long )Blen) - (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 554
        column: 2
        function: main
      value: (long long )Alen - (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety/diff-alloca-2.i
        line: 554
        column: 2
        function: main
      value: ((long long )Blen - (long long )i >= 0LL && ((((((((((((((((((((4 <=
        Blen && 4 <= i) && i <= 536870910) && (-8LL + (long long )Blen) + (long long
        )i >= 0LL) && (-5LL + (long long )Alen) + (long long )Blen >= 0LL) && (-5LL
        + (long long )Alen) + (long long )i >= 0LL) && (-5LL + (long long )Blen) +
        (long long )i >= 0LL) && (-5LL + (long long )i) + (long long )i >= 0LL) &&
        (536870906LL - (long long )Alen) + (long long )Blen >= 0LL) && (536870906LL
        - (long long )Alen) + (long long )i >= 0LL) && (536870906LL - (long long )Blen)
        + (long long )i >= 0LL) && (536870906LL - (long long )i) + (long long )i >=
        0LL) && (536870906LL + (long long )Blen) - (long long )i >= 0LL) && (536870909LL
        + (long long )Alen) - (long long )i >= 0LL) && (536870909LL + (long long )i)
        - (long long )i >= 0LL) && (1073741820LL - (long long )Alen) - (long long
        )i >= 0LL) && (1073741820LL - (long long )Blen) - (long long )i >= 0LL) &&
        (1073741820LL - (long long )i) - (long long )i >= 0LL) || ((((((((((((((((3
        <= Blen && (-6LL + (long long )Blen) + (long long )i >= 0LL) && (-4LL + (long
        long )Alen) + (long long )Blen >= 0LL) && (-4LL + (long long )Alen) + (long
        long )i >= 0LL) && (-4LL + (long long )Blen) + (long long )i >= 0LL) && (-4LL
        + (long long )i) + (long long )i >= 0LL) && (536870907LL - (long long )Alen)
        + (long long )Blen >= 0LL) && (536870907LL - (long long )Alen) + (long long
        )i >= 0LL) && (536870907LL - (long long )Blen) + (long long )i >= 0LL) &&
        (536870907LL - (long long )i) + (long long )i >= 0LL) && (2LL + (long long
        )Alen) - (long long )i >= 0LL) && (2LL + (long long )i) - (long long )i >=
        0LL) && (536870907LL + (long long )Blen) - (long long )i >= 0LL) && (536870913LL
        - (long long )Alen) - (long long )i >= 0LL) && (536870913LL - (long long )Blen)
        - (long long )i >= 0LL) && (536870913LL - (long long )i) - (long long )i >=
        0LL) && i == 3)) || ((((((((((((((((2 <= Blen && (-4LL + (long long )Blen)
        + (long long )i >= 0LL) && (-3LL + (long long )Alen) + (long long )Blen >=
        0LL) && (-3LL + (long long )Alen) + (long long )i >= 0LL) && (-3LL + (long
        long )Blen) + (long long )i >= 0LL) && (-3LL + (long long )i) + (long long
        )i >= 0LL) && (536870908LL - (long long )Alen) + (long long )Blen >= 0LL)
        && (536870908LL - (long long )Alen) + (long long )i >= 0LL) && (536870908LL
        - (long long )Blen) + (long long )i >= 0LL) && (536870908LL - (long long )i)
        + (long long )i >= 0LL) && (1LL + (long long )Alen) - (long long )i >= 0LL)
        && (1LL + (long long )i) - (long long )i >= 0LL) && (536870908LL + (long long
        )Blen) - (long long )i >= 0LL) && (536870912LL - (long long )Alen) - (long
        long )i >= 0LL) && (536870912LL - (long long )Blen) - (long long )i >= 0LL)
        && (536870912LL - (long long )i) - (long long )i >= 0LL) && i == 2)) || ((((((((((((((((1
        <= Blen && (-2LL + (long long )Alen) + (long long )Blen >= 0LL) && (-2LL +
        (long long )Alen) + (long long )i >= 0LL) && (-2LL + (long long )Blen) + (long
        long )i >= 0LL) && (-2LL + (long long )Blen) + (long long )i >= 0LL) && (-2LL
        + (long long )i) + (long long )i >= 0LL) && (536870909LL - (long long )Alen)
        + (long long )Blen >= 0LL) && (536870909LL - (long long )Alen) + (long long
        )i >= 0LL) && (536870909LL - (long long )Blen) + (long long )i >= 0LL) &&
        (536870909LL - (long long )i) + (long long )i >= 0LL) && (536870909LL + (long
        long )Blen) - (long long )i >= 0LL) && (536870911LL - (long long )Alen) -
        (long long )i >= 0LL) && (536870911LL - (long long )Blen) - (long long )i
        >= 0LL) && (536870911LL - (long long )i) - (long long )i >= 0LL) && (long
        long )Alen - (long long )i >= 0LL) && (long long )i - (long long )i >= 0LL)
        && i == 1))) || ((((((((((((((((((1 <= Blen && (-2LL + (long long )Alen) +
        (long long )Blen >= 0LL) && (-2LL + (long long )Blen) + (long long )i >= 0LL)
        && (-1LL + (long long )Alen) + (long long )i >= 0LL) && (-1LL + (long long
        )Blen) + (long long )i >= 0LL) && (-1LL + (long long )i) + (long long )i >=
        0LL) && (536870909LL - (long long )Alen) + (long long )Blen >= 0LL) && (536870910LL
        - (long long )Alen) + (long long )i >= 0LL) && (536870910LL - (long long )Blen)
        + (long long )i >= 0LL) && (536870910LL - (long long )i) + (long long )i >=
        0LL) && (-1LL + (long long )Alen) - (long long )i >= 0LL) && (-1LL + (long
        long )Blen) - (long long )i >= 0LL) && (-1LL + (long long )i) - (long long
        )i >= 0LL) && (536870909LL + (long long )Blen) - (long long )i >= 0LL) &&
        (536870910LL - (long long )Alen) - (long long )i >= 0LL) && (536870910LL -
        (long long )Blen) - (long long )i >= 0LL) && (536870910LL - (long long )i)
        - (long long )i >= 0LL) && 0 == i) && i == 0)
      format: c_expression
