- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 8495fef6-d569-4e32-95a1-1f1c0a6b0eee
    creation_time: 2025-03-22T16:53:47Z
    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/Benghazi.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-crafted/Benghazi.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-crafted/Benghazi.c: 9edf84ee73e15e033440f38035e679f46457b07702832d589a58530a086e57e5
      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/Benghazi.c
        line: 22
        column: 2
        function: main
      value: (((((-1LL + (long long )d2) + (long long )x >= 0LL && (-1LL - (long long
        )d1old) + (long long )d2 >= 0LL) && (long long )d1old + (long long )x >= 0LL)
        && (1LL + (long long )d1old) - (long long )d2 >= 0LL) && (((((((((((((((((((((((((((((((((-2147483424
        <= x && 77 <= d1) && 77 <= d1old) && 78 <= d2) && x <= 2147483347) && d1 <=
        2147483426) && d2 <= 2147483425) && d1old <= 2147483424) && (-155LL + (long
        long )d1) + (long long )d2 >= 0LL) && (-155LL + (long long )d1old) + (long
        long )d2 >= 0LL) && (-154LL + (long long )d1) + (long long )d1old >= 0LL)
        && (2147483345LL + (long long )d1) + (long long )x >= 0LL) && (2147483346LL
        - (long long )d1) + (long long )d2 >= 0LL) && (2147483347LL - (long long )d1)
        + (long long )d1old >= 0LL) && (4294966848LL - (long long )d1old) + (long
        long )x >= 0LL) && (4294966849LL - (long long )d2) + (long long )x >= 0LL)
        && (4294966850LL - (long long )d1) + (long long )x >= 0LL) && (2147483269LL
        + (long long )d2) - (long long )x >= 0LL) && (2147483270LL + (long long )d1)
        - (long long )x >= 0LL) && (2147483270LL + (long long )d1old) - (long long
        )x >= 0LL) && (2147483345LL + (long long )d1) - (long long )d1old >= 0LL)
        && (2147483346LL + (long long )d1) - (long long )d2 >= 0LL) && (2147483424LL
        - (long long )d1) - (long long )x >= 0LL) && (2147483424LL - (long long )d1old)
        - (long long )x >= 0LL) && (2147483425LL - (long long )d2) - (long long )x
        >= 0LL) && (4294966849LL - (long long )d1old) - (long long )d2 >= 0LL) &&
        (4294966850LL - (long long )d1) - (long long )d1old >= 0LL) && (4294966851LL
        - (long long )d1) - (long long )d2 >= 0LL) && d1 % 2 == 1) && d2 % 2 == 0)
        && d1old % 2 == 1) || ((((((((((((((((((((((((-75 <= x && x <= 2147483424)
        && (-153LL + (long long )d1) + (long long )d2 >= 0LL) && (-152LL + (long long
        )d1) + (long long )d1old >= 0LL) && (-151LL + (long long )d1old) + (long long
        )d2 >= 0LL) && (-2LL + (long long )d1) + (long long )x >= 0LL) && (1LL - (long
        long )d1) + (long long )d2 >= 0LL) && (2LL - (long long )d1) + (long long
        )d1old >= 0LL) && (150LL - (long long )d1old) + (long long )x >= 0LL) && (151LL
        - (long long )d2) + (long long )x >= 0LL) && (152LL - (long long )d1) + (long
        long )x >= 0LL) && (-2LL + (long long )d1) - (long long )d1old >= 0LL) &&
        (-1LL + (long long )d1) - (long long )d2 >= 0LL) && (2147483347LL + (long
        long )d1) - (long long )x >= 0LL) && (2147483348LL + (long long )d2) - (long
        long )x >= 0LL) && (2147483349LL + (long long )d1old) - (long long )x >= 0LL)
        && (151LL - (long long )d1old) - (long long )d2 >= 0LL) && (152LL - (long
        long )d1) - (long long )d1old >= 0LL) && (153LL - (long long )d1) - (long
        long )d2 >= 0LL) && (2147483499LL - (long long )d1old) - (long long )x >=
        0LL) && (2147483500LL - (long long )d2) - (long long )x >= 0LL) && (2147483501LL
        - (long long )d1) - (long long )x >= 0LL) && d1 == 77) && d2 == 76) && d1old
        == 75)) || ((((((((((((((((((((((((-75 <= x && x <= 2147483499) && (-151LL
        + (long long )d1) + (long long )d2 >= 0LL) && (-151LL + (long long )d1old)
        + (long long )d2 >= 0LL) && (-150LL + (long long )d1) + (long long )d1old
        >= 0LL) && (-1LL - (long long )d1) + (long long )d2 >= 0LL) && (0LL - (long
        long )d1) + (long long )d1old >= 0LL) && (150LL - (long long )d1) + (long
        long )x >= 0LL) && (150LL - (long long )d1old) + (long long )x >= 0LL) &&
        (151LL - (long long )d2) + (long long )x >= 0LL) && (long long )d1 + (long
        long )x >= 0LL) && (1LL + (long long )d1) - (long long )d2 >= 0LL) && (2147483423LL
        + (long long )d2) - (long long )x >= 0LL) && (2147483424LL + (long long )d1)
        - (long long )x >= 0LL) && (2147483424LL + (long long )d1old) - (long long
        )x >= 0LL) && (150LL - (long long )d1) - (long long )d1old >= 0LL) && (151LL
        - (long long )d1) - (long long )d2 >= 0LL) && (151LL - (long long )d1old)
        - (long long )d2 >= 0LL) && (2147483574LL - (long long )d1) - (long long )x
        >= 0LL) && (2147483574LL - (long long )d1old) - (long long )x >= 0LL) && (2147483575LL
        - (long long )d2) - (long long )x >= 0LL) && (long long )d1 - (long long )d1old
        >= 0LL) && d1 == 75) && d2 == 76) && d1old == 75)) || (((((((((((((((((((((((((-73
        <= x && x <= 2147483574) && (-149LL + (long long )d1) + (long long )d2 >=
        0LL) && (-148LL + (long long )d1) + (long long )d1old >= 0LL) && (-147LL +
        (long long )d1old) + (long long )d2 >= 0LL) && (-2LL + (long long )d1) + (long
        long )x >= 0LL) && (1LL - (long long )d1) + (long long )d2 >= 0LL) && (2LL
        - (long long )d1) + (long long )d1old >= 0LL) && (146LL - (long long )d1old)
        + (long long )x >= 0LL) && (147LL - (long long )d2) + (long long )x >= 0LL)
        && (148LL - (long long )d1) + (long long )x >= 0LL) && (-2LL + (long long
        )d1) - (long long )d1old >= 0LL) && (-1LL + (long long )d1) - (long long )d2
        >= 0LL) && (2147483499LL + (long long )d1) - (long long )x >= 0LL) && (2147483500LL
        + (long long )d2) - (long long )x >= 0LL) && (2147483501LL + (long long )d1old)
        - (long long )x >= 0LL) && (147LL - (long long )d1old) - (long long )d2 >=
        0LL) && (148LL - (long long )d1) - (long long )d1old >= 0LL) && (149LL - (long
        long )d1) - (long long )d2 >= 0LL) && (2147483647LL - (long long )d1old) -
        (long long )x >= 0LL) && (2147483648LL - (long long )d2) - (long long )x >=
        0LL) && (2147483649LL - (long long )d1) - (long long )x >= 0LL) && 73 == d1old)
        && d1 == 75) && d2 == 74) && d1old == 73))) || ((((((((((((((((((((((((((((-147LL
        + (long long )d1) + (long long )d2 >= 0LL && (2147483574LL + (long long )d2)
        + (long long )x >= 0LL) && (2147483574LL + (long long )d1old) + (long long
        )d2 >= 0LL) && (2147483575LL + (long long )d1) + (long long )x >= 0LL) &&
        (2147483575LL + (long long )d1) + (long long )d1old >= 0LL) && (4294967296LL
        + (long long )d1old) + (long long )x >= 0LL) && (-1LL - (long long )d1) +
        (long long )d2 >= 0LL) && (2147483573LL - (long long )d1old) + (long long
        )d2 >= 0LL) && (2147483721LL - (long long )d1) + (long long )x >= 0LL) &&
        (2147483721LL - (long long )d1) + (long long )d1old >= 0LL) && (2147483722LL
        - (long long )d2) + (long long )x >= 0LL) && (4294967295LL - (long long )d1old)
        + (long long )x >= 0LL) && (1LL + (long long )d1) - (long long )d2 >= 0LL)
        && (2147483573LL + (long long )d2) - (long long )x >= 0LL) && (2147483574LL
        + (long long )d1) - (long long )x >= 0LL) && (2147483574LL + (long long )d1)
        - (long long )d1old >= 0LL) && (2147483722LL + (long long )d1old) - (long
        long )d2 >= 0LL) && (4294967295LL + (long long )d1old) - (long long )x >=
        0LL) && (147LL - (long long )d1) - (long long )d2 >= 0LL) && (2147483720LL
        - (long long )d1) - (long long )x >= 0LL) && (2147483720LL - (long long )d1)
        - (long long )d1old >= 0LL) && (2147483721LL - (long long )d2) - (long long
        )x >= 0LL) && (2147483721LL - (long long )d1old) - (long long )d2 >= 0LL)
        && (4294967294LL - (long long )d1old) - (long long )x >= 0LL) && 73 == d1)
        && 74 == d2) && d1 == 73) && d2 == 74)
      format: c_expression
