- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d49adf4d-eaf6-4805-baa2-08026ee101fc
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 9ff4760b-b74b-46e2-966e-a2781502f3da
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 54e73065-7ba3-4a05-9513-839648e1604f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 3e4ed72c-8780-465e-b34b-c67651c8cc5c
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 623ed113-0a7b-430c-b09c-002f74c10ae6
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 6c0eaf4e-74de-4b51-a20a-97b7d7a2bbca
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: eeda1d66-991a-40b1-a424-480a80d301ad
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: aa112469-f3d7-4aa6-a400-eaa768386655
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 40d8b16c-0ba4-46a8-959d-b16c10d59c4d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 9bf497a5-15c5-4d8e-82d4-b8ecdaf048e5
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 200b6309-69a7-4910-b943-6f1d978b37f5
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: e1806fbd-f8a5-4966-8516-e7597878ccd3
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 4cbfe5f6-9169-454f-b608-bd1d3a4a075b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 5c94b222-8dc7-4e78-b006-5b4349cb20b8
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 9da35167-5f32-40b3-ba56-6a20ef79496d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 098c11ad-fe12-4db9-9db1-c5ba487aefc0
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: bcf3876b-7f41-4b49-ac73-3eb21a12c961
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 28d01c57-1a8a-4a60-8d1d-ee7e96ba7825
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 74e50ab0-b2bd-47aa-aa92-530871f5938f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 5333f2cb-9f56-42c4-942a-79e21630e096
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: a7ac0450-b916-43f6-b233-eba9315b7cd4
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 8878fb16-f5b8-4cb9-b641-82c24851e13d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: db41f065-ec2d-43cf-9195-288eebb677ee
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 1321e01c-6286-46ab-b122-477b573884f1
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: c9b9acb1-72d2-4510-98b9-1807dc1e3f29
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 1a3316d2-9224-4c79-9cf6-c0fd19f33384
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: f8221d5a-ab17-4607-806b-dcb47c6594f2
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 2cc8daf6-f73c-4c75-9868-f7595c9484aa
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 190e9625-5c7a-4dcb-9109-1c3a2ce3f010
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: f6d303b6-d39d-4cdb-90f4-d9bc933c00e7
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: e224eda3-5903-437f-aa9d-4b0dd048e772
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: f2d5665b-ec2c-46c1-bfc6-0f37281c6eee
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: c3fcc3f8-17d6-4ffc-9cec-99c8b32da8ba
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 5e34cc90-b408-48bd-8d8d-651154aec54a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 85cb2b28-701c-43d8-8e7e-c1416154cc1d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: b1ca5db1-46d6-43d2-a48c-b6efd0f8eabc
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 0b1a13b6-b711-461a-8f50-c47db73e3154
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: d095473b-817e-4262-8757-096b4375c61a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: a4b620ab-f400-4d71-a880-cd50492e535e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: c7c87489-9046-4853-89be-24e1b9480d65
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: b61e9135-9fc9-4ffb-8364-f68612fe4448
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: b242cb6b-2461-4d1b-8ee4-21d85cffe343
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: de920563-0640-4194-957e-214b78e0fca5
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 0451d5cf-ad1d-4a2d-8f6e-182d0b3726fe
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 194fc430-6b29-4f66-aa82-6680d47b1d94
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: d729a5f8-3891-4768-870f-08a71f79bad7
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: b12fbd56-6567-43f5-b42b-80ef35ef74cf
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 6262646f-fadc-4a88-ad74-25809b600ab1
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: b8d96a00-1484-47c4-b85d-490ac2961293
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: ab5ca5a9-45d6-4334-822e-eb78b7466e69
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 03c7c8ae-df0a-4787-9829-4e4a3caf8639
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: d6b24c09-c96e-48f2-ab9d-870722060468
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 621af216-541e-4f72-9149-89ba887fdb79
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 4862a2dd-68a4-4f0d-9f79-feceec057541
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 2102e67a-8788-432a-9682-9cee688041c0
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 28e29ce2-c7ce-491c-aec8-3cc70267914b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 319355ee-ff59-4f19-9eef-124449c7ea13
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 3769982d-18b4-4bf8-acf4-eee4d37671f1
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 71ca2ecc-14cf-44b4-8cc8-4311e5e9c439
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 87537d4b-7626-49b5-87c6-ed0f3b95eb7f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 339e8ac9-47bc-4baf-86b5-73a539e365d2
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 4987b3cd-c1a7-456d-92f1-1c6c04ec5f3c
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 53fe4e46-5cc4-44d5-aa9d-e13311195bb1
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 602ec850-bdb6-4ea7-bd61-3da57d6eba4d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: b153454b-33d3-45ce-948d-cd7eb5498d26
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: f63b7602-db05-486c-aff8-c2a22f6e67fb
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 22627b31-6659-47d4-990f-f982b8da3b85
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: a465863a-870d-4be3-b3b0-baaf3ae46a18
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 87a5da8b-1603-4334-8151-b3cc71589d02
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: cd7bc036-4397-4802-aa86-fac0462781b7
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 3fa106f8-c96b-4201-9dfa-c0e5c8627d35
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: bac459d2-8332-44ae-8e90-791732a61a02
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: b38233e9-2323-4d95-8957-765114e5cef4
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 838334f0-c14a-4bfa-b524-ef22c2d3f0eb
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: d3468ae6-6291-4544-a078-40dfce2187bf
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 5256010e-af93-40fa-9dd0-64763b445c6d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 7bf37445-7c0c-4f73-92c2-2ea6292f5ac4
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: ae97a3e4-2ab3-48aa-9e93-2b43495445b7
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: c96725f2-0941-4be3-b0d4-dd35925abd2c
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 629af71d-9a37-4624-ac13-febf9647b7c4
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: c0673605-8a21-49fd-b0e8-8b0bbf676686
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: c360e83b-206d-4c1d-aea9-54e199c7d870
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 0632504b-77a7-49ee-9d0c-8684f4d4c42b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 054716a5-bbc6-4275-a282-29f9a710083e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: d73ac0ae-2970-4ad2-b12e-300797b12e7e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 80733146-fd88-4371-a612-78f4e11f4c56
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 161b91c6-16ca-4ef9-865a-867324d04f2c
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: cf799505-ddf4-4ab5-8ee2-9bcdd2832f5e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 940810ee-5c03-4cf0-870a-d34a56daddab
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 8a93f3f4-5057-45a0-9390-a4961484b2d4
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 84d868f5-d4f7-41e0-b73c-6e8dc577c05b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: f5e50691-fd52-432b-b4e6-148dd1df6768
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 1ab7113b-3bfe-43d0-8dbf-1ee9f44d3a95
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 5e5eae2e-f13c-4ae5-88e9-7a40d770abfe
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 37a5c048-c4d6-4652-8edf-2ce4b2e34c94
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: b7e62035-bd63-4ebe-867f-87b92756c992
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 4748e9cb-d5f1-4657-88e7-6fd11e8ecf1b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: cd76d2be-fcd0-488b-9958-d9960ae5ecfd
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 2ee2d52a-9406-44ed-821d-9a9092a21253
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: c09d4c56-bbb1-4f21-82fc-0f2c40551683
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 2e924535-f617-4cf1-9a54-7be5f3b08487
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: d96cb49c-bb18-4530-95fa-d14f45ff8683
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: b9785bdf-453c-42fc-8bbb-06deb84f4d87
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: d5d2b2ef-b1d0-4694-b5bc-ef884d27c39f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 335cec61-d312-410b-ac7e-8143f50a3c91
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 36f8b80b-6223-4aab-ad9a-de16aff380d4
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: c469f268-4fa9-41f2-8275-9fa27cd1af86
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: c4cf8499-42a6-4bef-9da2-880019601361
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 4afa6963-752c-4966-bc9e-1580c6ebd4b6
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 7a69a40d-67b9-43db-89cf-6a174f9290a0
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 8c3d6e8c-179e-4881-83cf-2249bed65778
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 7b233a61-eed0-4807-b4b7-9e948e8f9d36
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 5b41555a-250b-4da2-9749-7b42bb9e3200
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 60ff6092-15c1-4892-a6fe-acbf5bd851a0
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: e5335336-ac3a-46f1-af31-1cefeb3c4966
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: fb127adb-3cb7-402a-a0e5-3a36c5753ee0
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: c898d892-9f91-4149-b6b2-7c857e16d392
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 36e2cee3-72e3-4b54-9b64-70be33703415
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 6c0614ef-83fb-453b-aac8-93ae62db5a1c
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 87fad2df-748d-480a-b4b4-d629c5989c12
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: b609d3f9-9a0c-4a15-8f7c-a50a81ae7b8c
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: e8a37b83-2a18-445b-830c-da6ba311833d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: b403c135-87a9-4eaf-b656-30e0400c10b5
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 29d4cc92-07da-498c-b3bc-5e971f0ffc33
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: ab14f6fa-1bd5-4b70-9c82-a8dd236c0703
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 505092bc-a60d-4ec5-97a6-a9fa9f13742b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 8225e091-468a-4133-ba80-473f411b3e61
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 3d25357a-430d-4dd5-badc-94ec8af02b36
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: a31f21a2-76a4-4a8e-8aeb-195d8aa00656
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 7dbbb91e-58c8-46c0-a4cf-6d451f3aed3b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 882eac76-8983-4d0a-b0d0-ab9247417736
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: c50cdd44-eb9e-49ce-ad22-b3d12758612c
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 71cf2103-50f8-4ceb-9552-64a62359d37e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: e164f65f-acde-4c2e-a39a-3dd31da10640
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 540a5631-27fb-4437-be33-03260b293dbe
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: a76a9764-d78e-439c-93da-708ff3d94c22
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 3c8ce03b-d5b9-4e44-9530-2dea6fbf0b73
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: fd5bb25e-5367-4372-936b-e60964ceff88
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 9b51a5dd-122f-43cb-872c-8de4dd54c659
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 819e8e88-db9a-4aea-8697-f88424deea73
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 7cfb4f59-621e-4f03-b9f7-688b523d1c47
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: bdec250f-f41a-4576-84a7-3a2722b2fd29
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 192f2184-777f-4013-9cf8-6c075885619c
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 7d420902-acaa-483f-b8a6-cb258f3fd1e2
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: e5ed83dc-fd83-471c-96ad-6c934a2eea1d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 1e6438bc-c589-47b0-980e-9e1ca321bee2
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: a6ded9e9-d2de-4bee-a23c-8f8eea42e974
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 43d357e9-c1df-4e5d-8a24-486e17fa3495
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: dd855e68-8288-49ff-a4e2-65255c3b04e1
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: e7edd441-5538-47ca-90d8-37238420ece8
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 5981ca6a-c91e-40c5-be95-7cb4d14a7abe
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 5a193b7c-c656-4adb-a0bc-f24b61db2fea
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 6bcf7dbb-d2f4-465d-b07a-19125f417114
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: eba3a2cf-4ad7-4606-abba-4c787ccdd7b3
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: abd7a2e3-3109-418b-9228-543972a5eb3e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: f3ce96ae-eb58-4358-9d02-a55623660da2
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: ff4c5a08-4754-4826-88d8-bcd0389e6eb4
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 289d4a56-ec19-467b-8c03-e66aa73536d6
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 77bdf059-915d-4813-91f7-3cd7911350f4
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 329a4d4f-262b-45bc-8b2d-3d321688935d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: b9a1feed-2cdb-4fa5-910a-41c9ac74265b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 44c04165-98b5-4488-8181-d514d4efcce1
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 64bb4668-13b1-47d3-8903-477d3998f822
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: ed8320e0-6f3f-429b-b666-33816227d8bb
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 2c7aff53-08c8-4b6c-a34b-aa8c730aa145
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 0fcc7d15-cc56-49d1-a74e-7fe49fe21d55
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 8c2c7768-8d57-4943-8d2f-80f62da7dc4e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 17a82160-0796-4a87-8d70-724eba737688
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 097f21b9-a760-4ce5-9416-974bab7ca60f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 5de02732-157e-4bfb-8366-7c76f846cf56
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 06567271-a02a-400c-9736-059961321ed1
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 5ce73b09-f958-46c2-8ad6-97a0fbf318fb
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 621541f3-c42c-4cf0-8b0e-2d450370ce0f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 4b0ac782-bbd2-4a37-b30b-dd03aa0a34dd
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 620cb302-ef60-4639-920e-947f79be1567
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: d789f4b3-e8ef-4caf-9f60-2881da861e3e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: eb22800f-22c9-4533-b7ef-a9ffd5e79bb6
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: a5fd61c8-7493-424e-a328-d9a8043f784a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: 2ea3cbd7-1cd7-4c74-a935-9f49c9a0ba8b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    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: d18e9f02-b227-4b71-9fd2-6994b659a9b9
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound100.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound100.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound100.c: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound100.c
    file_hash: c3e4caaff40cd418d8c93f0410c37d1e421cc5f90c41578bfaa7bb16ff289f1e
    line: 49
    column: 19
    function: main
  loop_invariant:
    string: b != 0LL
    type: assertion
    format: C
