- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 48547e52-005e-4713-9571-8071c7e81e41
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 35
    column: 4
    function: main
  location_invariant:
    string: -4611686016279904256LL <= xy
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ecb8724a-bbd9-4b5c-995e-bb7a802ba51e
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 35
    column: 4
    function: main
  location_invariant:
    string: xy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bca09608-4985-4629-9b75-ca77d895416c
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 36
    column: 4
    function: main
  location_invariant:
    string: -4611686016279904256LL <= xy
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9064184c-e4ee-45c4-b799-8268c02d6543
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 36
    column: 4
    function: main
  location_invariant:
    string: -4611686016279904256LL <= yy
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a2d86dc3-d129-49c8-a3c8-e86bf7e4ff93
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 36
    column: 4
    function: main
  location_invariant:
    string: xy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a47c806-f44c-47d8-886a-279197823d58
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 36
    column: 4
    function: main
  location_invariant:
    string: yy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c8c2180-af40-4d57-9c76-17f93936243b
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 37
    column: 4
    function: main
  location_invariant:
    string: -4611686016279904256LL <= yy
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db898770-4dc7-4c03-9e24-49c09e8a9d60
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 37
    column: 4
    function: main
  location_invariant:
    string: yy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 533ae169-ba57-48b6-92df-74a92d87adcb
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 40
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cc487d31-bec8-44b1-8fc6-ef63e69e2dd9
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 40
    column: 12
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1e2be7f-06d5-4cc6-877f-9824a3612e3f
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 42
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 53e8a3db-4726-4d1f-bc65-cd513210a8d8
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 42
    column: 8
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a114a6b-47fb-49d0-960d-fcc2f642ae58
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 42
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cbdbf2e6-d20c-4d94-88c2-916dfcde1e0b
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 43
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1dc5d6b1-1ed0-4d48-af54-da1aa0a21a71
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 62a4d9ab-1aa7-420a-a887-b114bed4557a
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 43
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd2009e6-d60b-415b-b471-fc50171b55fb
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 43
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39cba6f1-97e4-4134-99be-3d149f03736d
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 46
    column: 12
    function: main
  location_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6862df90-5e11-4a77-986b-4498ac864457
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 46
    column: 12
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee92d540-964a-4da5-8fb2-813ef01815c8
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 46
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee53cb50-839f-4367-9de5-bfb13a795679
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 46
    column: 12
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: df538fcb-aaae-4570-ba9a-3f392a134ffd
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 46
    column: 12
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae626882-682f-46e7-8d3b-d9b8a30cfcef
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 47
    column: 12
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 790c83b0-12a2-42cc-a8a5-e011b580c6f7
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 47
    column: 12
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c495f60-35ec-4c20-9221-a3d86723b1b7
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    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: 561cd8a5-b1a5-4f9f-adea-24b452244b61
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    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: 936c24a0-6e72-4b6e-8c0a-516ba394feb4
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    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: f799eccd-2a9b-4a0c-9a1c-abbfb15a8625
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 49
    column: 5
    function: main
  location_invariant:
    string: -4611686016279904256LL <= xy
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 84c800a7-fa4c-47ba-8f26-6d05dbdc1811
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 49
    column: 5
    function: main
  location_invariant:
    string: -4611686016279904256LL <= yy
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7352520e-6b94-482b-aa7e-e65752676c0c
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 49
    column: 5
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c48acd9a-dfa9-4802-8ce8-6d5611bcdf2f
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 49
    column: 5
    function: main
  location_invariant:
    string: xy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b0ba097-9f77-400e-8d97-6552259e04cc
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 49
    column: 5
    function: main
  location_invariant:
    string: yy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1eb5786c-17d3-420d-b509-b2a73464b5a0
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 49
    column: 5
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa17a690-021c-4dae-b866-74cbbfb7bea1
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 49
    column: 5
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0432cf3d-dba2-467f-80a0-2dd7dbedc6d2
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 50
    column: 16
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 415ad8f1-873e-4437-ab8c-37ece509010a
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 50
    column: 16
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c4285a76-3c73-4023-95ca-ceab3a92aa72
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 50
    column: 16
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c9c9258-7a12-4bff-8ca9-c8823afa37da
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 52
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f865f4f6-df13-446d-9d33-7eb0ba0c455a
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 52
    column: 12
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b69ef56-12f3-424d-8c29-89c24151cdd0
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 52
    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: 2ef41f06-9d63-487b-a159-89def2943ee8
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 52
    column: 12
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a25da2cf-3982-48f5-906f-ac7e9df3c015
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 53
    column: 12
    function: main
  location_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8515dc5b-c8d1-437e-add3-d86eef6cab06
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 53
    column: 12
    function: main
  location_invariant:
    string: c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc271ee9-b365-466f-b083-c4a0de2c33db
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 53
    column: 12
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eef18186-6810-4ca8-bc46-884cf335515c
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 56
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 608c7f71-4492-44d5-93b2-20110577a014
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 56
    column: 8
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b2b0921-7c5e-4b28-8329-9b5d3f93e0fc
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 56
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b11ca08-9a15-43f8-9e03-519daa3e3910
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 56
    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: 25b20aca-8fee-4154-8072-9a050ed391c9
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 56
    column: 8
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa6c8eb0-0732-404c-93e7-e3163ed1fb38
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 57
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9044d84d-0475-47d1-9891-997788d90fc4
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 57
    column: 8
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e50fa6a-29e3-45dc-869d-1baba5b532ed
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 57
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5372c8e6-648b-451e-9cec-0aa0c68e3655
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 57
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6612ad5d-d99b-4570-b06d-ee62f3bd49b1
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 57
    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: db37b717-6670-4d41-b213-b30051c73ee9
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 57
    column: 8
    function: main
  location_invariant:
    string: a != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8dbbca2a-d59e-4966-bc4e-ba9bda195d9a
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 60
    column: 8
    function: main
  location_invariant:
    string: b <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79c55cf3-886a-4829-8ab7-95dc96101d9d
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 60
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14ef6fa2-cc58-4093-9952-7e1eddae96a2
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 60
    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: 35feb05c-0cde-42dd-a368-dcb49649c1d6
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 61
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c071630-a29b-40b1-a64b-36897bc1ebbc
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 61
    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: ed1d678b-3fe9-4c5c-b14d-545a5184f089
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 62
    column: 8
    function: main
  location_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cf2d94e3-bf3f-4d07-8267-38e2d693b99e
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    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: c1eaa5d9-ee3f-4ad2-ae26-86e35c4b0784
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    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: 610fc8f8-53fb-45b2-9cb8-633b190d4d32
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    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: ffb43384-d74c-4ac4-a379-cc4e5c9a0f48
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    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: 8e0edf85-6d86-4688-93b5-4ebd9cfdc264
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    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: 7278d12b-f305-4d03-a98e-a3f2276eb5eb
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    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: 634f01b6-b6fe-4b0f-9777-d5e1fd48f173
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 65
    column: 8
    function: main
  location_invariant:
    string: -4611686016279904256LL <= yy
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd8df063-b7fe-4178-8341-beee03356eff
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 65
    column: 8
    function: main
  location_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e82a8a6-1ba6-47c4-89bc-d75f4fadfbef
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 65
    column: 8
    function: main
  location_invariant:
    string: yy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad39d01f-57cf-4a26-b023-8360f58d3519
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    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: fb65892b-4ec8-4bc9-a7ba-dada06d3a526
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    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: 88921157-3811-4b31-af5a-3eeb643799c6
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 69
    column: 4
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76d6d52f-3e41-4f7b-aadd-8403d420f981
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 70
    column: 4
    function: main
  location_invariant:
    string: -9223372036854775807LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c835ba7-e1eb-431f-9e70-62a65acb4436
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 70
    column: 4
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 60b405af-59f5-4e7b-ab95-720f19726297
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 70
    column: 4
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 94fe134b-a756-46a0-8e0c-1ec8bf803f5a
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 71
    column: 4
    function: main
  location_invariant:
    string: -9223372036854775807LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99917238-598f-4942-85dc-6bc0e24894f2
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 71
    column: 4
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0676a333-4910-4a5b-92af-e6175887d8d8
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    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: 4c54dfd9-8dd4-41a8-b27f-ff72e1b97dd3
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3504e901-9f01-4667-8d9e-c377bf0f934a
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 27
    column: 4
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee6fbf62-0bd5-4eed-9f7c-78e28a003332
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57fd58ba-4cdc-4725-ae62-316813f185e6
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 28
    column: 4
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ceec1ce3-c983-4b5e-b8b3-cd3641a35da9
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 39
    column: 11
    function: main
  loop_invariant:
    string: -9223372036854775807LL <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0dc9d83e-b4e4-44a1-b426-955b830715da
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 39
    column: 11
    function: main
  loop_invariant:
    string: -4611686016279904256LL <= xy
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 335c26f2-35cb-4ae9-80fd-3659dacac217
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 39
    column: 11
    function: main
  loop_invariant:
    string: -4611686016279904256LL <= yy
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: df87f8ed-5dde-426f-8134-746cb735ed56
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 39
    column: 11
    function: main
  loop_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d491436-1716-4009-8c18-f3bd3cf91de5
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 39
    column: 11
    function: main
  loop_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c4c38593-56e8-4efa-bd28-48fe447afd05
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 39
    column: 11
    function: main
  loop_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a15cc604-362d-4135-9e79-6a660b55f919
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 39
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bcfd16d6-56ad-44ef-9733-e41d084fc556
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 39
    column: 11
    function: main
  loop_invariant:
    string: xy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 41deb03d-fb27-4c53-b8d4-8e49bd46f624
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 39
    column: 11
    function: main
  loop_invariant:
    string: yy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b487685c-93cd-42cf-82da-566ebf7494e9
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 39
    column: 11
    function: main
  loop_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 425438ce-95f0-4f68-ae79-477a2be45223
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 45
    column: 15
    function: main
  loop_invariant:
    string: -4611686016279904256LL <= xy
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e2d128aa-8d09-43d5-8709-b6316aeb41ee
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 45
    column: 15
    function: main
  loop_invariant:
    string: -4611686016279904256LL <= yy
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 19cfcccd-10ab-4bbf-955c-c28cfc7179e5
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 45
    column: 15
    function: main
  loop_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 297694a3-33e2-4dbf-8454-e4380eafde1f
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 45
    column: 15
    function: main
  loop_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8bdef23d-3c8f-44ac-9d2f-9cd08bc42f14
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 45
    column: 15
    function: main
  loop_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 276edfea-9e7e-416b-bfab-c08917508aa4
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 45
    column: 15
    function: main
  loop_invariant:
    string: xy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5badced6-aa20-4bb2-adbe-3856bec16131
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 45
    column: 15
    function: main
  loop_invariant:
    string: yy <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fc7fe2f6-0756-4be4-b106-7452150b1584
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 45
    column: 15
    function: main
  loop_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: eeebc8ed-257a-4db1-9344-8fd364114d53
    creation_time: 2023-01-27T16:29:27Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd2-ll.c'''
    task:
      input_files:
      - ../plain/egcd2-ll.c
      input_file_hashes:
        ../plain/egcd2-ll.c: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd2-ll.c
    file_hash: ed6536c9cb0e4b2be9a327fc4a25c6bfba6e98b1dfb78e314dd25bca8cbdb087
    line: 45
    column: 15
    function: main
  loop_invariant:
    string: b != 0LL
    type: assertion
    format: C
