- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: fd0acc60-b0ea-43b9-b338-02d1b326452e
    creation_time: 2025-03-22T16:53:56Z
    producer:
      name: Goblint
      version: heads/master-0-g66dff5a90-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp.json'' ''--disable'' ''witness.graphml.enabled''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/termination.prp''
        ''--sets'' ''exp.architecture'' ''64bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-crafted/Mysore-2.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-crafted/Mysore-2.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-crafted/Mysore-2.c: e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7
      data_model: LP64
      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-crafted/Mysore-2.c
        line: 22
        column: 6
        function: main
      value: ((((((((6 <= c && x <= 65521) && (2147483641LL + (long long )c) + (long
        long )x >= 0LL) && (4294967295LL - (long long )c) + (long long )x >= 0LL)
        && (65515LL + (long long )c) - (long long )x >= 0LL) && (65527LL - (long long
        )c) - (long long )x >= 0LL) || (((((((-131074 <= x && 5 <= c) && c <= 65538)
        && x <= 65526) && (65536LL + (long long )c) + (long long )x >= 0LL) && (196612LL
        - (long long )c) + (long long )x >= 0LL) && (65521LL + (long long )c) - (long
        long )x >= 0LL) && (65531LL - (long long )c) - (long long )x >= 0LL)) || (((((((-131072
        <= x && 4 <= c) && c <= 65537) && x <= 65530) && (65535LL + (long long )c)
        + (long long )x >= 0LL) && (196609LL - (long long )c) + (long long )x >= 0LL)
        && (65526LL + (long long )c) - (long long )x >= 0LL) && (65534LL - (long long
        )c) - (long long )x >= 0LL)) || (((((((-131070 <= x && 3 <= c) && c <= 65536)
        && x <= 65533) && (65534LL + (long long )c) + (long long )x >= 0LL) && (196606LL
        - (long long )c) + (long long )x >= 0LL) && (65530LL + (long long )c) - (long
        long )x >= 0LL) && (65536LL - (long long )c) - (long long )x >= 0LL)) || (((((((-65535
        <= x && 2 <= c) && c <= 65535) && x <= 65535) && (65533LL + (long long )c)
        + (long long )x >= 0LL) && (131070LL - (long long )c) + (long long )x >= 0LL)
        && (65533LL + (long long )c) - (long long )x >= 0LL) && (131070LL - (long
        long )c) - (long long )x >= 0LL)
      format: c_expression
