- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 23bf734a-be0e-4d21-807c-d89fcd878e63
    creation_time: 2025-03-22T16:56:01Z
    producer:
      name: Goblint
      version: heads/master-0-g66dff5a90-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp.json'' ''--disable'' ''witness.graphml.enabled''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/termination.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c: 2eb1c51b5dcd2aa3c1ad85113a549918b304cfbd2b0e2e8012a19f3ab96e6b49
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(F end) )
  content:
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 47
        column: 9
        function: main
      value: 1U <= a
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 47
        column: 9
        function: main
      value: 1U <= b
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 47
        column: 9
        function: main
      value: a <= 65535U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 47
        column: 9
        function: main
      value: b <= 65535U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 47
        column: 9
        function: main
      value: (-2LL + (long long )a) + (long long )b >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 47
        column: 9
        function: main
      value: (65534LL - (long long )a) + (long long )b >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 47
        column: 9
        function: main
      value: (65534LL + (long long )a) - (long long )b >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 47
        column: 9
        function: main
      value: (131070LL - (long long )a) - (long long )b >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 47
        column: 9
        function: main
      value: ((((((((((-1LL + (long long )a) + (long long )x >= 0LL && (-1LL + (long
        long )b) + (long long )x >= 0LL) && (65535LL - (long long )a) + (long long
        )x >= 0LL) && (65535LL - (long long )b) + (long long )x >= 0LL) && (4294967294LL
        + (long long )a) - (long long )x >= 0LL) && (4294967294LL + (long long )b)
        - (long long )x >= 0LL) && (4295032830LL - (long long )a) - (long long )x
        >= 0LL) && (4295032830LL - (long long )b) - (long long )x >= 0LL) && (((((((((((4294967295LL
        - (long long )v) + (long long )x >= 0LL && (4294967294LL + (long long )a)
        - (long long )v >= 0LL) && (4294967294LL + (long long )b) - (long long )v
        >= 0LL) && (4295032830LL - (long long )a) - (long long )v >= 0LL) && (4295032830LL
        - (long long )b) - (long long )v >= 0LL) && (8589934590LL - (long long )v)
        - (long long )x >= 0LL) && ((((((((((((((((((((((((((((((((((-1LL + (long
        long )a) + (long long )y >= 0LL && (-1LL + (long long )a) + (long long )u
        >= 0LL) && (-1LL + (long long )b) + (long long )y >= 0LL) && (-1LL + (long
        long )b) + (long long )u >= 0LL) && (65535LL - (long long )a) + (long long
        )y >= 0LL) && (65535LL - (long long )a) + (long long )u >= 0LL) && (65535LL
        - (long long )b) + (long long )y >= 0LL) && (65535LL - (long long )b) + (long
        long )u >= 0LL) && (4294967295LL - (long long )x) + (long long )y >= 0LL)
        && (4294967295LL - (long long )u) + (long long )x >= 0LL) && (4294967295LL
        - (long long )u) + (long long )y >= 0LL) && (4294967295LL - (long long )v)
        + (long long )y >= 0LL) && (long long )x + (long long )y >= 0LL) && (long
        long )u + (long long )x >= 0LL) && (long long )u + (long long )y >= 0LL) &&
        (4294967294LL + (long long )a) - (long long )y >= 0LL) && (4294967294LL +
        (long long )a) - (long long )u >= 0LL) && (4294967294LL + (long long )b) -
        (long long )y >= 0LL) && (4294967294LL + (long long )b) - (long long )u >=
        0LL) && (4294967295LL + (long long )x) - (long long )y >= 0LL) && (4294967295LL
        + (long long )u) - (long long )x >= 0LL) && (4294967295LL + (long long )u)
        - (long long )y >= 0LL) && (4294967295LL + (long long )u) - (long long )v
        >= 0LL) && (4295032830LL - (long long )a) - (long long )y >= 0LL) && (4295032830LL
        - (long long )a) - (long long )u >= 0LL) && (4295032830LL - (long long )b)
        - (long long )y >= 0LL) && (4295032830LL - (long long )b) - (long long )u
        >= 0LL) && (8589934590LL - (long long )x) - (long long )y >= 0LL) && (8589934590LL
        - (long long )u) - (long long )x >= 0LL) && (8589934590LL - (long long )u)
        - (long long )y >= 0LL) && (8589934590LL - (long long )u) - (long long )v
        >= 0LL) && (8589934590LL - (long long )v) - (long long )y >= 0LL) || ((((((((((((((((((((((((((((((((((((((((((((((((1U
        <= y && 1U <= u) && y <= 65535U) && u <= 65535U) && (-2LL + (long long )a)
        + (long long )y >= 0LL) && (-2LL + (long long )a) + (long long )u >= 0LL)
        && (-2LL + (long long )b) + (long long )y >= 0LL) && (-2LL + (long long )b)
        + (long long )u >= 0LL) && (-2LL + (long long )u) + (long long )y >= 0LL)
        && (-1LL + (long long )a) + (long long )v >= 0LL) && (-1LL + (long long )b)
        + (long long )v >= 0LL) && (-1LL + (long long )x) + (long long )y >= 0LL)
        && (-1LL + (long long )u) + (long long )x >= 0LL) && (-1LL + (long long )u)
        + (long long )v >= 0LL) && (-1LL + (long long )v) + (long long )y >= 0LL)
        && (0LL - (long long )b) + (long long )y >= 0LL) && (0LL - (long long )b)
        + (long long )u >= 0LL) && (0LL - (long long )u) + (long long )y >= 0LL) &&
        (65534LL - (long long )a) + (long long )y >= 0LL) && (65534LL - (long long
        )a) + (long long )u >= 0LL) && (65535LL - (long long )a) + (long long )v >=
        0LL) && (65535LL - (long long )b) + (long long )v >= 0LL) && (65535LL - (long
        long )u) + (long long )x >= 0LL) && (65535LL - (long long )u) + (long long
        )v >= 0LL) && (4294967294LL - (long long )x) + (long long )y >= 0LL) && (4294967294LL
        - (long long )v) + (long long )y >= 0LL) && (long long )v + (long long )x
        >= 0LL) && (65534LL + (long long )a) - (long long )y >= 0LL) && (65534LL +
        (long long )a) - (long long )u >= 0LL) && (65535LL + (long long )x) - (long
        long )y >= 0LL) && (65535LL + (long long )v) - (long long )y >= 0LL) && (4294967294LL
        + (long long )u) - (long long )x >= 0LL) && (4294967294LL + (long long )u)
        - (long long )v >= 0LL) && (4294967295LL + (long long )v) - (long long )x
        >= 0LL) && (131070LL - (long long )a) - (long long )y >= 0LL) && (131070LL
        - (long long )a) - (long long )u >= 0LL) && (131070LL - (long long )b) - (long
        long )y >= 0LL) && (131070LL - (long long )b) - (long long )u >= 0LL) && (131070LL
        - (long long )u) - (long long )y >= 0LL) && (4295032830LL - (long long )x)
        - (long long )y >= 0LL) && (4295032830LL - (long long )u) - (long long )x
        >= 0LL) && (4295032830LL - (long long )u) - (long long )v >= 0LL) && (4295032830LL
        - (long long )v) - (long long )y >= 0LL) && (long long )b - (long long )y
        >= 0LL) && (long long )b - (long long )u >= 0LL) && (long long )u - (long
        long )y >= 0LL) && b == y) && b == u) && y == u)) || ((((((((((((((((((((((((((((((((((((((((((-1LL
        + (long long )a) + (long long )y >= 0LL && (-1LL + (long long )a) + (long
        long )u >= 0LL) && (-1LL + (long long )a) + (long long )v >= 0LL) && (-1LL
        + (long long )b) + (long long )y >= 0LL) && (-1LL + (long long )b) + (long
        long )u >= 0LL) && (-1LL + (long long )b) + (long long )v >= 0LL) && (65535LL
        - (long long )a) + (long long )y >= 0LL) && (65535LL - (long long )a) + (long
        long )u >= 0LL) && (65535LL - (long long )a) + (long long )v >= 0LL) && (65535LL
        - (long long )b) + (long long )y >= 0LL) && (65535LL - (long long )b) + (long
        long )u >= 0LL) && (65535LL - (long long )b) + (long long )v >= 0LL) && (4294967295LL
        - (long long )x) + (long long )y >= 0LL) && (4294967295LL - (long long )u)
        + (long long )x >= 0LL) && (4294967295LL - (long long )u) + (long long )y
        >= 0LL) && (4294967295LL - (long long )u) + (long long )v >= 0LL) && (4294967295LL
        - (long long )v) + (long long )y >= 0LL) && (long long )x + (long long )y
        >= 0LL) && (long long )u + (long long )x >= 0LL) && (long long )u + (long
        long )y >= 0LL) && (long long )u + (long long )v >= 0LL) && (long long )v
        + (long long )x >= 0LL) && (long long )v + (long long )y >= 0LL) && (4294967294LL
        + (long long )a) - (long long )y >= 0LL) && (4294967294LL + (long long )a)
        - (long long )u >= 0LL) && (4294967294LL + (long long )b) - (long long )y
        >= 0LL) && (4294967294LL + (long long )b) - (long long )u >= 0LL) && (4294967295LL
        + (long long )x) - (long long )y >= 0LL) && (4294967295LL + (long long )u)
        - (long long )x >= 0LL) && (4294967295LL + (long long )u) - (long long )y
        >= 0LL) && (4294967295LL + (long long )u) - (long long )v >= 0LL) && (4294967295LL
        + (long long )v) - (long long )x >= 0LL) && (4294967295LL + (long long )v)
        - (long long )y >= 0LL) && (4295032830LL - (long long )a) - (long long )y
        >= 0LL) && (4295032830LL - (long long )a) - (long long )u >= 0LL) && (4295032830LL
        - (long long )b) - (long long )y >= 0LL) && (4295032830LL - (long long )b)
        - (long long )u >= 0LL) && (8589934590LL - (long long )x) - (long long )y
        >= 0LL) && (8589934590LL - (long long )u) - (long long )x >= 0LL) && (8589934590LL
        - (long long )u) - (long long )y >= 0LL) && (8589934590LL - (long long )u)
        - (long long )v >= 0LL) && (8589934590LL - (long long )v) - (long long )y
        >= 0LL))) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((1U <=
        y && 1U <= u) && 3U <= v) && y <= 65535U) && u <= 65535U) && v <= 196605U)
        && (-4LL + (long long )a) + (long long )v >= 0LL) && (-4LL + (long long )b)
        + (long long )v >= 0LL) && (-4LL + (long long )u) + (long long )v >= 0LL)
        && (-4LL + (long long )v) + (long long )y >= 0LL) && (-3LL + (long long )v)
        + (long long )x >= 0LL) && (-2LL + (long long )a) + (long long )y >= 0LL)
        && (-2LL + (long long )a) + (long long )u >= 0LL) && (-2LL + (long long )b)
        + (long long )y >= 0LL) && (-2LL + (long long )b) + (long long )u >= 0LL)
        && (-2LL + (long long )u) + (long long )y >= 0LL) && (-1LL + (long long )x)
        + (long long )y >= 0LL) && (-1LL + (long long )u) + (long long )x >= 0LL)
        && (-2LL - (long long )b) + (long long )v >= 0LL) && (-2LL - (long long )u)
        + (long long )v >= 0LL) && (0LL - (long long )b) + (long long )y >= 0LL) &&
        (0LL - (long long )b) + (long long )u >= 0LL) && (0LL - (long long )u) + (long
        long )y >= 0LL) && (65532LL - (long long )a) + (long long )v >= 0LL) && (65534LL
        - (long long )a) + (long long )y >= 0LL) && (65534LL - (long long )a) + (long
        long )u >= 0LL) && (65535LL - (long long )u) + (long long )x >= 0LL) && (131070LL
        - (long long )v) + (long long )y >= 0LL) && (196605LL - (long long )v) + (long
        long )x >= 0LL) && (4294967294LL - (long long )x) + (long long )y >= 0LL)
        && (-2LL + (long long )v) - (long long )y >= 0LL) && (65534LL + (long long
        )a) - (long long )y >= 0LL) && (65534LL + (long long )a) - (long long )u >=
        0LL) && (65535LL + (long long )x) - (long long )y >= 0LL) && (131070LL + (long
        long )b) - (long long )v >= 0LL) && (131070LL + (long long )u) - (long long
        )v >= 0LL) && (196604LL + (long long )a) - (long long )v >= 0LL) && (4294967292LL
        + (long long )v) - (long long )x >= 0LL) && (4294967294LL + (long long )u)
        - (long long )x >= 0LL) && (131070LL - (long long )a) - (long long )y >= 0LL)
        && (131070LL - (long long )a) - (long long )u >= 0LL) && (131070LL - (long
        long )b) - (long long )y >= 0LL) && (131070LL - (long long )b) - (long long
        )u >= 0LL) && (131070LL - (long long )u) - (long long )y >= 0LL) && (262140LL
        - (long long )a) - (long long )v >= 0LL) && (262140LL - (long long )b) - (long
        long )v >= 0LL) && (262140LL - (long long )u) - (long long )v >= 0LL) && (262140LL
        - (long long )v) - (long long )y >= 0LL) && (4295032830LL - (long long )x)
        - (long long )y >= 0LL) && (4295032830LL - (long long )u) - (long long )x
        >= 0LL) && (4295163900LL - (long long )v) - (long long )x >= 0LL) && (long
        long )b - (long long )y >= 0LL) && (long long )b - (long long )u >= 0LL) &&
        (long long )u - (long long )y >= 0LL) && b == y) && b == u) && y == u)) ||
        ((((((((((((((((((((((((((((((((((((((-1LL + (long long )a) + (long long )y
        >= 0LL && (-1LL + (long long )a) + (long long )u >= 0LL) && (-1LL + (long
        long )b) + (long long )y >= 0LL) && (-1LL + (long long )b) + (long long )u
        >= 0LL) && (65535LL - (long long )a) + (long long )y >= 0LL) && (65535LL -
        (long long )a) + (long long )u >= 0LL) && (65535LL - (long long )b) + (long
        long )y >= 0LL) && (65535LL - (long long )b) + (long long )u >= 0LL) && (4294967295LL
        - (long long )x) + (long long )y >= 0LL) && (4294967295LL - (long long )u)
        + (long long )x >= 0LL) && (4294967295LL - (long long )u) + (long long )y
        >= 0LL) && (4294967295LL - (long long )v) + (long long )x >= 0LL) && (4294967295LL
        - (long long )v) + (long long )y >= 0LL) && (long long )x + (long long )y
        >= 0LL) && (long long )u + (long long )x >= 0LL) && (long long )u + (long
        long )y >= 0LL) && (4294967294LL + (long long )a) - (long long )y >= 0LL)
        && (4294967294LL + (long long )a) - (long long )u >= 0LL) && (4294967294LL
        + (long long )a) - (long long )v >= 0LL) && (4294967294LL + (long long )b)
        - (long long )y >= 0LL) && (4294967294LL + (long long )b) - (long long )u
        >= 0LL) && (4294967294LL + (long long )b) - (long long )v >= 0LL) && (4294967295LL
        + (long long )x) - (long long )y >= 0LL) && (4294967295LL + (long long )u)
        - (long long )x >= 0LL) && (4294967295LL + (long long )u) - (long long )y
        >= 0LL) && (4294967295LL + (long long )u) - (long long )v >= 0LL) && (4295032830LL
        - (long long )a) - (long long )y >= 0LL) && (4295032830LL - (long long )a)
        - (long long )u >= 0LL) && (4295032830LL - (long long )a) - (long long )v
        >= 0LL) && (4295032830LL - (long long )b) - (long long )y >= 0LL) && (4295032830LL
        - (long long )b) - (long long )u >= 0LL) && (4295032830LL - (long long )b)
        - (long long )v >= 0LL) && (8589934590LL - (long long )x) - (long long )y
        >= 0LL) && (8589934590LL - (long long )u) - (long long )x >= 0LL) && (8589934590LL
        - (long long )u) - (long long )y >= 0LL) && (8589934590LL - (long long )u)
        - (long long )v >= 0LL) && (8589934590LL - (long long )v) - (long long )x
        >= 0LL) && (8589934590LL - (long long )v) - (long long )y >= 0LL)) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((1U
        <= y && 1U <= u) && 2U <= v) && y <= 65535U) && u <= 65535U) && v <= 131070U)
        && (-3LL + (long long )a) + (long long )v >= 0LL) && (-3LL + (long long )b)
        + (long long )v >= 0LL) && (-3LL + (long long )u) + (long long )v >= 0LL)
        && (-3LL + (long long )v) + (long long )y >= 0LL) && (-2LL + (long long )a)
        + (long long )y >= 0LL) && (-2LL + (long long )a) + (long long )u >= 0LL)
        && (-2LL + (long long )b) + (long long )y >= 0LL) && (-2LL + (long long )b)
        + (long long )u >= 0LL) && (-2LL + (long long )u) + (long long )y >= 0LL)
        && (-2LL + (long long )v) + (long long )x >= 0LL) && (-1LL + (long long )x)
        + (long long )y >= 0LL) && (-1LL + (long long )u) + (long long )x >= 0LL)
        && (-1LL - (long long )b) + (long long )v >= 0LL) && (-1LL - (long long )u)
        + (long long )v >= 0LL) && (0LL - (long long )b) + (long long )y >= 0LL) &&
        (0LL - (long long )b) + (long long )u >= 0LL) && (0LL - (long long )u) + (long
        long )y >= 0LL) && (65533LL - (long long )a) + (long long )v >= 0LL) && (65534LL
        - (long long )a) + (long long )y >= 0LL) && (65534LL - (long long )a) + (long
        long )u >= 0LL) && (65535LL - (long long )u) + (long long )x >= 0LL) && (65535LL
        - (long long )v) + (long long )y >= 0LL) && (131070LL - (long long )v) + (long
        long )x >= 0LL) && (4294967294LL - (long long )x) + (long long )y >= 0LL)
        && (-1LL + (long long )v) - (long long )y >= 0LL) && (65534LL + (long long
        )a) - (long long )y >= 0LL) && (65534LL + (long long )a) - (long long )u >=
        0LL) && (65535LL + (long long )b) - (long long )v >= 0LL) && (65535LL + (long
        long )x) - (long long )y >= 0LL) && (65535LL + (long long )u) - (long long
        )v >= 0LL) && (131069LL + (long long )a) - (long long )v >= 0LL) && (4294967293LL
        + (long long )v) - (long long )x >= 0LL) && (4294967294LL + (long long )u)
        - (long long )x >= 0LL) && (131070LL - (long long )a) - (long long )y >= 0LL)
        && (131070LL - (long long )a) - (long long )u >= 0LL) && (131070LL - (long
        long )b) - (long long )y >= 0LL) && (131070LL - (long long )b) - (long long
        )u >= 0LL) && (131070LL - (long long )u) - (long long )y >= 0LL) && (196605LL
        - (long long )a) - (long long )v >= 0LL) && (196605LL - (long long )b) - (long
        long )v >= 0LL) && (196605LL - (long long )u) - (long long )v >= 0LL) && (196605LL
        - (long long )v) - (long long )y >= 0LL) && (4295032830LL - (long long )x)
        - (long long )y >= 0LL) && (4295032830LL - (long long )u) - (long long )x
        >= 0LL) && (4295098365LL - (long long )v) - (long long )x >= 0LL) && (long
        long )b - (long long )y >= 0LL) && (long long )b - (long long )u >= 0LL) &&
        (long long )u - (long long )y >= 0LL) && b == y) && b == u) && y == u)) ||
        ((((((((((((((((((((((((((((((((((((((((((((((((((((((((1U <= y && 1U <= u)
        && 1U <= v) && y <= 65535U) && u <= 65535U) && v <= 65535U) && (-2LL + (long
        long )a) + (long long )y >= 0LL) && (-2LL + (long long )a) + (long long )u
        >= 0LL) && (-2LL + (long long )a) + (long long )v >= 0LL) && (-2LL + (long
        long )b) + (long long )y >= 0LL) && (-2LL + (long long )b) + (long long )u
        >= 0LL) && (-2LL + (long long )b) + (long long )v >= 0LL) && (-2LL + (long
        long )u) + (long long )y >= 0LL) && (-2LL + (long long )u) + (long long )v
        >= 0LL) && (-2LL + (long long )v) + (long long )y >= 0LL) && (-1LL + (long
        long )x) + (long long )y >= 0LL) && (-1LL + (long long )u) + (long long )x
        >= 0LL) && (-1LL + (long long )v) + (long long )x >= 0LL) && (0LL - (long
        long )b) + (long long )y >= 0LL) && (0LL - (long long )b) + (long long )u
        >= 0LL) && (0LL - (long long )b) + (long long )v >= 0LL) && (0LL - (long long
        )u) + (long long )y >= 0LL) && (0LL - (long long )u) + (long long )v >= 0LL)
        && (0LL - (long long )v) + (long long )y >= 0LL) && (65534LL - (long long
        )a) + (long long )y >= 0LL) && (65534LL - (long long )a) + (long long )u >=
        0LL) && (65534LL - (long long )a) + (long long )v >= 0LL) && (65535LL - (long
        long )u) + (long long )x >= 0LL) && (65535LL - (long long )v) + (long long
        )x >= 0LL) && (4294967294LL - (long long )x) + (long long )y >= 0LL) && (65534LL
        + (long long )a) - (long long )y >= 0LL) && (65534LL + (long long )a) - (long
        long )u >= 0LL) && (65534LL + (long long )a) - (long long )v >= 0LL) && (65535LL
        + (long long )x) - (long long )y >= 0LL) && (4294967294LL + (long long )u)
        - (long long )x >= 0LL) && (4294967294LL + (long long )v) - (long long )x
        >= 0LL) && (131070LL - (long long )a) - (long long )y >= 0LL) && (131070LL
        - (long long )a) - (long long )u >= 0LL) && (131070LL - (long long )a) - (long
        long )v >= 0LL) && (131070LL - (long long )b) - (long long )y >= 0LL) && (131070LL
        - (long long )b) - (long long )u >= 0LL) && (131070LL - (long long )b) - (long
        long )v >= 0LL) && (131070LL - (long long )u) - (long long )y >= 0LL) && (131070LL
        - (long long )u) - (long long )v >= 0LL) && (131070LL - (long long )v) - (long
        long )y >= 0LL) && (4295032830LL - (long long )x) - (long long )y >= 0LL)
        && (4295032830LL - (long long )u) - (long long )x >= 0LL) && (4295032830LL
        - (long long )v) - (long long )x >= 0LL) && (long long )b - (long long )y
        >= 0LL) && (long long )b - (long long )u >= 0LL) && (long long )b - (long
        long )v >= 0LL) && (long long )u - (long long )y >= 0LL) && (long long )u
        - (long long )v >= 0LL) && (long long )v - (long long )y >= 0LL) && b == y)
        && b == u) && y == u))) || (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((1U
        <= x && 1U <= y) && 1U <= u) && x <= 65535U) && y <= 65535U) && u <= 65535U)
        && (-2LL + (long long )a) + (long long )x >= 0LL) && (-2LL + (long long )a)
        + (long long )y >= 0LL) && (-2LL + (long long )a) + (long long )u >= 0LL)
        && (-2LL + (long long )b) + (long long )x >= 0LL) && (-2LL + (long long )b)
        + (long long )y >= 0LL) && (-2LL + (long long )b) + (long long )u >= 0LL)
        && (-2LL + (long long )x) + (long long )y >= 0LL) && (-2LL + (long long )u)
        + (long long )x >= 0LL) && (-2LL + (long long )u) + (long long )y >= 0LL)
        && (-1LL + (long long )a) + (long long )v >= 0LL) && (-1LL + (long long )b)
        + (long long )v >= 0LL) && (-1LL + (long long )u) + (long long )v >= 0LL)
        && (-1LL + (long long )v) + (long long )x >= 0LL) && (-1LL + (long long )v)
        + (long long )y >= 0LL) && (-1LL - (long long )v) + (long long )x >= 0LL)
        && (-1LL - (long long )v) + (long long )y >= 0LL) && (0LL - (long long )a)
        + (long long )x >= 0LL) && (0LL - (long long )b) + (long long )y >= 0LL) &&
        (0LL - (long long )b) + (long long )u >= 0LL) && (0LL - (long long )u) + (long
        long )y >= 0LL) && (65534LL - (long long )a) + (long long )y >= 0LL) && (65534LL
        - (long long )a) + (long long )u >= 0LL) && (65534LL - (long long )b) + (long
        long )x >= 0LL) && (65534LL - (long long )x) + (long long )y >= 0LL) && (65534LL
        - (long long )u) + (long long )x >= 0LL) && (65535LL - (long long )a) + (long
        long )v >= 0LL) && (65535LL - (long long )b) + (long long )v >= 0LL) && (65535LL
        - (long long )u) + (long long )v >= 0LL) && (-1LL + (long long )a) - (long
        long )v >= 0LL) && (-1LL + (long long )b) - (long long )v >= 0LL) && (-1LL
        + (long long )u) - (long long )v >= 0LL) && (65534LL + (long long )a) - (long
        long )y >= 0LL) && (65534LL + (long long )a) - (long long )u >= 0LL) && (65534LL
        + (long long )b) - (long long )x >= 0LL) && (65534LL + (long long )x) - (long
        long )y >= 0LL) && (65534LL + (long long )u) - (long long )x >= 0LL) && (65535LL
        + (long long )v) - (long long )x >= 0LL) && (65535LL + (long long )v) - (long
        long )y >= 0LL) && (65535LL - (long long )a) - (long long )v >= 0LL) && (65535LL
        - (long long )b) - (long long )v >= 0LL) && (65535LL - (long long )u) - (long
        long )v >= 0LL) && (65535LL - (long long )v) - (long long )x >= 0LL) && (65535LL
        - (long long )v) - (long long )y >= 0LL) && (131070LL - (long long )a) - (long
        long )x >= 0LL) && (131070LL - (long long )a) - (long long )y >= 0LL) && (131070LL
        - (long long )a) - (long long )u >= 0LL) && (131070LL - (long long )b) - (long
        long )x >= 0LL) && (131070LL - (long long )b) - (long long )y >= 0LL) && (131070LL
        - (long long )b) - (long long )u >= 0LL) && (131070LL - (long long )x) - (long
        long )y >= 0LL) && (131070LL - (long long )u) - (long long )x >= 0LL) && (131070LL
        - (long long )u) - (long long )y >= 0LL) && (long long )a - (long long )x
        >= 0LL) && (long long )b - (long long )y >= 0LL) && (long long )b - (long
        long )u >= 0LL) && (long long )u - (long long )y >= 0LL) && 0U == v) && a
        == x) && b == y) && b == u) && y == u) && v == 0U)) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((-1LL
        + (long long )a) + (long long )x >= 0LL && (-1LL + (long long )a) + (long
        long )y >= 0LL) && (-1LL + (long long )a) + (long long )u >= 0LL) && (-1LL
        + (long long )a) + (long long )v >= 0LL) && (-1LL + (long long )b) + (long
        long )x >= 0LL) && (-1LL + (long long )b) + (long long )y >= 0LL) && (-1LL
        + (long long )b) + (long long )u >= 0LL) && (-1LL + (long long )b) + (long
        long )v >= 0LL) && (65535LL - (long long )a) + (long long )x >= 0LL) && (65535LL
        - (long long )a) + (long long )y >= 0LL) && (65535LL - (long long )a) + (long
        long )u >= 0LL) && (65535LL - (long long )a) + (long long )v >= 0LL) && (65535LL
        - (long long )b) + (long long )x >= 0LL) && (65535LL - (long long )b) + (long
        long )y >= 0LL) && (65535LL - (long long )b) + (long long )u >= 0LL) && (65535LL
        - (long long )b) + (long long )v >= 0LL) && (4294967295LL - (long long )x)
        + (long long )y >= 0LL) && (4294967295LL - (long long )u) + (long long )x
        >= 0LL) && (4294967295LL - (long long )u) + (long long )y >= 0LL) && (4294967295LL
        - (long long )u) + (long long )v >= 0LL) && (4294967295LL - (long long )v)
        + (long long )x >= 0LL) && (4294967295LL - (long long )v) + (long long )y
        >= 0LL) && (long long )x + (long long )y >= 0LL) && (long long )u + (long
        long )x >= 0LL) && (long long )u + (long long )y >= 0LL) && (long long )u
        + (long long )v >= 0LL) && (long long )v + (long long )x >= 0LL) && (long
        long )v + (long long )y >= 0LL) && (4294967294LL + (long long )a) - (long
        long )x >= 0LL) && (4294967294LL + (long long )a) - (long long )y >= 0LL)
        && (4294967294LL + (long long )a) - (long long )u >= 0LL) && (4294967294LL
        + (long long )a) - (long long )v >= 0LL) && (4294967294LL + (long long )b)
        - (long long )x >= 0LL) && (4294967294LL + (long long )b) - (long long )y
        >= 0LL) && (4294967294LL + (long long )b) - (long long )u >= 0LL) && (4294967294LL
        + (long long )b) - (long long )v >= 0LL) && (4294967295LL + (long long )x)
        - (long long )y >= 0LL) && (4294967295LL + (long long )u) - (long long )x
        >= 0LL) && (4294967295LL + (long long )u) - (long long )y >= 0LL) && (4294967295LL
        + (long long )u) - (long long )v >= 0LL) && (4294967295LL + (long long )v)
        - (long long )x >= 0LL) && (4294967295LL + (long long )v) - (long long )y
        >= 0LL) && (4295032830LL - (long long )a) - (long long )x >= 0LL) && (4295032830LL
        - (long long )a) - (long long )y >= 0LL) && (4295032830LL - (long long )a)
        - (long long )u >= 0LL) && (4295032830LL - (long long )a) - (long long )v
        >= 0LL) && (4295032830LL - (long long )b) - (long long )x >= 0LL) && (4295032830LL
        - (long long )b) - (long long )y >= 0LL) && (4295032830LL - (long long )b)
        - (long long )u >= 0LL) && (4295032830LL - (long long )b) - (long long )v
        >= 0LL) && (8589934590LL - (long long )x) - (long long )y >= 0LL) && (8589934590LL
        - (long long )u) - (long long )x >= 0LL) && (8589934590LL - (long long )u)
        - (long long )y >= 0LL) && (8589934590LL - (long long )u) - (long long )v
        >= 0LL) && (8589934590LL - (long long )v) - (long long )x >= 0LL) && (8589934590LL
        - (long long )v) - (long long )y >= 0LL)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 42
        column: 5
        function: main
      value: 1U <= a
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 42
        column: 5
        function: main
      value: 1U <= b
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 42
        column: 5
        function: main
      value: a <= 65535U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 42
        column: 5
        function: main
      value: b <= 65535U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 42
        column: 5
        function: main
      value: (-2LL + (long long )a) + (long long )b >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 42
        column: 5
        function: main
      value: (65534LL - (long long )a) + (long long )b >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 42
        column: 5
        function: main
      value: (65534LL + (long long )a) - (long long )b >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 42
        column: 5
        function: main
      value: (131070LL - (long long )a) - (long long )b >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 42
        column: 5
        function: main
      value: ((((((((((((((((((((((((((((((((((((((((((((((-1LL + (long long )a) +
        (long long )x >= 0LL && (-1LL + (long long )a) + (long long )y >= 0LL) &&
        (-1LL + (long long )a) + (long long )u >= 0LL) && (-1LL + (long long )b) +
        (long long )x >= 0LL) && (-1LL + (long long )b) + (long long )y >= 0LL) &&
        (-1LL + (long long )b) + (long long )u >= 0LL) && (65535LL - (long long )a)
        + (long long )x >= 0LL) && (65535LL - (long long )a) + (long long )y >= 0LL)
        && (65535LL - (long long )a) + (long long )u >= 0LL) && (65535LL - (long long
        )b) + (long long )x >= 0LL) && (65535LL - (long long )b) + (long long )y >=
        0LL) && (65535LL - (long long )b) + (long long )u >= 0LL) && (4294967295LL
        - (long long )x) + (long long )y >= 0LL) && (4294967295LL - (long long )u)
        + (long long )x >= 0LL) && (4294967295LL - (long long )u) + (long long )y
        >= 0LL) && (4294967295LL - (long long )v) + (long long )x >= 0LL) && (4294967295LL
        - (long long )v) + (long long )y >= 0LL) && (long long )x + (long long )y
        >= 0LL) && (long long )u + (long long )x >= 0LL) && (long long )u + (long
        long )y >= 0LL) && (4294967294LL + (long long )a) - (long long )x >= 0LL)
        && (4294967294LL + (long long )a) - (long long )y >= 0LL) && (4294967294LL
        + (long long )a) - (long long )u >= 0LL) && (4294967294LL + (long long )a)
        - (long long )v >= 0LL) && (4294967294LL + (long long )b) - (long long )x
        >= 0LL) && (4294967294LL + (long long )b) - (long long )y >= 0LL) && (4294967294LL
        + (long long )b) - (long long )u >= 0LL) && (4294967294LL + (long long )b)
        - (long long )v >= 0LL) && (4294967295LL + (long long )x) - (long long )y
        >= 0LL) && (4294967295LL + (long long )u) - (long long )x >= 0LL) && (4294967295LL
        + (long long )u) - (long long )y >= 0LL) && (4294967295LL + (long long )u)
        - (long long )v >= 0LL) && (4295032830LL - (long long )a) - (long long )x
        >= 0LL) && (4295032830LL - (long long )a) - (long long )y >= 0LL) && (4295032830LL
        - (long long )a) - (long long )u >= 0LL) && (4295032830LL - (long long )a)
        - (long long )v >= 0LL) && (4295032830LL - (long long )b) - (long long )x
        >= 0LL) && (4295032830LL - (long long )b) - (long long )y >= 0LL) && (4295032830LL
        - (long long )b) - (long long )u >= 0LL) && (4295032830LL - (long long )b)
        - (long long )v >= 0LL) && (8589934590LL - (long long )x) - (long long )y
        >= 0LL) && (8589934590LL - (long long )u) - (long long )x >= 0LL) && (8589934590LL
        - (long long )u) - (long long )y >= 0LL) && (8589934590LL - (long long )u)
        - (long long )v >= 0LL) && (8589934590LL - (long long )v) - (long long )x
        >= 0LL) && (8589934590LL - (long long )v) - (long long )y >= 0LL) || (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((1U
        <= x && 1U <= y) && 1U <= u) && x <= 65535U) && y <= 65535U) && u <= 65535U)
        && (-2LL + (long long )a) + (long long )x >= 0LL) && (-2LL + (long long )a)
        + (long long )y >= 0LL) && (-2LL + (long long )a) + (long long )u >= 0LL)
        && (-2LL + (long long )b) + (long long )x >= 0LL) && (-2LL + (long long )b)
        + (long long )y >= 0LL) && (-2LL + (long long )b) + (long long )u >= 0LL)
        && (-2LL + (long long )x) + (long long )y >= 0LL) && (-2LL + (long long )u)
        + (long long )x >= 0LL) && (-2LL + (long long )u) + (long long )y >= 0LL)
        && (-1LL + (long long )a) + (long long )v >= 0LL) && (-1LL + (long long )b)
        + (long long )v >= 0LL) && (-1LL + (long long )u) + (long long )v >= 0LL)
        && (-1LL + (long long )v) + (long long )x >= 0LL) && (-1LL + (long long )v)
        + (long long )y >= 0LL) && (-1LL - (long long )v) + (long long )x >= 0LL)
        && (-1LL - (long long )v) + (long long )y >= 0LL) && (0LL - (long long )a)
        + (long long )x >= 0LL) && (0LL - (long long )b) + (long long )y >= 0LL) &&
        (0LL - (long long )b) + (long long )u >= 0LL) && (0LL - (long long )u) + (long
        long )y >= 0LL) && (65534LL - (long long )a) + (long long )y >= 0LL) && (65534LL
        - (long long )a) + (long long )u >= 0LL) && (65534LL - (long long )b) + (long
        long )x >= 0LL) && (65534LL - (long long )x) + (long long )y >= 0LL) && (65534LL
        - (long long )u) + (long long )x >= 0LL) && (65535LL - (long long )a) + (long
        long )v >= 0LL) && (65535LL - (long long )b) + (long long )v >= 0LL) && (65535LL
        - (long long )u) + (long long )v >= 0LL) && (-1LL + (long long )a) - (long
        long )v >= 0LL) && (-1LL + (long long )b) - (long long )v >= 0LL) && (-1LL
        + (long long )u) - (long long )v >= 0LL) && (65534LL + (long long )a) - (long
        long )y >= 0LL) && (65534LL + (long long )a) - (long long )u >= 0LL) && (65534LL
        + (long long )b) - (long long )x >= 0LL) && (65534LL + (long long )x) - (long
        long )y >= 0LL) && (65534LL + (long long )u) - (long long )x >= 0LL) && (65535LL
        + (long long )v) - (long long )x >= 0LL) && (65535LL + (long long )v) - (long
        long )y >= 0LL) && (65535LL - (long long )a) - (long long )v >= 0LL) && (65535LL
        - (long long )b) - (long long )v >= 0LL) && (65535LL - (long long )u) - (long
        long )v >= 0LL) && (65535LL - (long long )v) - (long long )x >= 0LL) && (65535LL
        - (long long )v) - (long long )y >= 0LL) && (131070LL - (long long )a) - (long
        long )x >= 0LL) && (131070LL - (long long )a) - (long long )y >= 0LL) && (131070LL
        - (long long )a) - (long long )u >= 0LL) && (131070LL - (long long )b) - (long
        long )x >= 0LL) && (131070LL - (long long )b) - (long long )y >= 0LL) && (131070LL
        - (long long )b) - (long long )u >= 0LL) && (131070LL - (long long )x) - (long
        long )y >= 0LL) && (131070LL - (long long )u) - (long long )x >= 0LL) && (131070LL
        - (long long )u) - (long long )y >= 0LL) && (long long )a - (long long )x
        >= 0LL) && (long long )b - (long long )y >= 0LL) && (long long )b - (long
        long )u >= 0LL) && (long long )u - (long long )y >= 0LL) && 0U == v) && a
        == x) && b == y) && b == u) && y == u) && v == 0U)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: 1U <= a
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: 1U <= b
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: a <= 65535U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: b <= 65535U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: (-2LL + (long long )a) + (long long )b >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: (-1LL + (long long )a) + (long long )x >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: (-1LL + (long long )b) + (long long )x >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: (65534LL - (long long )a) + (long long )b >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: (65535LL - (long long )a) + (long long )x >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: (65535LL - (long long )b) + (long long )x >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: (4294967295LL - (long long )v) + (long long )x >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: (65534LL + (long long )a) - (long long )b >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: (4294967294LL + (long long )a) - (long long )x >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: (4294967294LL + (long long )a) - (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: (4294967294LL + (long long )b) - (long long )x >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: (4294967294LL + (long long )b) - (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: (131070LL - (long long )a) - (long long )b >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: (4295032830LL - (long long )a) - (long long )x >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: (4295032830LL - (long long )a) - (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: (4295032830LL - (long long )b) - (long long )x >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: (4295032830LL - (long long )b) - (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: (8589934590LL - (long long )v) - (long long )x >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-nla/lcm1-both-nt.c
        line: 55
        column: 9
        function: main
      value: (((((((((((((((((((((((((((((((((((((((((-1LL + (long long )a) + (long
        long )y >= 0LL && (-1LL + (long long )a) + (long long )u >= 0LL) && (-1LL
        + (long long )b) + (long long )y >= 0LL) && (-1LL + (long long )b) + (long
        long )u >= 0LL) && (65535LL - (long long )a) + (long long )y >= 0LL) && (65535LL
        - (long long )a) + (long long )u >= 0LL) && (65535LL - (long long )b) + (long
        long )y >= 0LL) && (65535LL - (long long )b) + (long long )u >= 0LL) && (4294967295LL
        - (long long )x) + (long long )y >= 0LL) && (4294967295LL - (long long )u)
        + (long long )x >= 0LL) && (4294967295LL - (long long )u) + (long long )y
        >= 0LL) && (4294967295LL - (long long )v) + (long long )y >= 0LL) && (long
        long )x + (long long )y >= 0LL) && (long long )u + (long long )x >= 0LL) &&
        (long long )u + (long long )y >= 0LL) && (4294967294LL + (long long )a) -
        (long long )y >= 0LL) && (4294967294LL + (long long )a) - (long long )u >=
        0LL) && (4294967294LL + (long long )b) - (long long )y >= 0LL) && (4294967294LL
        + (long long )b) - (long long )u >= 0LL) && (4294967295LL + (long long )x)
        - (long long )y >= 0LL) && (4294967295LL + (long long )u) - (long long )x
        >= 0LL) && (4294967295LL + (long long )u) - (long long )y >= 0LL) && (4294967295LL
        + (long long )u) - (long long )v >= 0LL) && (4295032830LL - (long long )a)
        - (long long )y >= 0LL) && (4295032830LL - (long long )a) - (long long )u
        >= 0LL) && (4295032830LL - (long long )b) - (long long )y >= 0LL) && (4295032830LL
        - (long long )b) - (long long )u >= 0LL) && (8589934590LL - (long long )x)
        - (long long )y >= 0LL) && (8589934590LL - (long long )u) - (long long )x
        >= 0LL) && (8589934590LL - (long long )u) - (long long )y >= 0LL) && (8589934590LL
        - (long long )u) - (long long )v >= 0LL) && (8589934590LL - (long long )v)
        - (long long )y >= 0LL) || ((((((((((((((((((((((((((((((((((((((1U <= y &&
        1U <= u) && y <= 65535U) && u <= 65535U) && (-2LL + (long long )a) + (long
        long )y >= 0LL) && (-2LL + (long long )a) + (long long )u >= 0LL) && (-2LL
        + (long long )b) + (long long )y >= 0LL) && (-2LL + (long long )b) + (long
        long )u >= 0LL) && (-2LL + (long long )u) + (long long )y >= 0LL) && (-1LL
        + (long long )x) + (long long )y >= 0LL) && (-1LL + (long long )u) + (long
        long )x >= 0LL) && (0LL - (long long )b) + (long long )y >= 0LL) && (0LL -
        (long long )b) + (long long )u >= 0LL) && (0LL - (long long )u) + (long long
        )y >= 0LL) && (65534LL - (long long )a) + (long long )y >= 0LL) && (65534LL
        - (long long )a) + (long long )u >= 0LL) && (65535LL - (long long )u) + (long
        long )x >= 0LL) && (4294967294LL - (long long )x) + (long long )y >= 0LL)
        && (4294967294LL - (long long )v) + (long long )y >= 0LL) && (65534LL + (long
        long )a) - (long long )y >= 0LL) && (65534LL + (long long )a) - (long long
        )u >= 0LL) && (65535LL + (long long )x) - (long long )y >= 0LL) && (4294967294LL
        + (long long )u) - (long long )x >= 0LL) && (4294967294LL + (long long )u)
        - (long long )v >= 0LL) && (131070LL - (long long )a) - (long long )y >= 0LL)
        && (131070LL - (long long )a) - (long long )u >= 0LL) && (131070LL - (long
        long )b) - (long long )y >= 0LL) && (131070LL - (long long )b) - (long long
        )u >= 0LL) && (131070LL - (long long )u) - (long long )y >= 0LL) && (4295032830LL
        - (long long )x) - (long long )y >= 0LL) && (4295032830LL - (long long )u)
        - (long long )x >= 0LL) && (4295032830LL - (long long )u) - (long long )v
        >= 0LL) && (4295032830LL - (long long )v) - (long long )y >= 0LL) && (long
        long )b - (long long )y >= 0LL) && (long long )b - (long long )u >= 0LL) &&
        (long long )u - (long long )y >= 0LL) && b == y) && b == u) && y == u)) ||
        ((((((((((((((((((((((((((((((((-1LL + (long long )a) + (long long )y >= 0LL
        && (-1LL + (long long )a) + (long long )u >= 0LL) && (-1LL + (long long )b)
        + (long long )y >= 0LL) && (-1LL + (long long )b) + (long long )u >= 0LL)
        && (65535LL - (long long )a) + (long long )y >= 0LL) && (65535LL - (long long
        )a) + (long long )u >= 0LL) && (65535LL - (long long )b) + (long long )y >=
        0LL) && (65535LL - (long long )b) + (long long )u >= 0LL) && (4294967295LL
        - (long long )x) + (long long )y >= 0LL) && (4294967295LL - (long long )u)
        + (long long )x >= 0LL) && (4294967295LL - (long long )u) + (long long )y
        >= 0LL) && (4294967295LL - (long long )v) + (long long )y >= 0LL) && (long
        long )x + (long long )y >= 0LL) && (long long )u + (long long )x >= 0LL) &&
        (long long )u + (long long )y >= 0LL) && (4294967294LL + (long long )a) -
        (long long )y >= 0LL) && (4294967294LL + (long long )a) - (long long )u >=
        0LL) && (4294967294LL + (long long )b) - (long long )y >= 0LL) && (4294967294LL
        + (long long )b) - (long long )u >= 0LL) && (4294967295LL + (long long )x)
        - (long long )y >= 0LL) && (4294967295LL + (long long )u) - (long long )x
        >= 0LL) && (4294967295LL + (long long )u) - (long long )y >= 0LL) && (4294967295LL
        + (long long )u) - (long long )v >= 0LL) && (4295032830LL - (long long )a)
        - (long long )y >= 0LL) && (4295032830LL - (long long )a) - (long long )u
        >= 0LL) && (4295032830LL - (long long )b) - (long long )y >= 0LL) && (4295032830LL
        - (long long )b) - (long long )u >= 0LL) && (8589934590LL - (long long )x)
        - (long long )y >= 0LL) && (8589934590LL - (long long )u) - (long long )x
        >= 0LL) && (8589934590LL - (long long )u) - (long long )y >= 0LL) && (8589934590LL
        - (long long )u) - (long long )v >= 0LL) && (8589934590LL - (long long )v)
        - (long long )y >= 0LL)) || ((((((((((((((((((((((((((((((((-1LL + (long long
        )a) + (long long )y >= 0LL && (-1LL + (long long )a) + (long long )u >= 0LL)
        && (-1LL + (long long )b) + (long long )y >= 0LL) && (-1LL + (long long )b)
        + (long long )u >= 0LL) && (65535LL - (long long )a) + (long long )y >= 0LL)
        && (65535LL - (long long )a) + (long long )u >= 0LL) && (65535LL - (long long
        )b) + (long long )y >= 0LL) && (65535LL - (long long )b) + (long long )u >=
        0LL) && (4294967295LL - (long long )x) + (long long )y >= 0LL) && (4294967295LL
        - (long long )u) + (long long )x >= 0LL) && (4294967295LL - (long long )u)
        + (long long )y >= 0LL) && (4294967295LL - (long long )v) + (long long )y
        >= 0LL) && (long long )x + (long long )y >= 0LL) && (long long )u + (long
        long )x >= 0LL) && (long long )u + (long long )y >= 0LL) && (4294967294LL
        + (long long )a) - (long long )y >= 0LL) && (4294967294LL + (long long )a)
        - (long long )u >= 0LL) && (4294967294LL + (long long )b) - (long long )y
        >= 0LL) && (4294967294LL + (long long )b) - (long long )u >= 0LL) && (4294967295LL
        + (long long )x) - (long long )y >= 0LL) && (4294967295LL + (long long )u)
        - (long long )x >= 0LL) && (4294967295LL + (long long )u) - (long long )y
        >= 0LL) && (4294967295LL + (long long )u) - (long long )v >= 0LL) && (4295032830LL
        - (long long )a) - (long long )y >= 0LL) && (4295032830LL - (long long )a)
        - (long long )u >= 0LL) && (4295032830LL - (long long )b) - (long long )y
        >= 0LL) && (4295032830LL - (long long )b) - (long long )u >= 0LL) && (8589934590LL
        - (long long )x) - (long long )y >= 0LL) && (8589934590LL - (long long )u)
        - (long long )x >= 0LL) && (8589934590LL - (long long )u) - (long long )y
        >= 0LL) && (8589934590LL - (long long )u) - (long long )v >= 0LL) && (8589934590LL
        - (long long )v) - (long long )y >= 0LL)) || ((((((((((((((((((((((((((((((((-1LL
        + (long long )a) + (long long )y >= 0LL && (-1LL + (long long )a) + (long
        long )u >= 0LL) && (-1LL + (long long )b) + (long long )y >= 0LL) && (-1LL
        + (long long )b) + (long long )u >= 0LL) && (65535LL - (long long )a) + (long
        long )y >= 0LL) && (65535LL - (long long )a) + (long long )u >= 0LL) && (65535LL
        - (long long )b) + (long long )y >= 0LL) && (65535LL - (long long )b) + (long
        long )u >= 0LL) && (4294967295LL - (long long )x) + (long long )y >= 0LL)
        && (4294967295LL - (long long )u) + (long long )x >= 0LL) && (4294967295LL
        - (long long )u) + (long long )y >= 0LL) && (4294967295LL - (long long )v)
        + (long long )y >= 0LL) && (long long )x + (long long )y >= 0LL) && (long
        long )u + (long long )x >= 0LL) && (long long )u + (long long )y >= 0LL) &&
        (4294967294LL + (long long )a) - (long long )y >= 0LL) && (4294967294LL +
        (long long )a) - (long long )u >= 0LL) && (4294967294LL + (long long )b) -
        (long long )y >= 0LL) && (4294967294LL + (long long )b) - (long long )u >=
        0LL) && (4294967295LL + (long long )x) - (long long )y >= 0LL) && (4294967295LL
        + (long long )u) - (long long )x >= 0LL) && (4294967295LL + (long long )u)
        - (long long )y >= 0LL) && (4294967295LL + (long long )u) - (long long )v
        >= 0LL) && (4295032830LL - (long long )a) - (long long )y >= 0LL) && (4295032830LL
        - (long long )a) - (long long )u >= 0LL) && (4295032830LL - (long long )b)
        - (long long )y >= 0LL) && (4295032830LL - (long long )b) - (long long )u
        >= 0LL) && (8589934590LL - (long long )x) - (long long )y >= 0LL) && (8589934590LL
        - (long long )u) - (long long )x >= 0LL) && (8589934590LL - (long long )u)
        - (long long )y >= 0LL) && (8589934590LL - (long long )u) - (long long )v
        >= 0LL) && (8589934590LL - (long long )v) - (long long )y >= 0LL)) || ((((((((((((((((((((((((((((((((-1LL
        + (long long )a) + (long long )y >= 0LL && (-1LL + (long long )a) + (long
        long )u >= 0LL) && (-1LL + (long long )b) + (long long )y >= 0LL) && (-1LL
        + (long long )b) + (long long )u >= 0LL) && (65535LL - (long long )a) + (long
        long )y >= 0LL) && (65535LL - (long long )a) + (long long )u >= 0LL) && (65535LL
        - (long long )b) + (long long )y >= 0LL) && (65535LL - (long long )b) + (long
        long )u >= 0LL) && (4294967295LL - (long long )x) + (long long )y >= 0LL)
        && (4294967295LL - (long long )u) + (long long )x >= 0LL) && (4294967295LL
        - (long long )u) + (long long )y >= 0LL) && (4294967295LL - (long long )v)
        + (long long )y >= 0LL) && (long long )x + (long long )y >= 0LL) && (long
        long )u + (long long )x >= 0LL) && (long long )u + (long long )y >= 0LL) &&
        (4294967294LL + (long long )a) - (long long )y >= 0LL) && (4294967294LL +
        (long long )a) - (long long )u >= 0LL) && (4294967294LL + (long long )b) -
        (long long )y >= 0LL) && (4294967294LL + (long long )b) - (long long )u >=
        0LL) && (4294967295LL + (long long )x) - (long long )y >= 0LL) && (4294967295LL
        + (long long )u) - (long long )x >= 0LL) && (4294967295LL + (long long )u)
        - (long long )y >= 0LL) && (4294967295LL + (long long )u) - (long long )v
        >= 0LL) && (4295032830LL - (long long )a) - (long long )y >= 0LL) && (4295032830LL
        - (long long )a) - (long long )u >= 0LL) && (4295032830LL - (long long )b)
        - (long long )y >= 0LL) && (4295032830LL - (long long )b) - (long long )u
        >= 0LL) && (8589934590LL - (long long )x) - (long long )y >= 0LL) && (8589934590LL
        - (long long )u) - (long long )x >= 0LL) && (8589934590LL - (long long )u)
        - (long long )y >= 0LL) && (8589934590LL - (long long )u) - (long long )v
        >= 0LL) && (8589934590LL - (long long )v) - (long long )y >= 0LL)) || ((((((((((((((((((((((((((((((((-1LL
        + (long long )a) + (long long )y >= 0LL && (-1LL + (long long )a) + (long
        long )u >= 0LL) && (-1LL + (long long )b) + (long long )y >= 0LL) && (-1LL
        + (long long )b) + (long long )u >= 0LL) && (65535LL - (long long )a) + (long
        long )y >= 0LL) && (65535LL - (long long )a) + (long long )u >= 0LL) && (65535LL
        - (long long )b) + (long long )y >= 0LL) && (65535LL - (long long )b) + (long
        long )u >= 0LL) && (4294967295LL - (long long )x) + (long long )y >= 0LL)
        && (4294967295LL - (long long )u) + (long long )x >= 0LL) && (4294967295LL
        - (long long )u) + (long long )y >= 0LL) && (4294967295LL - (long long )v)
        + (long long )y >= 0LL) && (long long )x + (long long )y >= 0LL) && (long
        long )u + (long long )x >= 0LL) && (long long )u + (long long )y >= 0LL) &&
        (4294967294LL + (long long )a) - (long long )y >= 0LL) && (4294967294LL +
        (long long )a) - (long long )u >= 0LL) && (4294967294LL + (long long )b) -
        (long long )y >= 0LL) && (4294967294LL + (long long )b) - (long long )u >=
        0LL) && (4294967295LL + (long long )x) - (long long )y >= 0LL) && (4294967295LL
        + (long long )u) - (long long )x >= 0LL) && (4294967295LL + (long long )u)
        - (long long )y >= 0LL) && (4294967295LL + (long long )u) - (long long )v
        >= 0LL) && (4295032830LL - (long long )a) - (long long )y >= 0LL) && (4295032830LL
        - (long long )a) - (long long )u >= 0LL) && (4295032830LL - (long long )b)
        - (long long )y >= 0LL) && (4295032830LL - (long long )b) - (long long )u
        >= 0LL) && (8589934590LL - (long long )x) - (long long )y >= 0LL) && (8589934590LL
        - (long long )u) - (long long )x >= 0LL) && (8589934590LL - (long long )u)
        - (long long )y >= 0LL) && (8589934590LL - (long long )u) - (long long )v
        >= 0LL) && (8589934590LL - (long long )v) - (long long )y >= 0LL)) || ((((((((((((((((((((((((((((((((-1LL
        + (long long )a) + (long long )y >= 0LL && (-1LL + (long long )a) + (long
        long )u >= 0LL) && (-1LL + (long long )b) + (long long )y >= 0LL) && (-1LL
        + (long long )b) + (long long )u >= 0LL) && (65535LL - (long long )a) + (long
        long )y >= 0LL) && (65535LL - (long long )a) + (long long )u >= 0LL) && (65535LL
        - (long long )b) + (long long )y >= 0LL) && (65535LL - (long long )b) + (long
        long )u >= 0LL) && (4294967295LL - (long long )x) + (long long )y >= 0LL)
        && (4294967295LL - (long long )u) + (long long )x >= 0LL) && (4294967295LL
        - (long long )u) + (long long )y >= 0LL) && (4294967295LL - (long long )v)
        + (long long )y >= 0LL) && (long long )x + (long long )y >= 0LL) && (long
        long )u + (long long )x >= 0LL) && (long long )u + (long long )y >= 0LL) &&
        (4294967294LL + (long long )a) - (long long )y >= 0LL) && (4294967294LL +
        (long long )a) - (long long )u >= 0LL) && (4294967294LL + (long long )b) -
        (long long )y >= 0LL) && (4294967294LL + (long long )b) - (long long )u >=
        0LL) && (4294967295LL + (long long )x) - (long long )y >= 0LL) && (4294967295LL
        + (long long )u) - (long long )x >= 0LL) && (4294967295LL + (long long )u)
        - (long long )y >= 0LL) && (4294967295LL + (long long )u) - (long long )v
        >= 0LL) && (4295032830LL - (long long )a) - (long long )y >= 0LL) && (4295032830LL
        - (long long )a) - (long long )u >= 0LL) && (4295032830LL - (long long )b)
        - (long long )y >= 0LL) && (4295032830LL - (long long )b) - (long long )u
        >= 0LL) && (8589934590LL - (long long )x) - (long long )y >= 0LL) && (8589934590LL
        - (long long )u) - (long long )x >= 0LL) && (8589934590LL - (long long )u)
        - (long long )y >= 0LL) && (8589934590LL - (long long )u) - (long long )v
        >= 0LL) && (8589934590LL - (long long )v) - (long long )y >= 0LL)) || ((((((((((((((((((((((((((((((((-1LL
        + (long long )a) + (long long )y >= 0LL && (-1LL + (long long )a) + (long
        long )u >= 0LL) && (-1LL + (long long )b) + (long long )y >= 0LL) && (-1LL
        + (long long )b) + (long long )u >= 0LL) && (65535LL - (long long )a) + (long
        long )y >= 0LL) && (65535LL - (long long )a) + (long long )u >= 0LL) && (65535LL
        - (long long )b) + (long long )y >= 0LL) && (65535LL - (long long )b) + (long
        long )u >= 0LL) && (4294967295LL - (long long )x) + (long long )y >= 0LL)
        && (4294967295LL - (long long )u) + (long long )x >= 0LL) && (4294967295LL
        - (long long )u) + (long long )y >= 0LL) && (4294967295LL - (long long )v)
        + (long long )y >= 0LL) && (long long )x + (long long )y >= 0LL) && (long
        long )u + (long long )x >= 0LL) && (long long )u + (long long )y >= 0LL) &&
        (4294967294LL + (long long )a) - (long long )y >= 0LL) && (4294967294LL +
        (long long )a) - (long long )u >= 0LL) && (4294967294LL + (long long )b) -
        (long long )y >= 0LL) && (4294967294LL + (long long )b) - (long long )u >=
        0LL) && (4294967295LL + (long long )x) - (long long )y >= 0LL) && (4294967295LL
        + (long long )u) - (long long )x >= 0LL) && (4294967295LL + (long long )u)
        - (long long )y >= 0LL) && (4294967295LL + (long long )u) - (long long )v
        >= 0LL) && (4295032830LL - (long long )a) - (long long )y >= 0LL) && (4295032830LL
        - (long long )a) - (long long )u >= 0LL) && (4295032830LL - (long long )b)
        - (long long )y >= 0LL) && (4295032830LL - (long long )b) - (long long )u
        >= 0LL) && (8589934590LL - (long long )x) - (long long )y >= 0LL) && (8589934590LL
        - (long long )u) - (long long )x >= 0LL) && (8589934590LL - (long long )u)
        - (long long )y >= 0LL) && (8589934590LL - (long long )u) - (long long )v
        >= 0LL) && (8589934590LL - (long long )v) - (long long )y >= 0LL)) || ((((((((((((((((((((((((((((((((-1LL
        + (long long )a) + (long long )y >= 0LL && (-1LL + (long long )a) + (long
        long )u >= 0LL) && (-1LL + (long long )b) + (long long )y >= 0LL) && (-1LL
        + (long long )b) + (long long )u >= 0LL) && (65535LL - (long long )a) + (long
        long )y >= 0LL) && (65535LL - (long long )a) + (long long )u >= 0LL) && (65535LL
        - (long long )b) + (long long )y >= 0LL) && (65535LL - (long long )b) + (long
        long )u >= 0LL) && (4294967295LL - (long long )x) + (long long )y >= 0LL)
        && (4294967295LL - (long long )u) + (long long )x >= 0LL) && (4294967295LL
        - (long long )u) + (long long )y >= 0LL) && (4294967295LL - (long long )v)
        + (long long )y >= 0LL) && (long long )x + (long long )y >= 0LL) && (long
        long )u + (long long )x >= 0LL) && (long long )u + (long long )y >= 0LL) &&
        (4294967294LL + (long long )a) - (long long )y >= 0LL) && (4294967294LL +
        (long long )a) - (long long )u >= 0LL) && (4294967294LL + (long long )b) -
        (long long )y >= 0LL) && (4294967294LL + (long long )b) - (long long )u >=
        0LL) && (4294967295LL + (long long )x) - (long long )y >= 0LL) && (4294967295LL
        + (long long )u) - (long long )x >= 0LL) && (4294967295LL + (long long )u)
        - (long long )y >= 0LL) && (4294967295LL + (long long )u) - (long long )v
        >= 0LL) && (4295032830LL - (long long )a) - (long long )y >= 0LL) && (4295032830LL
        - (long long )a) - (long long )u >= 0LL) && (4295032830LL - (long long )b)
        - (long long )y >= 0LL) && (4295032830LL - (long long )b) - (long long )u
        >= 0LL) && (8589934590LL - (long long )x) - (long long )y >= 0LL) && (8589934590LL
        - (long long )u) - (long long )x >= 0LL) && (8589934590LL - (long long )u)
        - (long long )y >= 0LL) && (8589934590LL - (long long )u) - (long long )v
        >= 0LL) && (8589934590LL - (long long )v) - (long long )y >= 0LL)) || ((((((((((((((((((((((((((((((((-1LL
        + (long long )a) + (long long )y >= 0LL && (-1LL + (long long )a) + (long
        long )u >= 0LL) && (-1LL + (long long )b) + (long long )y >= 0LL) && (-1LL
        + (long long )b) + (long long )u >= 0LL) && (65535LL - (long long )a) + (long
        long )y >= 0LL) && (65535LL - (long long )a) + (long long )u >= 0LL) && (65535LL
        - (long long )b) + (long long )y >= 0LL) && (65535LL - (long long )b) + (long
        long )u >= 0LL) && (4294967295LL - (long long )x) + (long long )y >= 0LL)
        && (4294967295LL - (long long )u) + (long long )x >= 0LL) && (4294967295LL
        - (long long )u) + (long long )y >= 0LL) && (4294967295LL - (long long )v)
        + (long long )y >= 0LL) && (long long )x + (long long )y >= 0LL) && (long
        long )u + (long long )x >= 0LL) && (long long )u + (long long )y >= 0LL) &&
        (4294967294LL + (long long )a) - (long long )y >= 0LL) && (4294967294LL +
        (long long )a) - (long long )u >= 0LL) && (4294967294LL + (long long )b) -
        (long long )y >= 0LL) && (4294967294LL + (long long )b) - (long long )u >=
        0LL) && (4294967295LL + (long long )x) - (long long )y >= 0LL) && (4294967295LL
        + (long long )u) - (long long )x >= 0LL) && (4294967295LL + (long long )u)
        - (long long )y >= 0LL) && (4294967295LL + (long long )u) - (long long )v
        >= 0LL) && (4295032830LL - (long long )a) - (long long )y >= 0LL) && (4295032830LL
        - (long long )a) - (long long )u >= 0LL) && (4295032830LL - (long long )b)
        - (long long )y >= 0LL) && (4295032830LL - (long long )b) - (long long )u
        >= 0LL) && (8589934590LL - (long long )x) - (long long )y >= 0LL) && (8589934590LL
        - (long long )u) - (long long )x >= 0LL) && (8589934590LL - (long long )u)
        - (long long )y >= 0LL) && (8589934590LL - (long long )u) - (long long )v
        >= 0LL) && (8589934590LL - (long long )v) - (long long )y >= 0LL)
      format: c_expression
