- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d248fef-6e27-45b7-b6f3-843a54ad4c9f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 6cc54241-1372-4957-ae59-c3f8d573ef00
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: cdd2854c-1e32-4713-8e0f-006e506d8221
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: dfa0c741-d12b-43e5-89b7-5646ab824a83
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: f7b07492-c268-427b-93ba-d10712911647
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: a5a134aa-5dc7-46e5-9ac6-a0fd21b7bc7d
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: eee0ba43-9d26-40af-bb36-31c83585fbed
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 7068371e-99eb-4b1a-888d-1fb4462054db
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 1719b3c7-9ba8-4eb6-95c4-8271762194ef
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 69b6320c-701a-4607-97dd-1bfee93c74d4
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: ba83cbfa-dd80-4a61-81a7-7d86fc654b81
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 646be6a2-105c-4f56-8d51-4c111b4e3fc1
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 2643573b-f42c-4d83-9ef6-e9900ca5b436
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: d7c0efbf-8669-4d32-89a8-eb82dd8c5368
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 167ce057-eade-47a8-a753-ff0b7005c3f9
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 93a0f5fc-789b-417e-892a-ec17efac0431
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 2c767b5b-e192-48e2-95a4-214bc934377a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 3a62b8bf-080d-4954-9a47-8d2487d11009
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: b2295329-dc42-4359-a581-4c343d0adee7
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: c14f479f-5c98-4a7b-a24b-ec921e0d0dcd
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: b91e402d-ecfa-4663-8ec7-faa43d3c7644
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 6d7d177a-7e76-4a5d-a320-190627527270
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 749c7ad9-86d7-47ab-8532-dff7bf6f848a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 6cbdd16f-56e5-424b-b7ff-f6da5332e1bd
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: d2c9a76b-b0bc-405f-ad84-2ee15ed984a5
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: ec639e0d-3a26-405a-b2b0-9790bbf15b18
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: a16d03a5-97db-46a7-b016-e777b6a7ba6e
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: a6bac7b4-5eaa-4e62-9f23-98b0e94d31a1
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 9ad26227-a587-4732-b2ce-64d4b9b00fc9
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 3fb4a3a4-9914-43ba-a8d7-316c3c01a93b
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: a60dad6c-2640-48d5-83fb-a8e3a23be82b
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 2fc4572a-5099-4a71-8f01-210ceed3fbff
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: d1957020-ec79-4ef1-a9b7-f4bc3d39dd26
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 2d0b4b78-419f-4a5d-b491-895be3074b74
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 945e9e08-2948-4177-9fa4-7e102297ca77
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: db92cfba-6460-42ed-b01d-43b7360b08e2
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 8e9f8eb3-47d3-46af-bad6-d774b79a3ebb
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 9b99ead5-5b33-4ce9-ab66-80eeb7c8be5c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: baba0574-f41a-468d-8e0f-12aba142fade
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 7af9b461-b0d2-47a3-bd0f-04214b3a73ac
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 82284239-f8b2-42b6-b900-7af4e07fcc5d
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 8785c343-b90f-458e-b660-09dbc07ea562
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 2da670c5-ef27-4929-8549-f4b2c4ab6bb7
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 085105d2-8564-40ba-8613-2899a4b9b0de
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: fb67ef37-fca4-46bb-9a85-a4d2f219ed15
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 853da47a-22fd-4dd9-a754-51b0319beec2
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 403fff25-8da2-462e-b216-f65c3785f5c2
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 5dfd152f-cd96-4cf5-af8f-e7f317a40e7c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 28fcdc08-02a4-43c1-a456-a82501bd5821
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 2772de6f-4520-495c-ae95-766eb56a7f83
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 2cd8cf5d-18c2-48f4-930b-a9e6d0de379f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 7d3e23bd-3557-4a24-9723-77cd35d18e8f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 73481499-f80e-4eba-8ced-ab0cd7740e9a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 33690936-ed3d-4d5a-8216-8bb3549369cf
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 0fcd18ea-8141-42c1-8915-cc59fb61c6df
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 4b893f63-6e83-4e25-93cb-c433889053cb
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 1dc163a0-facc-4d27-806d-139f3d44e293
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 83de48ab-cbc5-4bf4-ad4b-4d755afcc9f8
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: dd8c38a4-15ab-467b-bd88-f6b905502953
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 4696543c-6bad-4e09-8144-e68a17481076
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 8d415b82-1239-4235-b017-b82dcb36bb7e
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 01b8a79c-a101-4460-b27a-2c169ca35f27
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: ba096fbd-f6ba-4dcf-a51d-4400a3e41fcd
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 48dc4321-d757-4e67-98b9-710623c280f4
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: f7617315-7a76-4eff-a92b-3632dd891cd5
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 3c20a131-1896-4f01-8881-79563f484af7
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 56ff22f9-afde-4aae-85dd-fd649f488696
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: bf3f85a7-b274-4bc3-b40e-15fab770fe2f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: ea052368-d534-469f-9b42-083b7840d79b
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: fc599fff-f1ee-4486-9c5f-4e12bfc13e76
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: d08ac81a-cd20-461e-a0be-5c9b437e4b53
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 9f1628d7-32da-4e5e-a02f-4e2b4cb0ffbd
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 69afc7dc-a024-4372-ad2a-0bc579a1abc6
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 45a0f16a-3640-4584-b0d0-b8d7b1f90585
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 550c1718-dd7a-4fd3-ae8e-a6b265cada6c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: c3fdc116-d415-48ea-8e1d-25b73cd81294
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 7096ebf6-a25e-4b1f-be4e-9a61fda4f23a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 8c529083-c606-4183-9410-d8cfce96c2e2
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: b3fdee0b-623c-44b5-97af-3956e27bbaa9
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 95cc45a8-7526-44fc-a078-48bb48f99c4d
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: edde7642-fe05-4ba0-bb3c-c9df4d68ebdb
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 9ff77cc4-cae2-4224-a892-727a61a3fd8f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: a6aab640-c9c5-4944-bbd2-ac3f9a4a59bb
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 67ea6559-f3b4-4de7-bef0-11448a797595
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 1583241b-342f-4ba7-b432-f58e61336d67
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 18b68bac-a9c0-4b6c-b204-cdacde128cb5
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 694b0aff-b28c-472f-891c-2b4679a1e8e1
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 5072009a-9adb-4dc4-9118-7d888f17749c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 86e2d531-71bd-4ec9-8ed9-9d0ea1431e7d
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: fab8fd70-4ca2-4e17-84a3-ee2ad38dee33
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 1062ffbf-f84a-4c07-8bad-77667bee2baf
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 5746ca77-b491-4269-b7e6-893552358dba
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 2aad2a36-16ed-412f-bf45-ff977dce2809
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 888cadac-3bc6-48f3-996c-88f9b2c7dd4a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: d686a7d5-d58a-4729-9c62-cf1464177536
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 1f00a208-ed2c-4a2d-837f-97ab04228f3a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: f1e979c1-0bc0-4d34-9ffd-17c68b8ae930
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 91fa854b-f956-47a2-bbd0-bcb25f2b2e34
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: dc2c28be-4706-4002-832f-6ac0d416061a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: aaebbcc6-fd6a-407a-8715-64000ecc1230
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: c203244d-d349-4fea-bc78-7967355d0598
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 8598fcc8-f8ec-430a-b59a-a4a5fa85dbb3
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: e780ab5f-9e0b-4a33-b5f2-496e4f4d5646
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 24dec6bf-1073-477b-b73e-56234e8bd968
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: bec0d98c-68ee-41bd-99b4-8eece1319b1f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: dca0b778-c147-40ed-ad5f-3a7c797b6044
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 1630e7df-f050-4579-9252-e1a17d9bfa6f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: ef817f64-a4bc-4b03-83f6-04e8252f8c2b
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 76ae2337-7a02-401e-a56f-c8ec51759d83
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 1673dae2-25cd-4fc2-8a3f-dd54136d3768
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 9754cf8c-be44-4505-b97e-52ccc25af511
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 62236126-7401-446c-9c3a-c15295978f11
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: f3dcc5ef-28d4-41ef-aa8a-f51e4d676d31
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: e5f0e939-208b-4e8d-a196-067445522b6c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: c709e932-bf96-4c97-87b8-5855bd53aeba
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 414453aa-dbc8-4693-99da-5bbb210fd832
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 050953ff-1517-4f87-b21e-7f6bf7cd3107
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: f5415e27-14b2-4f96-86c6-e227b85c3705
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 8c930064-8182-45f1-941e-d9eab024a178
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: e1df5c24-6bec-4645-b48f-5377e87b11c9
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 2fdfbbc4-2fb6-4ef9-97fe-73d8cbc58625
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 460f57cf-0298-4bc3-9059-1b639db6a033
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 3f560b41-7d54-4661-9b50-d8d2b3160a09
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 20e4e9dc-6a32-4021-aa9f-a7aa134aa6e9
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 25f6bfca-b38b-4401-8618-8965642b0c1d
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 69827215-9ff3-46b8-ae23-45974ca726a3
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 6b0d1fd0-ba84-4e63-b80a-129a2083a4fe
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: a22e4226-256e-406d-ae21-174051e996a4
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 9275e477-6abd-43d6-ad43-378f083501b9
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 999c4f96-656c-44d7-b589-0b0450cc628c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 9ac9f25c-61ac-4e29-8843-df620005752d
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 40fcc134-b228-4107-8e9e-6778ef0a1f72
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 7cb25a3d-10b7-449b-9e14-a0cda7c84454
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: c9547bf4-ab96-4592-bc75-462dd52d4d5a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: d588c45e-e016-44ab-9e09-657d57814cf2
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 27afac59-50db-4998-aa7d-f545ee36226d
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: c20e46a8-68e6-480b-9c85-f1bf8f86a0a3
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: ec3a1617-b746-4bb3-a9bc-3aa3beea21ee
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: c4a0d8b2-d7c8-41b7-a231-cef965896a4c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: c7c9ed37-bf38-43b4-a2ef-cd2a7e7b388e
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: e0f68759-ee30-4b2b-b96a-22c55931e2e3
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: d6bbbd72-1059-4c86-b293-ba107efabe1b
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 706994ee-c06e-42a8-a706-4e7374fcce01
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 14566313-4bcd-46ab-89cb-e67b6403f812
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: ef42f6b2-4c6f-453e-ae4d-0fdb06fc44c0
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 48d56723-aa04-4adb-a1c8-9d2d474f8870
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 613dc72d-4763-4ce6-a66b-266b5859f7c6
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: b4f29a7a-24a4-4077-a995-4a3f2341c221
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: a3564472-20db-4995-bb7d-a956c538af62
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: a1a2f5be-2d2c-47b9-a97c-9ba23170f6b0
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: bddce125-022f-4e57-883c-3d7dcb8a0795
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 35b7498c-c398-445a-8314-27a322cf162b
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 5d2c04d5-4d20-43cc-bfda-1d05ea201774
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 6630989b-b309-4b35-872b-f2e409471725
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: d07766b3-a111-4d21-b3ec-c1f6e1ac3cd8
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 99a56d41-ef64-42e7-957a-3b7a8397f2f1
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 4a860ee3-86e6-4cf0-afca-cc8f838cfd3b
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 69d2dd60-feac-4881-9a2f-bfc36c808ce9
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: be1d3fc7-50a8-4838-bce3-6aecfd5ec80b
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: cfcacbcc-5073-4523-8631-b38cf02a976c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: c6c7537d-a592-4f60-a61e-add21d32f392
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: f8b40ebb-a79c-4194-8a2b-a25846c68218
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 25a97be0-49a7-443e-909b-0daded9ba6ae
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 4e68d545-20fe-4833-97d9-ca8819e0c6e0
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 071a6b5c-d148-46fd-807b-9a2fedb1ed22
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 94838a7c-6cdd-4b04-993d-35041360afc8
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 2f122c06-b7b8-4b6a-b420-ced5a144cc0f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 351962dd-3bf5-4ea2-8172-692aaf2e4182
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: fdea8b91-a728-456c-9f79-66fe078e3dd7
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 49cc6f29-b97d-496b-b503-6926d7295425
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 86abd3e5-6ade-4a7c-8c02-fc866cc5c759
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: afea1006-291d-40ef-828a-8ae35a67f4a5
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: a87d66e2-b9c8-4397-96e2-5ab8669472ba
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: f7b8df17-6309-4b13-9fd7-025d6005e75d
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 8fea6c56-0b8a-4dc9-8c80-f3f39246dce8
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 5af1d9a8-9db8-4726-ba35-18a9f01a1efa
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: e8a88ef7-17b1-4aed-b4a7-139b155c3135
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 056c9cb2-a1c9-4f76-9449-ebc52ccfbc6a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 32bf1582-b95b-4a84-b52c-32cc918902e9
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    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: 61a57e82-6008-4c7a-badc-6f08df908b37
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound20.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound20.c: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound20.c
    file_hash: 39b854852f8258ff198098e27d83a5b0e296df48090ebea0d59d234417af0752
    line: 49
    column: 19
    function: main
  loop_invariant:
    string: b != 0LL
    type: assertion
    format: C
