- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 713f1902-6842-4e0e-8165-1750b9729147
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 0 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a045f796-07fb-4c55-96bb-944bd7f02dc1
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99bd6dbc-39b5-4b29-88ab-ec6a5f63f0b9
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ccb3112-0157-400a-a121-4bea14a03a24
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 29
    column: 4
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be46c401-d0bb-4eb8-9844-2b8b194ae0a8
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2326c5e1-5116-4087-93e8-85b2da935c8d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 30
    column: 4
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25ba532d-f10d-4bc6-a4f8-e2862de99847
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 36
    column: 12
    function: main
  location_invariant:
    string: -9223372036854775806LL <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ff1c82f9-43b9-4e0e-9dcf-904cfbe0bf1a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 36
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4faf5e75-e09a-4687-bf1e-c89caa41b1b0
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 36
    column: 12
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8c879124-8b23-47b1-ae3d-eeb4eff43cf9
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 39
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775805LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 85912e08-42b1-487e-b23b-26aa0122acb6
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 39
    column: 8
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 53e84e38-8e07-43ef-81b6-2de0a1f85122
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 39
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fdd206b5-c14e-4b8b-91ac-a219d0d3b2ee
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 40
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775805LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2905fea8-5637-4926-b7ef-a5742ef43bb5
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 40
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d7e5a751-b0b5-488f-8701-e6803368bece
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 40
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5bf7a3aa-574d-4dd8-9fcf-4e3a57389598
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 43
    column: 16
    function: main
  location_invariant:
    string: -9223372036854775806LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d1f4066-e344-4896-bc2a-373316bafe8e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 43
    column: 16
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e670cb83-d95c-420c-b787-ea7ce41672e9
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 43
    column: 16
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 423f62eb-16c0-42b5-a890-dfdda783d2ea
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 43
    column: 16
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 059e508f-e598-4d40-8875-ffaf99e714df
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 43
    column: 16
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d63c0efe-70cb-4bf7-87ed-a33af1daac2c
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 43
    column: 16
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 47601e77-3955-4611-9f93-7393d170e00d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 43
    column: 16
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e580799e-ad47-4955-999a-7289cc2f7a38
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    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: f5613896-321a-4e06-9386-ff1f57be3ad3
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 46
    column: 12
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: acee86ee-9599-4328-ba06-6624bfd3035d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 46
    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: 9fd0f162-4e06-4a1b-95e7-7ed3a8676268
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 46
    column: 12
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 71d67792-945b-47d5-9b40-1a1745dcce89
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 47
    column: 12
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1a4c23b1-4363-4cff-b263-8c44a92d7a60
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    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: cf7e7b67-5ad6-4bb5-9134-32c57e89f5b5
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 47
    column: 12
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c177fcdf-78f8-4937-86c3-f9e02d83e241
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 47
    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: 47715935-d41f-4132-9c0b-99e79f4d3d9e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 47
    column: 12
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c6990e82-41bd-4256-b13c-aa54d85982d5
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 47
    column: 12
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bfc8f5dd-0fcd-4eb0-b627-cf68128bfb52
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 50
    column: 16
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af0a7fac-f96a-470a-a5de-d59730bcb1e1
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    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: 70c2da68-b195-4976-9fe0-d5ce8bf0e751
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 50
    column: 16
    function: main
  location_invariant:
    string: -1LL + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2a43fa8-0d96-4c14-847f-5e6282cde68a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 50
    column: 16
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7612fabe-bf5f-4c46-86bb-9ef6b3006308
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 50
    column: 16
    function: main
  location_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a2741f5f-2e6a-4b5a-ad82-d76081861e62
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 50
    column: 16
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f216e76-0c59-4ec3-9173-5904d1fcc872
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 50
    column: 16
    function: main
  location_invariant:
    string: c - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bdd10711-6555-4e69-b82e-9de75c5f91e6
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 51
    column: 16
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e59c44b-3bd3-459c-8074-8f670e59c8cd
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 51
    column: 16
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2dc3ebdf-785f-44e4-a918-2ffd1eac8220
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 51
    column: 16
    function: main
  location_invariant:
    string: -1LL + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c2249201-54b7-490c-9efc-09a093f88f89
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 51
    column: 16
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0ad11a74-84ec-410a-8256-39c0946259d4
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 51
    column: 16
    function: main
  location_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c46cde5e-1bd9-4c8e-a4ea-2e60a415bab2
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 51
    column: 16
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35350831-839d-498a-be45-2b2aba8dddae
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 51
    column: 16
    function: main
  location_invariant:
    string: c - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 448bb43c-675a-4561-8aba-310df75c5799
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 51
    column: 16
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3de0f2d5-824b-4124-ba34-fed4cc2f6b27
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 52
    column: 16
    function: main
  location_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3595941c-53fc-4b4d-87d6-8e827d90acf5
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 52
    column: 16
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2cabb973-dd73-4a3f-93f8-451927368007
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 52
    column: 16
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 06a61ae2-d133-46d3-a549-767a478eeb8a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 52
    column: 16
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 440c897e-70db-42cd-9af7-2cf05384f987
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 52
    column: 16
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c72dd09-0414-4d2c-be80-894ed9dd9f17
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 52
    column: 16
    function: main
  location_invariant:
    string: -1LL + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 29be6e4a-34aa-4fd8-af7e-55d5c7f66256
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 52
    column: 16
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77f8eba9-1981-4627-aea9-35126bf1c251
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 52
    column: 16
    function: main
  location_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8b623674-c692-450f-aec8-a2b29c5bc2d9
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 52
    column: 16
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b33c9843-29b8-4b77-9417-5ff403043bf6
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 52
    column: 16
    function: main
  location_invariant:
    string: c - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43163f7a-73e3-45e2-9d2a-0debee8930ed
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 52
    column: 16
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 306879f9-f428-4042-a838-12fa4cb9c400
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 53
    column: 16
    function: main
  location_invariant:
    string: 1LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d6ac6632-116b-4b98-b70a-395ffce57dbd
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 53
    column: 16
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a0135ed-d55f-41df-9911-c73bd06b9f72
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 53
    column: 16
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1f7bd74-346a-4635-9b10-09760f319727
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 53
    column: 16
    function: main
  location_invariant:
    string: -1LL + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ee6832a-ad73-4b03-8521-e5676be3de8b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 53
    column: 16
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e685d62-1a53-42ad-84f3-6c3d04eb8606
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 53
    column: 16
    function: main
  location_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5eabcf8d-9c23-4cc8-9f73-7e1d000978a3
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 53
    column: 16
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 38f99a80-c6e7-4362-a9ba-a0b2752a3b4e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 53
    column: 16
    function: main
  location_invariant:
    string: c - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 082085f8-c7c7-4605-809e-028eae22fda9
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 53
    column: 16
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 46af1927-2176-4bf1-aa4b-c91f140d9705
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 55
    column: 20
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e03d2596-5967-4816-98d8-80ee0f6f8e58
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 55
    column: 20
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0cf4032f-5d86-44b8-aa52-659040261305
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 55
    column: 20
    function: main
  location_invariant:
    string: -1LL + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 56b3c28d-bc3a-4a10-a3a7-5c0a70648bbd
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 55
    column: 20
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 02a5691d-cffa-4d53-add8-aea18a0c3be8
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 55
    column: 20
    function: main
  location_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 11464787-54ef-4c30-91d8-d068ad332ad6
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 55
    column: 20
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0490ea7d-5c8d-4128-8142-5b5eb7acee9f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 55
    column: 20
    function: main
  location_invariant:
    string: c - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db6d0e43-5878-4e45-bc4d-d454dc6b7116
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 57
    column: 16
    function: main
  location_invariant:
    string: 1LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cf0314a7-9027-4cf6-a4d0-04d6526efee3
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 57
    column: 16
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 41fe34df-79aa-4b03-a377-dbc61c8731be
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 57
    column: 16
    function: main
  location_invariant:
    string: -1LL + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6dddce5-6c31-4422-bd6d-fdd786d19934
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 57
    column: 16
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8897c54b-67bd-436b-a7a0-b843ecdd00b3
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 57
    column: 16
    function: main
  location_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 20142e8e-e951-4597-aa34-0e1552caea0f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 57
    column: 16
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a949b08-cb94-48f0-98aa-ddd18dfa59e1
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 57
    column: 16
    function: main
  location_invariant:
    string: c - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cec98d5f-c04e-4da8-af37-84fd40697310
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 57
    column: 16
    function: main
  location_invariant:
    string: c - 2LL * v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1289c444-cd2f-4824-9952-59bb01e8e604
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 58
    column: 16
    function: main
  location_invariant:
    string: 2LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4604353f-32cc-4f1d-b645-029f1a31165d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 58
    column: 16
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b3c45dfd-f352-4e73-85a9-18ac5765368c
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 58
    column: 16
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c120f374-6ca6-45e9-b236-26db107a8e68
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 58
    column: 16
    function: main
  location_invariant:
    string: -2LL + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b81305ab-24c3-47ec-9c9b-99befd4bbd71
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 58
    column: 16
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5df3a98-4338-4571-a137-2a78540b35ff
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 58
    column: 16
    function: main
  location_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 22eea209-f6f5-4580-963a-2dfbd82a4236
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 58
    column: 16
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 749cf890-6bf2-4eb7-b7d2-847431e0a3cd
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 58
    column: 16
    function: main
  location_invariant:
    string: c - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 41710847-aeaf-4e7f-8828-6184fbe29767
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 58
    column: 16
    function: main
  location_invariant:
    string: c - 2LL * v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3d2011d5-eb87-4670-9e17-84b4c42039f2
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 58
    column: 16
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 683223f9-d353-446a-975c-47cedc023b0e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 60
    column: 12
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d7fa19ed-ac6a-40c0-ae95-912239126f59
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 60
    column: 12
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80038c5a-206f-4f0f-ab3b-f80b555efb35
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 60
    column: 12
    function: main
  location_invariant:
    string: -1LL + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f1fab866-904b-4e01-a415-0b762aea98bd
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 60
    column: 12
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82ee08b7-ddae-4937-a0e5-d55d39db0764
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 60
    column: 12
    function: main
  location_invariant:
    string: (-1LL - c) + 2LL * v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 527b5bf5-44d4-48b7-9387-212a15d06536
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 60
    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: ead1bafa-755b-495a-a50b-7ee0b0520bdc
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 60
    column: 12
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 70fcb4ea-f00f-4178-96e7-97b66ebc6d6f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 60
    column: 12
    function: main
  location_invariant:
    string: c - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d2f5361f-6f7e-4b06-b6f3-f38a6cd8c522
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 61
    column: 12
    function: main
  location_invariant:
    string: -9223372036854775806LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ea70d41-a968-4ae1-96b8-ac8310eef891
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 61
    column: 12
    function: main
  location_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d5dd6650-da90-4636-a8f5-32dea9f6922b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 61
    column: 12
    function: main
  location_invariant:
    string: 1LL <= d
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 71969b4d-4faf-4656-80a1-1b7a64245223
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 61
    column: 12
    function: main
  location_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 273190d7-7e25-41d1-870b-ed934490500a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 61
    column: 12
    function: main
  location_invariant:
    string: c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a1dfe5b5-1c24-4504-8d2c-088c3cf6b5a4
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 61
    column: 12
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 616a2633-8682-4d32-af84-897f1dde242a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 61
    column: 12
    function: main
  location_invariant:
    string: -1LL + d >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f117df1-84bc-4568-9b8e-3e35f2879674
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 61
    column: 12
    function: main
  location_invariant:
    string: ((0LL - b) + c) + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 430d9cb6-223b-4f0e-b962-b26f0a0343e0
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 61
    column: 12
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7cfd1567-0cf7-4595-9c5a-2d4f526e9740
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 61
    column: 12
    function: main
  location_invariant:
    string: (-1LL - c) + v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cc1f9721-22a0-4c4a-9766-bd837aa9fcb3
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 61
    column: 12
    function: main
  location_invariant:
    string: (a - c) - v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1500c8bb-4e64-44d2-8c0f-189398e0695f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 64
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775805LL <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ed4bcfbd-138f-4f1d-943f-2fcd94777caf
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 64
    column: 8
    function: main
  location_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fa0795a2-eb0d-4713-bd7a-ef453835bc1d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    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: fd0a0299-5c4b-430c-afc4-567bc6d6c32d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 64
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7511fd53-7c3b-4d39-8d18-e4329fbd985c
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 64
    column: 8
    function: main
  location_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4420648b-3cbb-4823-994e-a8d0a2b3401f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 64
    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: 671e2442-864a-4fe0-93d2-ed472df6bfc2
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 64
    column: 8
    function: main
  location_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b870e7e8-d08b-4322-aaa2-cd3e31b76809
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 65
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775806LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d9bcba9b-2ad0-46b4-804d-c07a84f28c18
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 65
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775805LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 261bf962-17f9-4c34-8fb7-786216c51507
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 65
    column: 8
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a04d7c9c-339d-4094-84e2-f8c4928d2053
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 65
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d5cc7ed-6ec8-475f-844c-d3c2e6883b02
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    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: 236b3a21-32b3-4a59-b3c5-79bd6765b3dc
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 65
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - c) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b0caa359-5cf5-4cf5-b14a-7b76da02f44e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 65
    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: 6614e059-1906-40b6-b6ee-261c149747b2
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 65
    column: 8
    function: main
  location_invariant:
    string: a != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f8299f6b-9734-4ea1-9a2f-dd625636ec72
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 67
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775806LL <= b
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7227b937-8a37-4acb-9a81-455a85ac15b2
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 67
    column: 8
    function: main
  location_invariant:
    string: b <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a71dfea-e211-47d6-ab41-b6b679c96ca9
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 67
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e5720514-3cc6-4458-b5d4-8079f6303271
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 67
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8a99cf48-f573-480d-adaa-b571cf6d0ff3
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 67
    column: 8
    function: main
  location_invariant:
    string: (-1LL + a) - b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1a6a93ca-2bd9-4f8c-9fd0-7e2905ec301b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 68
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e7ff5394-5d3c-4001-b37a-2d6cc26a91a9
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 68
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8acf8b58-9681-4d94-bfd6-0aa668ce7c87
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 68
    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: 381d33be-a392-442a-9aa8-8b7da91b6856
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 69
    column: 8
    function: main
  location_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c743b34-cffa-4401-a687-41c9ae837645
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 69
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 998523db-b2d5-4ef5-bee3-9a15be4cc381
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 69
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 061d4496-01c8-4176-aa5b-b6f226b51178
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 69
    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: 9842a511-8a8b-475a-badf-8143ffd98074
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 70
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 271bd183-b29d-471b-b9d8-373950d40812
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 70
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 65facf46-59f9-4800-9a78-138b9ebca71a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 70
    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: edefad68-69af-464f-b279-b06f56afdca1
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 71
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 89af5e66-b1fc-435e-8e83-541ae9863ad9
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 71
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b481998a-7a80-49ae-b47b-f5e71d2174d0
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 71
    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: 93473cf6-d826-4e9c-a660-96fa4750b086
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 72
    column: 8
    function: main
  location_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba9196d3-be63-45aa-925a-29888153b5a6
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 72
    column: 8
    function: main
  location_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b86a19b-c9ca-4058-9fe0-3ac8269702e4
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 72
    column: 8
    function: main
  location_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2aa082b9-a283-4652-a54d-4a6d37fd45d8
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 72
    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: e6be6c1f-b126-49c9-ae0c-b33faa091b61
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 74
    column: 4
    function: main
  location_invariant:
    string: -9223372036854775805LL <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c21bdeb6-0b25-40d1-b459-02ff7acf8592
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 74
    column: 4
    function: main
  location_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9beb772b-fad9-49fd-a7b0-5ec7b06a165a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 74
    column: 4
    function: main
  location_invariant:
    string: ((0LL - a) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 28817414-eb8f-4ae0-bf36-7738f9e5369c
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 75
    column: 4
    function: main
  location_invariant:
    string: ((0LL - a) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a3966096-ef50-4ef1-b342-7bd536ea8ac8
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 22
    column: 4
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8493e691-517f-4a12-8426-d86336d1a710
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 22
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fd598e7c-39ed-4fd3-8e2c-1cbe2ad4b27a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: -9223372036854775806LL <= b
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a5a873a3-f404-4045-a66c-bbcaa152b301
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: -9223372036854775805LL <= a
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3f241b5c-aadb-44ce-bc54-038232b27957
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2ee057c3-4a3f-456b-99cb-caa65d0e3ddd
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f3c3545-39e4-4cd6-933c-9b5a7a78220f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 35
    column: 11
    function: main
  loop_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 77872c97-440d-406f-b95e-3236d0e16a97
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 42
    column: 15
    function: main
  loop_invariant:
    string: -9223372036854775806LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 792c14b3-65b3-4947-8393-efc6a7eb52bd
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 42
    column: 15
    function: main
  loop_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4e6628e4-a24d-4591-b7a5-63061d26d8fb
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 42
    column: 15
    function: main
  loop_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: dd82e848-0fab-4e5b-b4e1-52044ee9a2ce
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 42
    column: 15
    function: main
  loop_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 21ee7daf-cfa8-46ab-b88d-ba4202b52d26
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 42
    column: 15
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d47054f3-8db4-4d55-915f-bc53736cfc8a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 42
    column: 15
    function: main
  loop_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b696df2-c019-416b-8e71-29268906e64a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 42
    column: 15
    function: main
  loop_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1a407c24-2119-4c09-90d2-6e1e354268a9
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 42
    column: 15
    function: main
  loop_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7fe17394-1004-49b4-91f7-5013d8157a74
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 42
    column: 15
    function: main
  loop_invariant:
    string: b != 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0adc609e-cd27-4caf-b8da-75033f612f2b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 49
    column: 19
    function: main
  loop_invariant:
    string: 0LL <= k
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e80a9a64-2762-4e8e-ba0c-44ef07336a11
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 49
    column: 19
    function: main
  loop_invariant:
    string: 1LL <= d
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9cadfa6b-b561-4466-b6ec-e6802f9ec40a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 49
    column: 19
    function: main
  loop_invariant:
    string: a <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6bb7c2b2-ce20-4938-8554-094019156f46
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 49
    column: 19
    function: main
  loop_invariant:
    string: b <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 2ab1ba08-e3c9-46ae-b3c6-7c28ef94ec30
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 49
    column: 19
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 362c48c6-f01e-49d5-bdf1-56bc453ac8a6
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 49
    column: 19
    function: main
  loop_invariant:
    string: k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b362c1c6-ab09-4b55-a45b-e2fcdc2a3965
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 49
    column: 19
    function: main
  loop_invariant:
    string: -1LL + d >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d9cabd5-984e-4fc1-9086-1ee97fb0ee92
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 49
    column: 19
    function: main
  loop_invariant:
    string: (((0LL - a) - b) + (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e7a018e-6e14-4ad7-a226-8b8675ed797a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 49
    column: 19
    function: main
  loop_invariant:
    string: (0LL - b) + c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ce4af1a5-d8db-4eb3-b9a0-8f39894badc2
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 49
    column: 19
    function: main
  loop_invariant:
    string: a - c >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e127d3ba-c1be-4cc4-88da-1abd9e92a563
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 49
    column: 19
    function: main
  loop_invariant:
    string: c - v >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 040dacbe-f96f-4d79-b1cb-94e030b8e870
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound2.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound2.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound2.c: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound2.c
    file_hash: bda512f5ab4e84c08e80fd02a1c07c8fba5ca60aa45d55edfde2cc268dd1288e
    line: 49
    column: 19
    function: main
  loop_invariant:
    string: b != 0LL
    type: assertion
    format: C
