- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 1b80a8fd-21fb-46f0-ab98-426850174083
    creation_time: 2025-03-20T23:30:59Z
    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-realloc/array-realloc-3.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety-realloc/array-realloc-3.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety-realloc/array-realloc-3.i: 165c3d31baf6e9e6eb3241886fc1e2aed511e6788979a2e699609d2c8b9e748b
      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-realloc/array-realloc-3.i
        line: 516
        column: 3
        function: expandArray
      value: num <= 99
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety-realloc/array-realloc-3.i
        line: 516
        column: 3
        function: expandArray
      value: ind == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety-realloc/array-realloc-3.i
        line: 516
        column: 3
        function: expandArray
      value: i == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-memsafety-realloc/array-realloc-3.i
        line: 516
        column: 3
        function: expandArray
      value: (((0LL - (long long )newsize) + (long long )num >= 0LL && a == b) &&
        ((((((((((((((10 <= num && 10 <= newsize) && newsize <= 99) && (-20LL + (long
        long )newsize) + (long long )num >= 0LL) && (89LL + (long long )newsize) -
        (long long )num >= 0LL) && (198LL - (long long )newsize) - (long long )num
        >= 0LL) || ((((9 <= num && (-18LL + (long long )newsize) + (long long )num
        >= 0LL) && (90LL + (long long )newsize) - (long long )num >= 0LL) && (108LL
        - (long long )newsize) - (long long )num >= 0LL) && newsize == 9)) || ((((8
        <= num && (-16LL + (long long )newsize) + (long long )num >= 0LL) && (91LL
        + (long long )newsize) - (long long )num >= 0LL) && (107LL - (long long )newsize)
        - (long long )num >= 0LL) && newsize == 8)) || ((((7 <= num && (-14LL + (long
        long )newsize) + (long long )num >= 0LL) && (92LL + (long long )newsize) -
        (long long )num >= 0LL) && (106LL - (long long )newsize) - (long long )num
        >= 0LL) && newsize == 7)) || ((((6 <= num && (-12LL + (long long )newsize)
        + (long long )num >= 0LL) && (93LL + (long long )newsize) - (long long )num
        >= 0LL) && (105LL - (long long )newsize) - (long long )num >= 0LL) && newsize
        == 6)) || ((((5 <= num && (-10LL + (long long )newsize) + (long long )num
        >= 0LL) && (94LL + (long long )newsize) - (long long )num >= 0LL) && (104LL
        - (long long )newsize) - (long long )num >= 0LL) && newsize == 5)) || ((((4
        <= num && (-8LL + (long long )newsize) + (long long )num >= 0LL) && (95LL
        + (long long )newsize) - (long long )num >= 0LL) && (103LL - (long long )newsize)
        - (long long )num >= 0LL) && newsize == 4)) || ((((3 <= num && (-6LL + (long
        long )newsize) + (long long )num >= 0LL) && (96LL + (long long )newsize) -
        (long long )num >= 0LL) && (102LL - (long long )newsize) - (long long )num
        >= 0LL) && newsize == 3)) || ((((2 <= num && (-4LL + (long long )newsize)
        + (long long )num >= 0LL) && (97LL + (long long )newsize) - (long long )num
        >= 0LL) && (101LL - (long long )newsize) - (long long )num >= 0LL) && newsize
        == 2)) || ((((1 <= num && (-2LL + (long long )newsize) + (long long )num >=
        0LL) && (98LL + (long long )newsize) - (long long )num >= 0LL) && (100LL -
        (long long )newsize) - (long long )num >= 0LL) && newsize == 1))) || ((((((1
        <= num && (-1LL + (long long )newsize) + (long long )num >= 0LL) && (-1LL
        - (long long )newsize) + (long long )num >= 0LL) && (99LL + (long long )newsize)
        - (long long )num >= 0LL) && (99LL - (long long )newsize) - (long long )num
        >= 0LL) && newsize == 0) && arg == a)
      format: c_expression
