- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b8d3da91-e285-437d-99e4-bd162358ac60
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 29
    column: 12
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 94331ff6-b39f-4e36-b4cf-bcd95eee5f0b
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 29
    column: 12
    function: main
  location_invariant:
    string: (long long )x - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8c842b1c-32b5-4b26-b5e2-bfea184330cf
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 30
    column: 12
    function: main
  location_invariant:
    string: 0 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d178cb68-77b5-47ef-812b-026817283dc2
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 30
    column: 12
    function: main
  location_invariant:
    string: y <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 374df30d-9f91-4860-8ba6-ab3103b3c5a0
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 30
    column: 12
    function: main
  location_invariant:
    string: 49LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 28f2e1b2-62ef-49f9-a04d-0d383c523284
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 30
    column: 12
    function: main
  location_invariant:
    string: (long long )x - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98613966-f7bb-4fd1-bf79-aaf5f62e9752
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 32
    column: 12
    function: main
  location_invariant:
    string: 0 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f5229966-a2c3-44ee-9c69-7f880ecd7cf4
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 32
    column: 12
    function: main
  location_invariant:
    string: y <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 67c6e9c5-4d61-4091-9755-5deb50793d9a
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 32
    column: 12
    function: main
  location_invariant:
    string: -50LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b46a9b8c-e097-4145-b1a5-4dc0f3d7dc4a
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 32
    column: 12
    function: main
  location_invariant:
    string: (long long )x - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3413714-356c-43c4-8171-b24cdf1a88ec
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 34
    column: 12
    function: main
  location_invariant:
    string: -1 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 677444c0-d467-4923-b347-ad037165df9c
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 34
    column: 12
    function: main
  location_invariant:
    string: y <= 2147483645
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8b75f91-15d9-4792-a4c6-78a2d8983502
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 34
    column: 12
    function: main
  location_invariant:
    string: (1LL + (long long )x) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 34d797f6-544e-48a2-aa84-83d682c2b2dd
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 516dc4ca-3d9f-42b4-a179-63fc6c851913
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 35
    column: 8
    function: main
  location_invariant:
    string: (1LL + (long long )x) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ae70cc5-092d-47f1-9d86-4368a8008294
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 35
    column: 8
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 063d71a1-a426-44fd-a382-79eaad047663
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 37
    column: 4
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 144e42d8-6b00-448e-994e-12123edc9fc3
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 37
    column: 4
    function: main
  location_invariant:
    string: -1LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d2bf5044-5a23-4a71-a47f-5821d54519cd
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 37
    column: 4
    function: main
  location_invariant:
    string: (1LL + (long long )x) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9fc80e09-25f9-4890-9faa-ab86d5fc061d
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 38
    column: 4
    function: main
  location_invariant:
    string: -1LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 65486ad5-4d5c-4227-a3e3-ec8c6d3bd0b7
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 38
    column: 4
    function: main
  location_invariant:
    string: (1LL + (long long )x) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ff541e8f-1c79-4389-887b-df37665ef694
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 28
    column: 11
    function: main
  loop_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e70886d2-11d9-4fdb-97eb-d30cf4debf4a
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 28
    column: 11
    function: main
  loop_invariant:
    string: 0 <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 481bbba6-631b-4d58-9832-793827ab4140
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 28
    column: 11
    function: main
  loop_invariant:
    string: y <= 2147483646
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c79a69c4-149f-49fb-94de-a637021bd4b2
    creation_time: 2023-01-27T16:29:32Z
    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/gr2006.i'''
    task:
      input_files:
      - ../plain/gr2006.i
      input_file_hashes:
        ../plain/gr2006.i: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/gr2006.i
    file_hash: 3ef045eb54c58e8ecfe4972142a43378e1f3b08091dc3d5b7e399cf5703f1724
    line: 28
    column: 11
    function: main
  loop_invariant:
    string: (long long )x - (long long )y >= 0LL
    type: assertion
    format: C
