- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 075c2a1e-34f9-4342-84b9-22b0b73f3e03
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    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: 64d939cd-2f41-4f91-a05c-1336b5872fc9
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    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: 79514ff3-002b-4081-90b1-9d3a569ab3ea
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    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: d59467de-351a-4837-8361-5ec1d0aa2ea0
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    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: ad16d20f-c7ee-4d05-933c-4616ab689b82
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    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: 2a0146ed-9e45-4867-aa2b-ccf08f9d64c9
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    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: 32d65c92-f1c7-4c9f-853e-c8986a7b7d84
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 37
    column: 4
    function: main
  location_invariant:
    string: -4611686016279904256LL <= xy
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a2c5a1ab-f1bf-4262-b5d3-a797418c7192
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 37
    column: 4
    function: main
  location_invariant:
    string: xy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 28941096-aabf-417b-966b-df83ae66476a
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 38
    column: 4
    function: main
  location_invariant:
    string: -4611686016279904256LL <= xy
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 296a91d6-f0fb-4425-a2ee-addd9eaf32be
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 38
    column: 4
    function: main
  location_invariant:
    string: -4611686016279904256LL <= yy
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 536ee208-344f-4f71-a55c-3bd9ba9d9b5f
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 38
    column: 4
    function: main
  location_invariant:
    string: xy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a3de8d39-353f-432d-9c58-6821e30b2693
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 38
    column: 4
    function: main
  location_invariant:
    string: yy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8a283fc-059e-4b13-ac4e-dbc0f34fc033
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 39
    column: 4
    function: main
  location_invariant:
    string: -4611686016279904256LL <= yy
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2d5038d-c6cc-4e34-93a3-5d9e2942372c
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 39
    column: 4
    function: main
  location_invariant:
    string: yy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3f275a02-ca2a-4acc-a50b-1e4d3c8aac4e
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 42
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f880273a-3180-47e2-982c-423b99166c21
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 42
    column: 12
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57bf7f34-0d28-417a-ba5f-1b61ecd84f84
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 44
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf352837-d055-43d6-8973-07b5c2e38b67
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 44
    column: 8
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb589972-9443-4974-b1d9-45a28f673d86
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 44
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9c76e68-80c3-49fd-9531-acd351c4df93
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 45
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c960513-1856-4436-8cb8-d8abaacd6ffa
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 45
    column: 8
    function: main
  location_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f3bc9a07-b576-459d-9c8d-bbb4e7dfcff8
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 45
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c00a18f-f4be-4257-9d65-90b84227907f
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 45
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a276ba0-3bc6-473c-801e-31b067578cf6
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 48
    column: 12
    function: main
  location_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 813dc45d-1f66-40af-bc37-a1130388debb
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 48
    column: 12
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75ad9c10-9299-4b46-ae8c-e14f6e3682a0
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 48
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da14bf8d-c785-4801-ac45-985f51ef25cc
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 48
    column: 12
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b7b94327-cac2-416e-8f14-920f7a94056c
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    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: 882e0a4a-d0f6-4661-8b68-c602287455aa
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 49
    column: 12
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6bd86990-bbae-4c0c-b915-0ce8ad98eaed
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 49
    column: 12
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7dbeb0ed-bd87-4f54-b651-12858965eb96
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 50
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4252e18e-c5f2-4140-884a-720537afaf68
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 50
    column: 12
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d5d17e7-c935-4a20-a555-41a42c782d4a
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    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: 3acc8145-ae02-4180-8f2f-531257b99bf9
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 51
    column: 5
    function: main
  location_invariant:
    string: -4611686016279904256LL <= xy
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4093322b-6ad0-4786-87ee-2710d01d9c1e
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 51
    column: 5
    function: main
  location_invariant:
    string: -4611686016279904256LL <= yy
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e0e7abb8-f7cf-4b41-89f3-4f161894ac69
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 51
    column: 5
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 659b368a-504a-493e-8e4a-6999bf48102a
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 51
    column: 5
    function: main
  location_invariant:
    string: xy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bbabdecb-1967-4ea5-9e0a-8b879b613303
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 51
    column: 5
    function: main
  location_invariant:
    string: yy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 67223eac-27da-4550-b9de-c72ecfd5b798
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 51
    column: 5
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad78db83-9c78-41a9-ac16-c98f57c75801
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 51
    column: 5
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 01d2ced6-4ee1-4c3b-907f-dc6c9cc0fcbd
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 52
    column: 16
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ffdc66c2-a533-4c07-b149-e2c27cb500af
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 52
    column: 16
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ecbb55fb-6029-4cce-819a-bc4781184f28
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 52
    column: 16
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f87f9ad-7514-41fd-b36e-a84f3703bee5
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 54
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 72cf11bc-d040-4233-8557-2d663581b3c8
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 54
    column: 12
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ff2b72cd-e2ab-4c08-988b-a0bee6e62e76
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 54
    column: 12
    function: main
  location_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 56e94ca6-c99e-441b-a642-313b97701106
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 54
    column: 12
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c59ee95-2db1-4dfb-aaef-9ca3082bdfa6
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 55
    column: 12
    function: main
  location_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b05a92b8-d5bc-46a5-ba6b-b469361e6b84
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 55
    column: 12
    function: main
  location_invariant:
    string: c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be4a8135-afd3-45f9-ba53-dc373e7e02d0
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 55
    column: 12
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d5e0efd-6b8a-4b7b-9fe7-09ceaef4b536
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 58
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c09a09d7-7a53-4600-ad62-88862761b5a4
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 58
    column: 8
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b53e422-8f80-48c5-8612-81e5bee65246
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 58
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f1c18a61-ba17-4d63-bfc8-6d4f71b5f430
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 58
    column: 8
    function: main
  location_invariant:
    string: (-1LL + b) - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4f2e915d-d0a6-469c-9a44-65f7a2b7121c
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 58
    column: 8
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da53ba63-1bc2-4066-9b06-0160895dd706
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 59
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f5fbb430-41ba-4f01-a4f7-2a20cef00425
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 59
    column: 8
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f51f6f6c-64a8-43df-9cbc-8425f9f8902d
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 59
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 21fe8cb6-8095-4210-b37f-1d821bacae65
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 59
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 04a1b69c-9747-4619-9726-ccd7fe8baff5
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 59
    column: 8
    function: main
  location_invariant:
    string: (-1LL + a) - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad7bef8e-dd64-4341-8124-83d582e3f772
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 59
    column: 8
    function: main
  location_invariant:
    string: a != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 867a5fd2-bf44-4cd7-9f02-cc3fb5f50cc0
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 62
    column: 8
    function: main
  location_invariant:
    string: b <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b6a1c2c1-7608-4446-bda3-42991e8cd372
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 62
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3578561b-afef-4632-9a77-29dd7b6b693f
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 62
    column: 8
    function: main
  location_invariant:
    string: (-1LL + a) - b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 86ef2090-b8a4-4b32-b249-0357f0d26a4c
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 63
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7930f62-715d-482d-90dc-ac06c983dd1a
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 63
    column: 8
    function: main
  location_invariant:
    string: (-1LL + a) - b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 81491810-97b1-48f9-bee3-65bfade0ab89
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 64
    column: 8
    function: main
  location_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f26eafbd-bb19-4ce5-80b6-6f01d1bc4ada
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 64
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 06e0ee1b-066b-4592-b033-8d769c3b234c
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 64
    column: 8
    function: main
  location_invariant:
    string: (-1LL + a) - b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9701ce4-f8eb-4624-9a2e-0db592d599e1
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 65
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 85e0d30d-8768-4aa2-83de-70fc478f12e6
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 65
    column: 8
    function: main
  location_invariant:
    string: (-1LL + a) - b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18c80996-7174-46a3-b995-e0fb5e90f13b
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 66
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 65953c5d-095d-45e8-a899-7d34995bda6d
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 66
    column: 8
    function: main
  location_invariant:
    string: (-1LL + a) - b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 612b5fbd-e5b7-4b15-a95f-5c6ed5fbc343
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 67
    column: 8
    function: main
  location_invariant:
    string: -4611686016279904256LL <= yy
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8952be0e-8fde-445a-af7d-9469aff8d8db
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 67
    column: 8
    function: main
  location_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a73b437e-29c1-4d0f-b842-ef791ee029df
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 67
    column: 8
    function: main
  location_invariant:
    string: yy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8775f903-5231-4132-8b63-15a2a7f4c862
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 67
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af2f492c-5fbb-4c7c-9455-da4343c1b2e8
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 67
    column: 8
    function: main
  location_invariant:
    string: (-1LL + a) - b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eaaa2d10-5156-4c42-95c0-cc036b3a9273
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 71
    column: 4
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: da4d4f72-31ca-4047-9c19-4577fb979621
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 72
    column: 4
    function: main
  location_invariant:
    string: -9223372036854775807LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a3b46870-4baa-4437-8ebd-eb15106aee90
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 72
    column: 4
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 59bc2cb7-c2ab-4421-a108-32f9897e7d04
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 72
    column: 4
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43a7f924-e76d-43c2-bbe7-112ac2a594e3
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 73
    column: 4
    function: main
  location_invariant:
    string: -9223372036854775807LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2df8a806-39a6-4b28-b5f9-38acee3510b1
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 73
    column: 4
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e148c92-90e5-4a11-95b0-b2c095c8d2ae
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 73
    column: 4
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 29c681ee-dc2d-41bf-80ae-5eb2c83d3ed7
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    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: 405d6113-de29-4983-bd8d-99addbcb3aef
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    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: 7f06dc5c-0e5e-49ee-9f25-c1cbaf26b9ec
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: -9223372036854775807LL <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 39345a6d-06b5-499a-983c-48212bd3dcaa
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: -4611686016279904256LL <= xy
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 798ea033-49ff-4c4e-91f9-723464733662
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: -4611686016279904256LL <= yy
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d4fe70a8-4556-4ddb-a7a9-2a90ab4a4ab7
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7863ef9b-112c-441e-809a-19d2bec8a359
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b931dfd-1f0d-4744-8ae6-5b6e171828e0
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 879653a4-ed49-4f3b-84f6-6f11e8666393
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: dee49354-6d00-4e9f-9eff-ed3c2b7e24dc
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: xy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0cbf5e10-1f86-424e-92f9-b1298f3bfd12
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: yy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 74287bca-db9e-4467-8df4-b47d7268c682
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 41
    column: 11
    function: main
  loop_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9314487f-4119-4c38-b19f-c5d975e5faad
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 47
    column: 15
    function: main
  loop_invariant:
    string: -4611686016279904256LL <= xy
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d60fcf3-a17b-42de-8645-ce1696821104
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 47
    column: 15
    function: main
  loop_invariant:
    string: -4611686016279904256LL <= yy
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 48143700-9d08-4c3a-872a-92732143e692
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 47
    column: 15
    function: main
  loop_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c5213a0b-2e93-439a-bf66-73dc63616d8d
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 47
    column: 15
    function: main
  loop_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e9da65ba-04b5-4dd8-a9c8-b0d1a4fc8646
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 47
    column: 15
    function: main
  loop_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7676e9f5-39a7-42e8-9475-b83bb37d30cc
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 47
    column: 15
    function: main
  loop_invariant:
    string: xy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d165981-3455-49c0-b627-75b7b6dd0d56
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 47
    column: 15
    function: main
  loop_invariant:
    string: yy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 804476c0-4d46-4b2c-a698-ebe62d357c29
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 47
    column: 15
    function: main
  loop_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: eee8968b-8137-4a90-8a9c-f66055109cfd
    creation_time: 2023-01-27T16:29:28Z
    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/egcd2-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd2-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd2-ll_valuebound2.c: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll_valuebound2.c
    file_hash: ebdf8b0d6633d593d56778eaf5218135ab2be92cae14e75cdda2462494f96410
    line: 47
    column: 15
    function: main
  loop_invariant:
    string: b != 0LL
    type: assertion
    format: C
