- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b01ccb0e-8c37-44ff-a979-95f89fe8a240
    creation_time: 2023-01-27T16:31:09Z
    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/underapprox_2-2.c'''
    task:
      input_files:
      - ../plain/underapprox_2-2.c
      input_file_hashes:
        ../plain/underapprox_2-2.c: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/underapprox_2-2.c
    file_hash: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
    line: 21
    column: 2
    function: main
  location_invariant:
    string: -6LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d3bd841-a0aa-4107-b9bc-c7220d767531
    creation_time: 2023-01-27T16:31:09Z
    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/underapprox_2-2.c'''
    task:
      input_files:
      - ../plain/underapprox_2-2.c
      input_file_hashes:
        ../plain/underapprox_2-2.c: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/underapprox_2-2.c
    file_hash: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
    line: 22
    column: 0
    function: main
  location_invariant:
    string: -6LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97315657-f3d0-49db-a1f2-e1446cdf51cd
    creation_time: 2023-01-27T16:31:09Z
    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/underapprox_2-2.c'''
    task:
      input_files:
      - ../plain/underapprox_2-2.c
      input_file_hashes:
        ../plain/underapprox_2-2.c: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/underapprox_2-2.c
    file_hash: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
    line: 13
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fad78db4-f37c-4fb3-bb9b-1b57a12689e7
    creation_time: 2023-01-27T16:31:09Z
    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/underapprox_2-2.c'''
    task:
      input_files:
      - ../plain/underapprox_2-2.c
      input_file_hashes:
        ../plain/underapprox_2-2.c: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/underapprox_2-2.c
    file_hash: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
    line: 13
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e7e68e07-9935-4c0f-b68d-a90ea77acf88
    creation_time: 2023-01-27T16:31:09Z
    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/underapprox_2-2.c'''
    task:
      input_files:
      - ../plain/underapprox_2-2.c
      input_file_hashes:
        ../plain/underapprox_2-2.c: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/underapprox_2-2.c
    file_hash: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
    line: 13
    column: 15
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10373bc0-9ebf-449b-a831-4a5aee085cba
    creation_time: 2023-01-27T16:31:09Z
    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/underapprox_2-2.c'''
    task:
      input_files:
      - ../plain/underapprox_2-2.c
      input_file_hashes:
        ../plain/underapprox_2-2.c: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/underapprox_2-2.c
    file_hash: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
    line: 13
    column: 15
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce3cffcc-3818-46de-983d-6fc38c6c64f7
    creation_time: 2023-01-27T16:31:09Z
    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/underapprox_2-2.c'''
    task:
      input_files:
      - ../plain/underapprox_2-2.c
      input_file_hashes:
        ../plain/underapprox_2-2.c: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/underapprox_2-2.c
    file_hash: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
    line: 14
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5fa98534-d3e2-4b4e-b95e-26af05803f6a
    creation_time: 2023-01-27T16:31:09Z
    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/underapprox_2-2.c'''
    task:
      input_files:
      - ../plain/underapprox_2-2.c
      input_file_hashes:
        ../plain/underapprox_2-2.c: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/underapprox_2-2.c
    file_hash: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
    line: 14
    column: 15
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 556eb44d-3f33-4127-b8e2-a2b102507dc8
    creation_time: 2023-01-27T16:31:09Z
    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/underapprox_2-2.c'''
    task:
      input_files:
      - ../plain/underapprox_2-2.c
      input_file_hashes:
        ../plain/underapprox_2-2.c: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/underapprox_2-2.c
    file_hash: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
    line: 17
    column: 4
    function: main
  location_invariant:
    string: x <= 5U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d4857dd-c48a-41d1-a438-2b5d376aac40
    creation_time: 2023-01-27T16:31:09Z
    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/underapprox_2-2.c'''
    task:
      input_files:
      - ../plain/underapprox_2-2.c
      input_file_hashes:
        ../plain/underapprox_2-2.c: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/underapprox_2-2.c
    file_hash: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
    line: 17
    column: 4
    function: main
  location_invariant:
    string: 5LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da786946-d2fa-493e-8b37-108d12b5a95a
    creation_time: 2023-01-27T16:31:09Z
    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/underapprox_2-2.c'''
    task:
      input_files:
      - ../plain/underapprox_2-2.c
      input_file_hashes:
        ../plain/underapprox_2-2.c: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/underapprox_2-2.c
    file_hash: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
    line: 18
    column: 4
    function: main
  location_invariant:
    string: 1U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ba54d1c-c372-4dab-be18-558cd1320d2f
    creation_time: 2023-01-27T16:31:09Z
    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/underapprox_2-2.c'''
    task:
      input_files:
      - ../plain/underapprox_2-2.c
      input_file_hashes:
        ../plain/underapprox_2-2.c: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/underapprox_2-2.c
    file_hash: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
    line: 18
    column: 4
    function: main
  location_invariant:
    string: x <= 6U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9ff5b617-dda9-42e7-aff4-dfff4ae52fbe
    creation_time: 2023-01-27T16:31:09Z
    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/underapprox_2-2.c'''
    task:
      input_files:
      - ../plain/underapprox_2-2.c
      input_file_hashes:
        ../plain/underapprox_2-2.c: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/underapprox_2-2.c
    file_hash: c187a61b21cc0091fb22a1c4e23554540f928674895dd149d9c60db42e5420c7
    line: 16
    column: 9
    function: main
  loop_invariant:
    string: x <= 6U
    type: assertion
    format: C
