- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dba0ad50-696d-4e30-ad31-0ef297d94823
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 83f52698-038b-46a0-9528-49721da2f9eb
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 81a350ab-2bd3-40e5-81b7-b679830a2abb
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: a4f5e153-8fdf-485f-8b6d-cd2f843f6bd5
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: dca496c3-bf47-4176-aff0-0a45dbaa61ff
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 7b1280b8-05e7-4a0c-b4b0-e2b5fd63d574
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 49903c1f-37f7-4221-a898-0172fd921e0a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: a3c6c94b-8ef1-4185-b9ea-fb44f84a3361
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: d9d9bf79-8ec6-408f-b23c-d306a2845f36
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: f8129102-b533-41d0-abc5-c5137d60ae32
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: efe26ad3-1ec5-4542-b553-d9ef2d0293cc
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 3ea044ca-7bed-4ede-a736-f50348bc0721
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 6e6a51cc-93c7-4cc9-885f-408eb5a366e9
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: a7adac46-f29c-4e30-b346-a8f06d0675b3
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: dc56f628-699f-4bd3-bcfb-93c4c0126a77
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 28dbdabb-d2d8-4e63-a0a5-3e2ca1708b7c
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 21450494-e851-4fe9-9ace-a7f5503dc6a2
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: e55c2b44-d73b-42ff-b613-ef4534881c52
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: bce7b4c1-f842-4c65-a67e-c31c588bc416
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 26c34e08-3c73-4fdc-b12e-7030e82c44a4
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 63c6f0f6-0b2a-47ed-972e-65ec78f46df3
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 5f5a34e9-f99f-4813-a426-b25fd340c26d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: ac1c3cee-c0f1-4d61-971f-47051764fc71
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 390d7ebf-f0f2-4d11-ba37-7c9cc992aa1d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: c4ffc415-da51-4eea-9f3e-eb64ecc9830b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 926dae63-2cee-44d5-8c37-07acef82af5f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 6d7f250f-99c9-4169-b7b1-6810d0d574f5
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 9b389be2-4286-4fcd-83c8-470777ef2f76
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: a7ca8a09-f477-49d2-a4d4-e0ad53cf2069
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: a759dd10-06c1-4235-946f-b6188f0778e0
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: e4e065d3-3b38-4cd9-9f08-c21a2718c290
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: edd1db8f-79d8-4e49-bc5b-53b9b0fb22e3
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: feb92a6a-79c5-4010-a6bf-7bc584a9e63d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 23122893-f98c-434c-a662-cdd5dfab05e9
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 5983eb50-bb7d-4815-b32b-f4659e735371
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: f26841a9-332f-43f5-b244-ac9b5b80a69a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 114ef955-0d54-47a6-8873-3f79f844d386
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 33103afc-6aa5-4001-a62b-41532b2931a6
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: b31bb5e3-fcb0-4c36-a442-0d24366bfbfa
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 9808c038-06a0-4a53-a8ce-6d05b69c0949
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: c242f572-89ac-4c8f-ad2a-3415bafbd57e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 40524cbf-a479-417f-823c-f1ff6bc47aec
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: a06ccea9-c7d1-46ac-b368-a75d243ba3db
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: cb4039ad-89ff-42ff-9729-21dbafea3c69
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 64b80f45-1542-4942-835f-7e1122b9371f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 507e02f4-c33d-4244-8e31-94b76ce15727
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 01b2697a-7624-455e-9fce-582686b4b554
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: d7ccb78e-5fa0-4c61-9918-b9e43436d3f2
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: a4fcce84-d773-4cbb-bdf2-12f693d087ca
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 44f713b8-3dea-47d1-b7cb-0c22608cbdaa
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: d8711e99-beaf-438c-91e3-af4f151b1b6b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 096278b4-07af-488d-8fee-714beb8f93eb
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: a179cfb8-56e3-4cf8-88b2-15543a1d9972
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 72c1bc79-9489-4243-80c8-47af3cf48b10
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 99330c48-86ce-4878-8301-9584a2fd2afd
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: ef823295-0c56-48fb-bb9c-68e2edc54c7f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 132904bd-355c-4ddc-82ef-432e5091ad3c
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 271d4b81-d89c-4205-98d6-07b27426f83f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 5db85729-d96f-4525-866f-9cf2e74b172d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 3f6f1804-9930-4a1e-8f87-9c275c183707
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: de07a93c-71f6-4412-8f52-dba861213a4d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: ff6e4d6f-41e2-4a19-aaf0-0540b283fa58
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 53e187bb-30b3-4b47-8c24-ce2edbd3ba3b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 62b66dd5-732e-407d-aa8b-b252102546e7
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 5c013bcd-4ce1-4d6c-b5a1-b7d5ab907bf8
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 9e60fc83-f5e6-487d-9d9a-c5b2299a5859
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 2b8a4977-14ff-4c22-b00e-5f1040a104e1
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 3c7603a2-a4a9-4f4c-ad31-26494097feee
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 3076f2e3-b924-41c4-b306-bb0099f4181b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: faf38895-8fdd-45fb-96e2-ca6d73fe6f3d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 75568865-9a6b-4de6-9dd3-7da0fdcf0db3
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 3f008ac4-d1f2-4698-8847-c239fce6d876
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 4ec894a5-cb2b-4083-b704-0569c0e20a99
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 50c2b8f2-a6b6-47e3-9cc8-77800cfaed7b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 68a58f0d-ea20-444b-8b45-d71b17e05e80
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 6d1c8dc5-406a-460b-bb31-95d18e5bec6b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 059e1114-4c6f-49d8-8b34-3190fd17f656
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 2e3df1b0-1489-4bfe-b7df-51ac87633add
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 0aed9cf3-6c3e-4fff-adfc-51dd449c4eaf
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 2b0f3b43-7cdd-49cf-abad-71f4616c9527
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: d36f51ff-346d-4dfd-8acc-ebc5b8d59a54
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: dbd6ece0-b6f8-4bad-a314-e8b82e65f041
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 0c6c69cc-6f04-49b0-9293-311231185d74
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 4f1facd3-081d-4a48-8219-8e74a034ba20
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 8e9fd0f3-9353-4ee0-9b35-b690094cdcc0
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: b9549442-f95b-4191-b5c1-b4d3c4514be2
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 0f44d999-b0bb-4315-8966-02dc5b47b524
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: b6f206eb-225c-4dbd-a7eb-29441200a285
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 227ff4c1-80f2-42b1-b04f-56541b95440e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 66614e3b-8cea-47bc-a705-6f1a5e2ac94f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: f72fe7e5-1bae-43cd-a941-c5cb97221a31
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: b930b6b2-8901-4c3a-acc6-47697a8a6819
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 15b9bdfc-fad1-4855-87c5-a3c89467cd9d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: cc901e86-620b-4aa4-bfb6-8dd81c428586
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: fda428f0-8711-460a-859a-8020f08a0b3c
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: c6ad0052-f5a1-4e28-83c2-a0540fbbf71e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 6fa4cd49-2943-4970-b9dd-629306170d7a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 33757141-e171-44c3-95ef-0302228f159f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 260c4e12-dc19-44aa-afe6-fbb2d7a3721a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 0c1d3f8c-1111-4e2f-bab2-61e9d1222d2b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: ebe7ff25-3113-419f-9d8d-8014f8aafe3f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: ff6b28aa-c9ae-402b-a837-67ee59c37140
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: a04f4523-2ecf-4875-95ef-8ae157edff1f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 1b33b12b-7043-4497-8ca6-159b846bdabf
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: ee2f5ea9-6e59-44cd-a392-a76e033e455e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 53bf0cf7-a450-4c94-b3ab-9162a2ecfd0d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 05d97238-dda1-4b4e-a4f3-b3ee9c3bf916
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 77e4915c-956b-4f16-baa7-11c43d7e09d4
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 9fb5c4e3-30b7-49ec-8d1d-d37d111ae8f6
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 2a2cac1b-0fcb-48e8-b456-3f467eb9059f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: f9dc1889-416f-4ddb-9e20-bbc564ca912e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 42465588-f01f-4b88-b932-d19ba33c56e2
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: f9798caf-a221-4a77-9414-092f4d7760dd
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 9b667fb6-1261-4bdb-8484-f60bfffeb55d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 120768c8-2508-4674-95d7-cc6da23e42d1
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: d1268be5-9a05-4cf7-aca1-72625a7d9cdc
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 4b5e5cf2-8169-4116-b1ed-004dc3a7b272
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 9a07236f-23f7-4fe4-afe3-d36ccf0c97ba
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: ccc64244-0ff8-46ba-9449-335152873e21
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: ff925382-9736-4aa0-8930-34439610faf5
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: e6898831-1633-4aba-ba7c-47b955868341
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 2dae0c68-68fa-4ab9-babb-c0bd063df588
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: e42264d8-4e7c-4b86-bbb4-3aac903d9aa5
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 9cecba3c-aa44-49ec-9437-0012314bd9ac
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 2a21f677-d9a3-451d-9b94-eed448320ab0
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 482896ca-b85b-4300-b06f-030cd3729967
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: d91cb7d1-248e-4d12-a6b8-a526d7c44432
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: c69fea1f-3076-4f76-8b55-fb067f686379
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 8a905054-465b-42cb-8b32-50f18347314b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 6b6c9beb-fbb2-46ec-8df3-77458a874852
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: ca3fefb9-b82c-401b-be0a-d8712affb73e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: f839ec74-3ec9-4b71-9d35-a3b7c489a314
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: c315113e-85b1-4a75-a8e0-4eb6bee20a60
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 2955f99b-ee66-45ba-8ae4-b01fe6388c24
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: fe6526aa-3a95-4b3a-967e-5bd6639bbd30
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 616caad8-453f-48fb-828f-a1b43caa643a
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 907a0fa5-f84a-4bd1-8027-3025dd4a0692
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 955b15bf-5e7a-4975-a2f6-6e9e0c68f8f6
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 7db4ebdb-4587-45b1-b6da-ac905fb72438
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 95f0427e-9b54-4f69-a021-b7ae68f84831
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: fe905cf6-61d9-4194-892e-0d9108e31fb6
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 8670d212-25d7-46dc-a74f-176fbaa0567b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 4974d7f9-b8d8-4024-882e-ee82ecb9ddf1
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: d6a714c0-e0c6-4420-913f-c92fb551b56c
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 274c180e-a352-459a-802a-38c5c0e52584
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 0f9e744c-2bd8-48af-a519-b03285525599
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: ba9d97ca-d69b-4ef0-94f1-7a4a6bb7f442
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: b1302436-691d-48e3-b74c-07fc2c62864c
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: ded61df4-d251-445d-a3af-47a83a5675e3
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 47a63797-ed9b-4e6a-9bbb-73a19e806ded
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 405d9da0-e76c-4387-a6c4-093e933010f2
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 1215d50d-004e-42dc-8159-e53b2293503b
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: ed09aec3-c26e-4599-b526-b359ac1b98e6
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 40b7a5aa-e9fc-4756-b197-0b6739c1d91e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 58f4b8b0-b7e4-4e1c-8612-1b8e649955a7
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: aa2ff153-498a-4631-be18-d42d7c59cf22
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 8c8b1490-8875-465d-9901-1dc4495c8f2c
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: bd8f6adf-eb70-4c07-86f2-c829c59c2b65
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 026c8b0f-73cb-4ebb-9c0f-767e5315f7f8
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 63bddd2e-8af7-48f6-ab98-440dd261cb1c
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 38c5e5e0-e154-4817-aa73-58d7b09b0352
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: ab044e63-175e-4be7-9c0d-9465ab04476e
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: db37cea0-8b62-446c-a8e2-5a8823b00485
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 7d36ba8e-52d9-4962-8212-244f9ee4b0ab
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 751c07ab-5588-405d-9f0a-d72149373e72
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 3bed781a-75c2-474d-8f9c-1277fddd4f79
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 744c8b80-0e70-4b0e-b7fa-2850efb1a0d3
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 88dd4d2e-8dc3-42b4-9418-7bad57f0e5d7
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 06fe96b4-233f-47a4-8b7d-2b8da7f7c688
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 1af14e95-a985-4443-8662-4fcc65394d97
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 27693a9f-a6fe-478e-9bee-cc77dc38f965
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 6837a937-cfcd-441c-a2e8-1a174dae824f
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: f47d60f2-63e9-4a69-b81c-047da52da85d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 7e0b632a-69b0-47a6-ab6f-1e483c2bc4dc
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 540ecba0-5070-4d17-9936-63ff1b104453
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 30a518cd-46d7-4fe7-b4b3-5c74ab86ffd7
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 8a841d28-defc-4fe9-9742-1100ecaab755
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 5cb25cf5-4519-4c4c-bbc9-f675d7ccbb20
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: 1b2d6523-0b24-4db0-bf7c-642674f4797d
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    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: af5b753d-2fa2-4acb-b2e6-db3717161cc5
    creation_time: 2023-01-27T16:29:29Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound5.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound5.c: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound5.c
    file_hash: 1aca3c96522e618238f11f200c96e0ec490e756d4e04895bd2a51f9a4ff85af1
    line: 49
    column: 19
    function: main
  loop_invariant:
    string: b != 0LL
    type: assertion
    format: C
