- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 426e1777-dd8d-48b7-a3ef-5e637d8197a5
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e1e65ae9-5dc4-4e49-8923-d18108dfb2fc
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 34
    column: 8
    function: main
  location_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd04e406-389b-4aad-a6f2-67dcc4473e6d
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 34
    column: 8
    function: main
  location_invariant:
    string: q <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c4d43108-9028-41b0-9d35-02ae8e901e2f
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 34
    column: 8
    function: main
  location_invariant:
    string: r <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5bb4ebed-bf29-4d83-9b45-2d370bfffc76
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f4c461c-b102-444e-b338-90d1bea6424f
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 35
    column: 8
    function: main
  location_invariant:
    string: r <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f69b70f1-f3fc-4bc6-bebf-1b763e756dce
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    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: c5bc70a1-5536-489f-bd21-e6096d9fc34a
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    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: 7b7cda48-64d4-4bd8-bc02-da14b44c177e
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 42
    column: 12
    function: main
  location_invariant:
    string: -9223372036854775807LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d6fde5c3-7e75-4ae2-9d7d-fa338ccd61ec
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 42
    column: 12
    function: main
  location_invariant:
    string: b <= 9223372036854775806LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 279d2ee6-a449-4a52-9f36-1823644275c1
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 42
    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: 4de5c81a-2ad4-4ac2-97a0-61c3b5115a64
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 43
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3336ebf4-f934-493e-9517-ce4ec8fa193b
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 43
    column: 12
    function: main
  location_invariant:
    string: q <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 24d330d8-f40b-415f-9e48-9e62e62d34da
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 43
    column: 12
    function: main
  location_invariant:
    string: -1LL + a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a1f1883-0c03-4206-b89a-d690916a17e3
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 44
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 623231b9-bd0f-4c51-a5c4-a20c89f92303
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 44
    column: 12
    function: main
  location_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef38f82d-4e31-4c3d-addd-d91ef5be7eb3
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 44
    column: 12
    function: main
  location_invariant:
    string: r <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 605d5641-d9c5-4af3-b8e9-ef22dfd62f84
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 44
    column: 12
    function: main
  location_invariant:
    string: -1LL + a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3021e7f0-8b21-4c75-a71b-1b50846d1d13
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 46
    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: 7cb79569-3705-459e-8df7-e573fcea8064
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 47
    column: 12
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fdd78f60-9e8d-4b6f-8f8a-fd4526a4097e
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 47
    column: 12
    function: main
  location_invariant:
    string: q <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4280365d-d77a-4d16-bbf4-277d28e5884a
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 47
    column: 12
    function: main
  location_invariant:
    string: b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75e847f6-62cc-4df6-a3ee-921093eb5f59
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 48
    column: 12
    function: main
  location_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b8e9bd40-578b-4675-a0f0-9339b2ea401a
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 48
    column: 12
    function: main
  location_invariant:
    string: q <= -1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57578f00-16f3-4e40-aad4-bff10149745e
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 48
    column: 12
    function: main
  location_invariant:
    string: r <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b732f916-c498-4283-add1-db2289507cdf
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 48
    column: 12
    function: main
  location_invariant:
    string: b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb96a4b4-959f-4ca3-b162-306f13f78029
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 53
    column: 4
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: efb6146d-ce67-4088-9bb4-5428e9e6f3db
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 53
    column: 4
    function: main
  location_invariant:
    string: r <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eea735b9-c10d-4be5-864c-bc19ce694e17
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 54
    column: 4
    function: main
  location_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d7a1cae-75df-40a6-9d72-a6cb740141c5
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 54
    column: 4
    function: main
  location_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bcd127ca-8e94-4198-bc0d-d9bcd0aa7866
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 54
    column: 4
    function: main
  location_invariant:
    string: q <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6136a71c-d186-477e-824e-96d0f77f2607
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 54
    column: 4
    function: main
  location_invariant:
    string: r <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c45f2946-6e1f-4fbf-b789-c71f8b150d5e
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 55
    column: 4
    function: main
  location_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ed116bdf-19e1-4a54-83bd-fa9e47407f42
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 55
    column: 4
    function: main
  location_invariant:
    string: q <= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9dc57549-ffc0-401e-9bb2-a122ffa662e8
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 976ed9b4-900f-4e03-9b4a-9f8674ef2ed3
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 27
    column: 4
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3f7c4cb-95c0-465f-9f60-70d196292db0
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73fd600b-cc46-4bd7-a833-b7f9618d5121
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 28
    column: 4
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1fbe8141-2e91-4fcb-8a22-74e172ae1867
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= p
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 00060c91-d378-4ec5-8166-9d5e8b64f45e
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= s
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 09bd3853-3b55-4af1-8e71-67fb26a37dc4
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: q <= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 18ba2369-fd6d-4f3a-9a9e-e8bb1a4ae6da
    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.c'''
    task:
      input_files:
      - ../plain/egcd-ll.c
      input_file_hashes:
        ../plain/egcd-ll.c: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll.c
    file_hash: 5cf588c7d7521936f2238a5a4b8ed55e91050a69daa6016b5b2b4a486ef1b9f8
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: r <= 0LL
    type: assertion
    format: C
