- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1f4c9f14-7255-4fd0-9ddb-1169cf624ec0
    creation_time: 2023-01-27T15:24:31Z
    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/nested_delay_nd.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      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/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 25
    column: 7
    function: main
  loop_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e7b7d527-f718-4697-adf3-cbc50324dd20
    creation_time: 2023-01-27T15:24:31Z
    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/nested_delay_nd.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      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/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 25
    column: 7
    function: main
  loop_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0959252c-8f0b-472c-b275-a3cb08dcae07
    creation_time: 2023-01-27T15:24:31Z
    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/nested_delay_nd.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      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/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 25
    column: 7
    function: main
  loop_invariant:
    string: 0 <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 91d0bac1-4dcc-4ca7-97bc-5270d5c4e6db
    creation_time: 2023-01-27T15:24:31Z
    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/nested_delay_nd.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      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/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 25
    column: 7
    function: main
  loop_invariant:
    string: 0 <= st
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e738c42-ec95-4a41-b0fa-8ae4f3cee3c4
    creation_time: 2023-01-27T15:24:31Z
    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/nested_delay_nd.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      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/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 25
    column: 7
    function: main
  loop_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 90c21568-252e-46c5-a5a3-e38585d25563
    creation_time: 2023-01-27T15:24:31Z
    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/nested_delay_nd.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      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/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 25
    column: 7
    function: main
  loop_invariant:
    string: c <= 200000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ce5686c-5555-47f7-8d82-df000e948fbb
    creation_time: 2023-01-27T15:24:31Z
    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/nested_delay_nd.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      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/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 25
    column: 7
    function: main
  loop_invariant:
    string: st <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c80826d-f7c6-4beb-a7cc-2394aa7b573e
    creation_time: 2023-01-27T15:24:31Z
    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/nested_delay_nd.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      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/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 25
    column: 7
    function: main
  loop_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7cb678f2-8aa2-4c19-9624-4c9040168948
    creation_time: 2023-01-27T15:24:31Z
    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/nested_delay_nd.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      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/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a9924b4-f3f7-4436-9ef9-88bc8ff46b01
    creation_time: 2023-01-27T15:24:31Z
    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/nested_delay_nd.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      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/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: 0 <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a8073461-6593-4c4e-8e90-5aa42eb725ae
    creation_time: 2023-01-27T15:24:31Z
    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/nested_delay_nd.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      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/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: 0 <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fd102293-346b-4546-a301-40287346c845
    creation_time: 2023-01-27T15:24:31Z
    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/nested_delay_nd.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      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/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: 0 <= st
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 491bbc60-dc81-40ed-a548-21d68603d72e
    creation_time: 2023-01-27T15:24:31Z
    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/nested_delay_nd.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      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/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: 0 <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b149a3b-0f8e-49a2-9e6c-6ab4d5ff4db2
    creation_time: 2023-01-27T15:24:31Z
    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/nested_delay_nd.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      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/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: c <= 200000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ea0e2253-0445-4a9e-a347-f579f9107e1c
    creation_time: 2023-01-27T15:24:31Z
    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/nested_delay_nd.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      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/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: st <= 1
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 94bb8e71-85ba-4f0d-b5ee-8234ed57a054
    creation_time: 2023-01-27T15:24:31Z
    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/nested_delay_nd.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      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/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: (-1LL + (long long )c) + (long long )st >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f6c3ef13-2d62-4738-b209-77eb152deb91
    creation_time: 2023-01-27T15:24:31Z
    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/nested_delay_nd.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      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/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: 1LL - (long long )st >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 46934974-6677-4184-b3b7-4a600fd4b42e
    creation_time: 2023-01-27T15:24:31Z
    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/nested_delay_nd.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      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/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: 200000LL - (long long )c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cdc56fc1-1283-4958-a7a9-a58bf39c1ec5
    creation_time: 2023-01-27T15:24:31Z
    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/nested_delay_nd.c'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c
      input_file_hashes:
        /mnt/thread-witnesses/replication/sv-benchmarks/c/loops-crafted-1/nested_delay_nd.c: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
      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/nested_delay_nd.c
    file_hash: 39463d01f5c85d47bf5e231172595e96b8ff556c59c4a9ab8cf46a88a393b05c
    line: 27
    column: 5
    function: main
  loop_invariant:
    string: (long long )d >= 0LL
    type: assertion
    format: C
