- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b65147b1-51e4-4aac-8f45-20e44bd47192
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 30
    column: 6
    function: main
  location_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 83af6196-e2aa-46fa-8eef-92590b8d5b44
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 30
    column: 6
    function: main
  location_invariant:
    string: i <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 167a508d-a96e-4fc7-b174-be41feeb837e
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 30
    column: 6
    function: main
  location_invariant:
    string: (-1LL - (long long )i) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3dfd7c89-359d-4dfc-b8af-9f46450ca8c8
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 30
    column: 6
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e0d0948c-c444-430b-b84b-d5a771baf020
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 31
    column: 6
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 162e9f2a-03c3-41e1-b7a4-9fcbd3ebd5bc
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 31
    column: 6
    function: main
  location_invariant:
    string: 1 <= i
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b7b9dbc-b0d3-4497-954d-9dc7f97d5b91
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 31
    column: 6
    function: main
  location_invariant:
    string: -1LL + (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e71bb75c-0236-4463-a499-bb0b47577b54
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 31
    column: 6
    function: main
  location_invariant:
    string: (0LL - (long long )i) + (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5fc5ffa4-a714-4706-837b-12553737f2cb
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 33
    column: 6
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 431a7a95-9900-42f0-b065-4ee818e5f326
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 33
    column: 6
    function: main
  location_invariant:
    string: (long long )i - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f4fe8cb2-d469-452f-b85a-e63186a6d6ee
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 33
    column: 6
    function: main
  location_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93721ec2-7f83-48d5-8048-e3e0f0734066
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 35
    column: 6
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f6c75b8-5d48-4eb9-93a0-66de582a223e
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 35
    column: 6
    function: main
  location_invariant:
    string: -1LL + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a0b9e79-c525-493b-9577-f4bd97a791c5
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 35
    column: 6
    function: main
  location_invariant:
    string: (0LL - (long long )j) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a8517af6-fa9c-4584-af57-b463c01e1100
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 35
    column: 6
    function: main
  location_invariant:
    string: (long long )i - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d49ca8e0-debe-41ac-bae4-d593d708e339
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 36
    column: 6
    function: main
  location_invariant:
    string: 1 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f354cc26-0250-42ac-bd79-09072ed20b43
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 36
    column: 6
    function: main
  location_invariant:
    string: -1LL + (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fe694e51-23f2-465f-becd-20a042613582
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 36
    column: 6
    function: main
  location_invariant:
    string: (0LL - (long long )j) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3b828fad-6eab-4529-a3f7-03cfe7bd56ad
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 36
    column: 6
    function: main
  location_invariant:
    string: (long long )i - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76033929-b3b2-4580-bc40-388aae2ba563
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 36
    column: 6
    function: main
  location_invariant:
    string: j != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d5dfd33c-eb7a-4bde-8560-eb82709947e7
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 37
    column: 6
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fdfe1684-7112-4f13-aa39-a5e26a7c5dc6
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 37
    column: 6
    function: main
  location_invariant:
    string: 0 <= j
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75acdac9-d44f-45fb-a34a-33a36a7d5f94
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 37
    column: 6
    function: main
  location_invariant:
    string: j <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 52af2fa5-c796-4f01-9ac4-5836264bcf80
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 37
    column: 6
    function: main
  location_invariant:
    string: (-1LL - (long long )j) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a28d5fa0-47b5-43de-abe5-9fdc8eab61ad
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 37
    column: 6
    function: main
  location_invariant:
    string: (long long )i - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 12ffa172-fed5-47bc-b50a-67ff0057a9ae
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 37
    column: 6
    function: main
  location_invariant:
    string: (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d0064cd-be92-46ed-a6cf-506d38f463aa
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 37
    column: 6
    function: main
  location_invariant:
    string: j != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 443c1834-0167-4f36-bceb-1b1b6777fead
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 39
    column: 2
    function: main
  location_invariant:
    string: 0LL - (long long )j >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b3008c7-cfcc-4d09-83a2-70a78d94d3ec
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 39
    column: 2
    function: main
  location_invariant:
    string: (long long )i - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d163af9-1ddb-45dd-a2be-9ac9ab1691d3
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 39
    column: 2
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e84d3cd-4012-4f3e-9f88-ed6d94cb89f2
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 29
    column: 9
    function: main
  loop_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 408deb3b-ea1c-404e-8d5f-c1487b0052e8
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 29
    column: 9
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a4adcc08-7276-49d3-b1f7-37d43acdb1fe
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 29
    column: 9
    function: main
  loop_invariant:
    string: (long long )i >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d956300f-1168-4a1e-924c-9aec559972fb
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 34
    column: 9
    function: main
  loop_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 405d6615-f89e-43d3-a893-2547c8bb7d0e
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 34
    column: 9
    function: main
  loop_invariant:
    string: 0 <= i
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 817a9e3e-5eef-4ec4-a103-7ba04d463459
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 34
    column: 9
    function: main
  loop_invariant:
    string: (0LL - (long long )j) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a1d214af-82a9-4d73-944b-792389442743
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 34
    column: 9
    function: main
  loop_invariant:
    string: (long long )i - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f1f2ca0e-4c7e-4039-96ba-6dc097b5bb25
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/down.i'''
    task:
      input_files:
      - ../plain/down.i
      input_file_hashes:
        ../plain/down.i: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/down.i
    file_hash: d487f6cb836d5c7294168f7ececc6a4515780c0860389f79570a9c0e20e7bcc0
    line: 34
    column: 9
    function: main
  loop_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
