- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 1412c571-9d96-48b5-937d-7d96673e5a50
    creation_time: 2025-03-21T00:29:06Z
    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/memsafety-ext2/optional_data_creation_test04-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memsafety-ext2/optional_data_creation_test04-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memsafety-ext2/optional_data_creation_test04-1.i: 7408f3b7e084094987873e007e2bbb0a022372240d1ad946af6301d3e9707406
      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/memsafety-ext2/optional_data_creation_test04-1.i
        line: 587
        column: 3
        function: main
      value: dataNotFinished == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memsafety-ext2/optional_data_creation_test04-1.i
        line: 557
        column: 5
        function: create_data
      value: (((((((((((((((((((counter == 17 || counter == 16) || counter == 15)
        || counter == 14) || counter == 13) || counter == 12) || counter == 11) ||
        counter == 10) || counter == 9) || counter == 8) || counter == 7) || counter
        == 6) || counter == 5) || counter == 4) || counter == 3) || counter == 2)
        || counter == 1) || (0 == counter && counter == 0)) || counter == 20) || counter
        == 19) || counter == 18
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memsafety-ext2/optional_data_creation_test04-1.i
        line: 584
        column: 3
        function: main
      value: dataNotFinished == 0
      format: c_expression
