- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c4d67c6f-7257-46fc-8930-9932cbf6d46c
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 0 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3998ab6d-0e0a-49a3-9683-6a95ffa9d29a
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 676fd7a5-4e4e-4f57-b985-ae4780830078
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: faf6bc9c-d4a4-4b9a-890d-b48cbb11c04b
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 29
    column: 4
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 05820312-c8e8-4695-820e-6975e2aabb38
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 487ab29c-2643-4c77-a987-c767fadaf084
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 30
    column: 4
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: adf9dbbf-e76b-4244-b42d-9e616a22f395
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 36
    column: 8
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc4ce793-0b5c-4748-a41e-8de71673c69d
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 36
    column: 8
    function: main
  location_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f357651c-44c3-4328-a45f-941a60902bdb
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 36
    column: 8
    function: main
  location_invariant:
    string: q <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a35857f-dd87-4aff-b77d-d44888c30e49
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 36
    column: 8
    function: main
  location_invariant:
    string: r <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc0a486b-6c4c-455b-884a-9be07e80c15d
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 37
    column: 8
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 860f04bc-ec09-4994-8557-dcac52be3467
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 37
    column: 8
    function: main
  location_invariant:
    string: r <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 201d0c16-08e6-4267-886b-d6d92c482a05
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 38
    column: 8
    function: main
  location_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a051a5e-9b35-46de-b190-0aa49e10ea8e
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 38
    column: 8
    function: main
  location_invariant:
    string: q <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a694a084-2c0a-41ba-9d51-77c41aa6f9ab
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 44
    column: 12
    function: main
  location_invariant:
    string: -9223372036854775807LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a5d3c6b-fd6d-4a13-8cec-f078607ff9c0
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 44
    column: 12
    function: main
  location_invariant:
    string: b <= 9223372036854775806LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57c3b95e-318b-4ace-8ff3-13c84476cd03
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 44
    column: 12
    function: main
  location_invariant:
    string: (-1LL + a) - b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a571d2c-f76f-461a-ad1a-a8ffc1fe96e8
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 45
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ebb3caa8-2868-4570-9726-73628249b2ca
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 45
    column: 12
    function: main
  location_invariant:
    string: q <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 135d806f-49dd-4798-8afa-c9e1f09ae079
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 45
    column: 12
    function: main
  location_invariant:
    string: -1LL + a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3dc43e20-7228-4068-88aa-de0fda3acc63
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 46
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c4b69ab3-c988-48ca-a347-09ff6a7152be
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 46
    column: 12
    function: main
  location_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 95d04ef7-afc3-48f4-b088-677e46d2ffab
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 46
    column: 12
    function: main
  location_invariant:
    string: r <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f420ed89-5f03-448f-af62-46dc46f02bc7
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 46
    column: 12
    function: main
  location_invariant:
    string: -1LL + a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d6ed1a38-4f00-456e-b6b9-721ac5835711
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 48
    column: 12
    function: main
  location_invariant:
    string: (0LL - a) + b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e5fcc9f-898a-4323-a59b-545e1570c19c
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 49
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1bd785a3-c1ac-4d35-8d5e-19d80a5e009b
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 49
    column: 12
    function: main
  location_invariant:
    string: q <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c27670f-e825-4c7c-b7bd-9c908c7fc36e
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 49
    column: 12
    function: main
  location_invariant:
    string: b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc15ded4-c7be-4a03-b6ca-6be64a66fe2e
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 50
    column: 12
    function: main
  location_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e35f249e-4955-4704-ab86-76f2e48f8511
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 50
    column: 12
    function: main
  location_invariant:
    string: q <= -1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d249a42-37f8-47d5-8f49-ca61aa0dff3e
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 50
    column: 12
    function: main
  location_invariant:
    string: r <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8bd5418e-d1f4-4b0b-9c34-6926758f2379
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 50
    column: 12
    function: main
  location_invariant:
    string: b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 955388c2-a00e-477e-9009-b621c98a2ec9
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 55
    column: 4
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 976bd40f-d72a-4bfb-bc70-8df6036f7d38
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 55
    column: 4
    function: main
  location_invariant:
    string: r <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a78f3f3f-75e1-4d6c-9a2a-05d0105c2512
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 56
    column: 4
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c41cee1d-af24-4913-9d03-c8074bfa48f6
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 56
    column: 4
    function: main
  location_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0071e8d3-ad24-4e73-8dd2-4c2b5f3a2b47
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 56
    column: 4
    function: main
  location_invariant:
    string: q <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b165340-97ee-42c1-b92f-0ee03ec73a10
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 56
    column: 4
    function: main
  location_invariant:
    string: r <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 30a0849e-3bae-4529-ae5e-ab0e9635ff37
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 57
    column: 4
    function: main
  location_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d6defc58-3393-4727-a1a1-96debbf3da32
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 57
    column: 4
    function: main
  location_invariant:
    string: q <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e98fd34-d994-4350-a9fb-57560f955822
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 22
    column: 4
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d361a15-54e6-4cef-98f8-ee7fadd5e789
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 22
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c9cbd49b-42dd-41d8-9ae1-8dab47dc5dd8
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b49a83f4-b661-44b6-93a0-a4f9f8981f08
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bb7be94a-77af-4083-82ac-3b1f621a7dce
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: q <= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a8c71cf7-53de-4ab9-b15d-9804b2f21ace
    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/egcd-ll_valuebound10.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound10.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound10.c: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound10.c
    file_hash: 3d9847fe213bf8df5d23c53d2bc8b53fb384c85820b87c09591484702dabefc3
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: r <= 0LL
    type: assertion
    format: C
