- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e1c8dd0-4d1f-4c86-9f55-ba8a1e3aba52
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 370019f4-e2a6-450c-b9dd-bd7b7e61f623
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: d328fce9-5299-4f85-922e-975b865650a2
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 518d487f-89bd-4b28-ad5b-37553195028a
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 7ae613fd-2741-437b-b3d0-41c1d3cf75ef
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: ce2318f6-2a98-498b-9185-430de8e5bd6f
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 06261ae6-7796-4f6b-aee0-65fdcd591c4f
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 9fb1573e-6a74-429b-aa66-0d060747db00
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: a35ec8bd-c2b0-44ec-a830-fdf92d05fa32
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: a28fe7dc-e9d2-4d2c-b324-d84508666af5
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: f5457a3c-440c-4174-994c-d4e52f4c1c52
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 950b6894-7137-4f7f-9980-521da47db83a
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: e16fc4f4-08c1-40f6-a954-54cf5ec7eaf1
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: ea779c85-04f1-44ca-a598-0bddec635ba9
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 2d8e1e15-e885-40fb-b11d-e82e6292ffb7
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 6d193786-b728-423e-b1ba-14ecf7a7b7f7
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 311931df-7012-40bf-82c9-4f7934ba9e9f
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 1f78be86-83fe-4b10-ad52-9d7b4eac35f3
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 4dec2918-da38-4182-aa6f-ce135c9ba05f
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 935074a9-3a4d-497d-9d35-eeaac610cd1f
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 0839ffef-77f1-4a4a-a40c-5e3f264ea257
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: fdfda991-5d43-48fe-ab03-fd3aea60ed49
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 4a03a9bc-8a68-4f52-a9f1-64db6dcd1a6f
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 940fbc13-817f-4668-a5d8-52e9b0647140
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 1d6bbaec-f01a-4ef0-a672-44555c326d05
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: c3edbba0-38fa-4d8c-bb58-35a297808b7e
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 4b39be97-f027-4315-8c32-06410406fd1d
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: db70dcd4-6ebc-424f-9a27-936a38b7bd89
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 0ac20ae5-86a7-4ac2-bddc-05c83f110b61
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 635bb6ac-e9f4-4baa-b1f0-4d6b34ee8a10
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 0691ccca-a507-495f-9c26-099639552a7c
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 853eb2a5-65ad-4af8-a244-58b17e834aef
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 7f7ceae8-9601-4182-9ff4-243d1c67354e
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 42213896-fb44-441a-8c60-212895607fa7
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 3e99141a-438a-4e5f-bf5f-faa68d6a4380
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 25cca556-4cd1-458f-925c-39fb4c80e739
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 56febdc4-c9c6-4f5b-94fe-3c17be8917b8
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 71b57713-2fda-46b8-8697-b347495eaf9c
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 13600844-eba6-492a-8bbe-94e32cdceaa5
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 4b105d2a-a8df-4072-b1d8-4ae49f3234f6
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: ef02faf7-8209-47cc-af33-d8c893e82a9e
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 591136eb-71ad-48a7-8172-da18968e31c9
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 6b78530e-646b-47ad-820e-1f047dc066ad
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 83348061-4c79-43a0-9523-ffddb31a7997
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 00be4a9f-5b4d-4360-954b-c85153f548d4
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    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: 253fd450-53e7-446a-8007-da1f66b53320
    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_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd-ll_valuebound2.c: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd-ll_valuebound2.c
    file_hash: e89b4ab54b22145b4041cfb458aca993f2d791ac86940dcd03d48a90a5273393
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: r <= 0LL
    type: assertion
    format: C
