- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 677a0806-9bc9-4ebb-95c9-6ef9ce8ecd03
    creation_time: 2025-03-21T01:25:39Z
    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'' ''64bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-crafted/4NestedWith3Variables-1.c'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-crafted/4NestedWith3Variables-1.c
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/termination-crafted/4NestedWith3Variables-1.c: b39ec4b52f8da315ff57d8e97152c727a55203720ed4bc216d0daa6b94e35d48
      data_model: LP64
      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/termination-crafted/4NestedWith3Variables-1.c
        line: 26
        column: 2
        function: main
      value: ((0LL - (long long )olda) + (long long )q >= 0LL && ((((((((((((((((((((((((((q
        <= 2147483646 && (4294967296LL + (long long )a) + (long long )b >= 0LL) &&
        (4294967296LL + (long long )a) + (long long )q >= 0LL) && (4294967296LL +
        (long long )a) + (long long )olda >= 0LL) && (4294967296LL + (long long )b)
        + (long long )q >= 0LL) && (4294967296LL + (long long )b) + (long long )olda
        >= 0LL) && (4294967296LL + (long long )olda) + (long long )q >= 0LL) && (4294967296LL
        - (long long )a) + (long long )b >= 0LL) && (4294967296LL - (long long )a)
        + (long long )q >= 0LL) && (4294967296LL - (long long )a) + (long long )olda
        >= 0LL) && (4294967296LL - (long long )b) + (long long )q >= 0LL) && (4294967296LL
        - (long long )b) + (long long )olda >= 0LL) && (4294967296LL + (long long
        )a) - (long long )b >= 0LL) && (4294967296LL + (long long )a) - (long long
        )q >= 0LL) && (4294967296LL + (long long )a) - (long long )olda >= 0LL) &&
        (4294967296LL + (long long )b) - (long long )q >= 0LL) && (4294967296LL +
        (long long )b) - (long long )olda >= 0LL) && (4294967296LL + (long long )olda)
        - (long long )q >= 0LL) && (4294967296LL - (long long )a) - (long long )b
        >= 0LL) && (4294967296LL - (long long )a) - (long long )q >= 0LL) && (4294967296LL
        - (long long )a) - (long long )olda >= 0LL) && (4294967296LL - (long long
        )b) - (long long )q >= 0LL) && (4294967296LL - (long long )b) - (long long
        )olda >= 0LL) && (4294967296LL - (long long )olda) - (long long )q >= 0LL)
        || ((((((((((((((((((((((((((((((-169868967 <= a && -161480323 <= b) && -23068621
        <= q) && -23068621 <= olda) && a <= 167771759) && b <= 176160404) && q <=
        29360063) && olda <= 25165769) && (46137242LL + (long long )olda) + (long
        long )q >= 0LL) && (182451800LL + (long long )b) + (long long )q >= 0LL) &&
        (182451800LL + (long long )b) + (long long )olda >= 0LL) && (188743295LL +
        (long long )a) + (long long )q >= 0LL) && (188743295LL + (long long )a) +
        (long long )olda >= 0LL) && (283114901LL + (long long )a) + (long long )b
        >= 0LL) && (142605990LL - (long long )a) + (long long )q >= 0LL) && (142605990LL
        - (long long )a) + (long long )olda >= 0LL) && (150994635LL - (long long )b)
        + (long long )q >= 0LL) && (150994635LL - (long long )b) + (long long )olda
        >= 0LL) && (281017692LL - (long long )a) + (long long )b >= 0LL) && (4718580LL
        + (long long )olda) - (long long )q >= 0LL) && (138411702LL + (long long )b)
        - (long long )olda >= 0LL) && (143130282LL + (long long )b) - (long long )q
        >= 0LL) && (146800346LL + (long long )a) - (long long )olda >= 0LL) && (151518926LL
        + (long long )a) - (long long )q >= 0LL) && (297794981LL + (long long )a)
        - (long long )b >= 0LL) && (54525832LL - (long long )olda) - (long long )q
        >= 0LL) && (188743234LL - (long long )a) - (long long )olda >= 0LL) && (192937528LL
        - (long long )a) - (long long )q >= 0LL) && (195034730LL - (long long )b)
        - (long long )olda >= 0LL) && (199753310LL - (long long )b) - (long long )q
        >= 0LL) && (295697774LL - (long long )a) - (long long )b >= 0LL)) || ((((((((((((((((((((((((((((((-25690057
        <= a && -25690049 <= b) && -3670007 <= q) && -3670007 <= olda) && a <= 25690055)
        && b <= 25690063) && q <= 4718581) && olda <= 3670009) && (7340014LL + (long
        long )olda) + (long long )q >= 0LL) && (28311486LL + (long long )b) + (long
        long )q >= 0LL) && (28311486LL + (long long )b) + (long long )olda >= 0LL)
        && (28311492LL + (long long )a) + (long long )q >= 0LL) && (28311492LL + (long
        long )a) + (long long )olda >= 0LL) && (44040090LL + (long long )a) + (long
        long )b >= 0LL) && (22020046LL - (long long )a) + (long long )q >= 0LL) &&
        (22020046LL - (long long )a) + (long long )olda >= 0LL) && (22020054LL - (long
        long )b) + (long long )q >= 0LL) && (22020054LL - (long long )b) + (long long
        )olda >= 0LL) && (44040088LL - (long long )a) + (long long )b >= 0LL) && (1048572LL
        + (long long )olda) - (long long )q >= 0LL) && (22020042LL + (long long )b)
        - (long long )olda >= 0LL) && (22020050LL + (long long )a) - (long long )olda
        >= 0LL) && (23068614LL + (long long )b) - (long long )q >= 0LL) && (23068622LL
        + (long long )a) - (long long )q >= 0LL) && (44040104LL + (long long )a) -
        (long long )b >= 0LL) && (8388590LL - (long long )olda) - (long long )q >=
        0LL) && (28311492LL - (long long )a) - (long long )olda >= 0LL) && (28311498LL
        - (long long )b) - (long long )olda >= 0LL) && (29360064LL - (long long )a)
        - (long long )q >= 0LL) && (29360070LL - (long long )b) - (long long )q >=
        0LL) && (44040102LL - (long long )a) - (long long )b >= 0LL)) || ((((((((((((((((((((((((((((((-3670009
        <= a && -3670009 <= b) && -524287 <= q) && -524287 <= olda) && a <= 3670009)
        && b <= 3670009) && q <= 1048573) && olda <= 524287) && (1048574LL + (long
        long )olda) + (long long )q >= 0LL) && (4194296LL + (long long )a) + (long
        long )q >= 0LL) && (4194296LL + (long long )a) + (long long )olda >= 0LL)
        && (4194296LL + (long long )b) + (long long )q >= 0LL) && (4194296LL + (long
        long )b) + (long long )olda >= 0LL) && (6291444LL + (long long )a) + (long
        long )b >= 0LL) && (3145722LL - (long long )a) + (long long )q >= 0LL) &&
        (3145722LL - (long long )a) + (long long )olda >= 0LL) && (3145722LL - (long
        long )b) + (long long )q >= 0LL) && (3145722LL - (long long )b) + (long long
        )olda >= 0LL) && (6291444LL - (long long )a) + (long long )b >= 0LL) && (524286LL
        + (long long )olda) - (long long )q >= 0LL) && (3145722LL + (long long )a)
        - (long long )olda >= 0LL) && (3145722LL + (long long )b) - (long long )olda
        >= 0LL) && (3670008LL + (long long )a) - (long long )q >= 0LL) && (3670008LL
        + (long long )b) - (long long )q >= 0LL) && (6291444LL + (long long )a) -
        (long long )b >= 0LL) && (1572860LL - (long long )olda) - (long long )q >=
        0LL) && (4194296LL - (long long )a) - (long long )olda >= 0LL) && (4194296LL
        - (long long )b) - (long long )olda >= 0LL) && (4718582LL - (long long )a)
        - (long long )q >= 0LL) && (4718582LL - (long long )b) - (long long )q >=
        0LL) && (6291444LL - (long long )a) - (long long )b >= 0LL))) || (((((((((((((((((((((((((((((-524287
        <= a && -524287 <= b) && -524287 <= q) && a <= 524287) && b <= 524287) &&
        q <= 524287) && (1048574LL + (long long )a) + (long long )b >= 0LL) && (1048574LL
        + (long long )a) + (long long )q >= 0LL) && (1048574LL + (long long )b) +
        (long long )q >= 0LL) && (2148007935LL + (long long )a) + (long long )olda
        >= 0LL) && (2148007935LL + (long long )b) + (long long )olda >= 0LL) && (2148007935LL
        + (long long )olda) + (long long )q >= 0LL) && (1048574LL - (long long )a)
        + (long long )b >= 0LL) && (1048574LL - (long long )a) + (long long )q >=
        0LL) && (1048574LL - (long long )b) + (long long )q >= 0LL) && (2148007934LL
        - (long long )olda) + (long long )q >= 0LL) && (2148007935LL - (long long
        )a) + (long long )olda >= 0LL) && (2148007935LL - (long long )b) + (long long
        )olda >= 0LL) && (1048574LL + (long long )a) - (long long )b >= 0LL) && (1048574LL
        + (long long )a) - (long long )q >= 0LL) && (1048574LL + (long long )b) -
        (long long )q >= 0LL) && (2148007934LL + (long long )a) - (long long )olda
        >= 0LL) && (2148007934LL + (long long )b) - (long long )olda >= 0LL) && (2148007935LL
        + (long long )olda) - (long long )q >= 0LL) && (1048574LL - (long long )a)
        - (long long )b >= 0LL) && (1048574LL - (long long )a) - (long long )q >=
        0LL) && (1048574LL - (long long )b) - (long long )q >= 0LL) && (2148007934LL
        - (long long )a) - (long long )olda >= 0LL) && (2148007934LL - (long long
        )b) - (long long )olda >= 0LL) && (2148007934LL - (long long )olda) - (long
        long )q >= 0LL)
      format: c_expression
