- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 47dc6d3e-99b1-44e6-9b58-09a145df84f4
    creation_time: 2023-01-27T15:24:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 23
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a871c7f4-87db-4edc-b460-aec9e9ec35d2
    creation_time: 2023-01-27T15:24:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 23
    column: 8
    function: main
  loop_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: de278981-3213-4bec-82f3-b2b521d2f209
    creation_time: 2023-01-27T15:24:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 23
    column: 8
    function: main
  loop_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 794dc350-e80c-42b3-a9b4-a72b222f9901
    creation_time: 2023-01-27T15:24:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 29
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e1775959-1261-45b7-b179-bc502b2b408f
    creation_time: 2023-01-27T15:24:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 29
    column: 8
    function: main
  loop_invariant:
    string: (long long )n - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e85d797-366c-4057-8689-3aef80e8e358
    creation_time: 2023-01-27T15:24:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 29
    column: 8
    function: main
  loop_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ddc94c5d-2068-489b-98bd-d0f56206c92c
    creation_time: 2023-01-27T15:24:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 35
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b5f4837-0871-4ae0-b4a0-a056c2824442
    creation_time: 2023-01-27T15:24:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 35
    column: 8
    function: main
  loop_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4044f175-ae6d-4ceb-9899-1aea3b497e0a
    creation_time: 2023-01-27T15:24:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 35
    column: 8
    function: main
  loop_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 83651457-6073-4291-9d2e-c6cbde7bc3dd
    creation_time: 2023-01-27T15:24:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 41
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fbd536ce-8271-4533-81d1-e00e4136f93f
    creation_time: 2023-01-27T15:24:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 41
    column: 8
    function: main
  loop_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c6b5872-1e89-4582-9b8f-7509cf198075
    creation_time: 2023-01-27T15:24:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 41
    column: 8
    function: main
  loop_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 91cacec0-5128-4e23-8d81-1668a7bd2e35
    creation_time: 2023-01-27T15:24:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9054e3af-915b-4724-adfc-238ac2724ccc
    creation_time: 2023-01-27T15:24:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c18f8489-2cfe-451c-b663-151dbc49813d
    creation_time: 2023-01-27T15:24:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 658260d6-7775-4306-b4da-2fe959f1196e
    creation_time: 2023-01-27T15:24:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f9625b92-0ca3-4722-ab0c-ac2c52c9fe99
    creation_time: 2023-01-27T15:24:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set''
        ''ana.apron.domain'' ''polyhedra'' ''--enable'' ''witness.invariant.loop-head''
        ''--disable'' ''witness.invariant.other'' ''--disable'' ''witness.invariant.accessed''
        ''--sets'' ''ana.specification'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
