- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7609542c-39ce-4651-8388-951523db5b15
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: f9c9d2dd-2594-49fe-8ff7-202ba55200e3
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: afb01ac1-b06f-4af1-8cca-f142624716d3
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 781c4b1a-20fd-4e42-a272-5be30c5213ca
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 8fb980a8-c89c-4fb2-a52f-f4b8509e44d2
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: a1814b31-9ef8-45e4-a81d-46d07ed751e8
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 3891963d-9097-4121-851a-89da587d8f87
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: a58e9ba7-913a-4908-bc0e-85fb02b01790
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: dd5ff7d7-d125-4759-81a6-af448a33e047
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 231a73c8-a0c3-46bc-8b1f-7676c53b0d7b
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 3576a04d-b8dc-48e5-bdf9-917f324bd119
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: b9dbc7e0-ba19-4481-9926-8ef340212494
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 37b25f11-b72a-4936-a088-b85cbfdbe23b
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 4b383669-3f0b-489e-965c-2c6470cc00d6
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 90ac65e2-7ff4-492a-9944-8141b3015354
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 7a01b3da-e20f-4268-acd0-b7757014bd97
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: b4fc9c70-1499-433d-91d6-22a97869c01a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 08ab66ee-6b5f-4003-b9d5-a2417f0b87c8
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: c7221cda-439a-4927-a5c5-af1e8b68694f
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: aa9b8217-0a5c-43c2-99e5-bafde65f49b8
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 22f0ed5b-4d29-4d9b-b59f-6a8a09bd4e2e
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 8ecabed3-b98f-4ed5-bfdc-a1d302033c8a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 7b7377ae-b7b6-42fd-8d3a-273a1744d00c
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: e7cc370d-6291-4614-81f4-1751947e22bb
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: cc00732c-6227-4d6f-bfa0-c69f357c2461
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: f4fb5ba0-1b77-4b3d-ac4e-dd0f99bc483b
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: a9b9b1fd-d2fd-41d9-a91d-e10d107f2ea1
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 012bf0f7-de57-4108-af90-b28f550b971d
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 4a354b79-dfd6-42cd-bc8c-5943ba32c8df
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 9d2f06b5-10d2-4342-9c27-41317f80b6e3
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: d45619ea-0acf-42fa-8647-e26a8726eaed
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 4951d139-4985-4d21-90bb-e1c5579a51c7
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: d0053d85-7341-49c7-91af-9fb120e42e9a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: a814e4b0-e2a6-4af2-8e19-7f35a7f65562
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 89ea1260-97dc-4f8d-a3d3-ee2b21d86b75
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: a3e0f3d7-912d-4025-93b1-98d25cbd5fe0
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: b2dfd081-7290-4215-af59-ac11e19ec0c2
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 9ea72c3e-24cf-4606-b767-662dcb60f7f8
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 63f2ffc7-e494-4ba4-8803-f46305ab493e
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 7ccfae10-f4ba-4e83-a76f-003fd4b1fd86
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: f191fb45-fbe4-4dac-9cbe-1dc2526fd504
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 42cce28e-ebc2-43d0-b7d9-0f9138bfca4a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: ba3135f1-2856-47aa-b32d-72f1b04665a8
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 95c8e127-1b6e-480d-88d4-6eb4874a5e65
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: ac0deb08-d5a6-4dbc-9afe-13dfaaeabf67
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: d528d2fb-668b-48ac-82c7-a9a990d8b249
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: b8676bc0-2329-4771-b1ac-7d7b1bdb1333
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 8be41dd2-3e73-4b90-a344-6fddbaae55fb
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 5bf264df-5504-490e-8e90-bcd1f8d2d2a9
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: df9aae57-ad76-4ec7-811e-6285d919fac5
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: d63473cb-01a6-4698-8444-a7e6d2c5d131
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: b9f99b20-24b7-479d-a425-a9801a198895
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 10165e4f-532e-448b-befd-380fe53c5566
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: ce640885-0d74-4685-8e6c-e570f5b54163
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: f1c34596-0dd3-47e8-8129-73bd1707285e
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 91b738e5-6f55-4408-b8ac-8a93c94c3f41
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: bbeedbd5-9bfe-4478-89c9-4f40d57fa21c
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 8199cd7c-1dc5-4989-b9d0-340d4184974d
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 0c7a43ef-54d1-40d0-a797-9d55b8e750e0
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 99587891-ba0c-458e-859d-305765b8459f
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 05fe0b49-71bc-495d-b92c-356d038daedd
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 00930a59-b9de-4c7f-98b4-fcec7e5065fb
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: e73a56de-1293-4864-89c1-a70fe468c46a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: bc329fce-ecfb-4a10-a71b-fe90b57156a7
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 5fb2f4aa-87b7-4d71-bfc1-b6428d53ad1b
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 3ca4e626-664b-4f79-86e4-7f4cb5377cc3
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: cf563cf4-6d61-4e5d-921d-47e4f581a744
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 69ccecc7-2e09-4dd5-8682-2ec2897c9e9b
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: ef947c4f-581b-4873-81e3-c777022c9a31
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: dbe4e8b3-8770-4791-8284-9953d3e5dc95
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: d8ff0ff2-6c01-4a36-b225-e8cd266f912c
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: bd195181-15a3-4e67-a892-80e6e70cec92
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 98565a16-101b-4767-9722-5e4f9c9756f1
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 977f9d43-df7f-4627-a6f0-b0e866978df4
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 45ce30b2-8178-4052-8073-19089939c3a9
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: f7e34997-6ca0-4421-a749-27e511ed10ef
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 023af909-665b-4b6c-9051-817fda1f32ea
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 5b8393a8-87b2-49d5-a032-ea5b8802872c
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 535f3561-8563-47ec-8d92-4939acdae037
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 4386adda-d7b8-43b6-a8c2-479bf2dc6a98
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 5dd90ae5-55a1-4c42-a306-12ab46ffe62e
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 91a9d3ee-504b-40c6-b791-88e76f96763e
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: c8087c88-4f9c-477c-83f8-db4e398e776d
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: bf401970-93ae-4214-a1aa-101dcf81b979
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 11acf1a3-3eb5-4c95-ae75-14e3f9e0c6a0
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 2f065ae5-0726-462c-934b-d2c45b81799c
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 567c36f2-45ab-4b17-a39f-c83418ffb635
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 04694595-0f2f-4252-90a2-cc266ca81d5a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: d4c1d774-902e-4c4d-a882-86da80dedb65
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: c7cc9d21-c67c-4a5a-9f26-f83656eb1407
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 0200e1e4-83aa-4445-9401-fd2268f16092
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 1c7a072a-5cfb-4f38-990e-38cd91d1b28a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: fb457444-cd81-46cf-93d7-33100f5fa256
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 7f3ea68f-b8e1-4012-8608-0b94db5a8ad9
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: c39a6e4d-5586-4f78-ad3a-3f5251088efa
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: f411d47c-0b53-49a3-a83b-914020d913f7
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 420d0500-0807-4609-b8cf-7c235d7e8c04
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: a50e041b-c0b2-4a30-a3fb-c37526377dc7
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: b2f3128f-55a3-409e-b76f-4e0b44dc2e69
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 6c181bf1-ced4-4be8-b93a-68ee88e96141
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 5ba6aeff-60eb-43a2-af7b-7eb2902a6d58
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: a3faf2ea-957e-43cb-ae0c-50d2a382bdb2
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 2e71ef77-6900-4234-bf16-3fe2604ed3e7
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 884a06fc-db85-48e1-bd97-e6300a23157d
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: f505a239-acf4-4ea0-965d-ae1e4ba98f1d
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 0d0423b6-6da1-405f-8909-14468c708883
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 4c5311cb-b101-42b6-9c9c-7cf79b57cd87
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: c065b8b6-02fa-4dff-9b64-fbf269ce5fa8
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 71c1aa3c-31a2-4a98-8564-c4973c764828
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 88db5e0f-a0a9-4181-bf4b-d4f0dbc26d73
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 819595f1-d476-422d-98e7-5c87e697888c
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: eec39bf3-640e-456b-80e9-1f109a3ebce4
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 307eee47-e98f-49a7-90be-518940ffa54e
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: eef80126-cfb8-4be1-bd18-39f2c549c651
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: dff21a69-9d30-423b-88c9-88ca6ee7a4b9
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 3e2eecbe-8753-4bba-b8fd-578f967d8df9
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 8a77fa3f-0337-424c-abde-8a7c73cd1c6a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: cfdff7c8-759d-4fab-b101-8b658577d621
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 884adcd8-80e8-4139-954e-8b902820e5e8
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 1a10a927-2aa4-41c0-8133-7d6355af36ee
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 4c2d79fe-92c4-4807-92e9-042ea54b45e2
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 3d4f861e-0363-42df-936e-b04ce4ef2223
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 85bd4b83-dc08-43aa-82ec-566378c93558
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 55e8812a-c987-4777-9f34-ef31428a09d4
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: cb1a53c3-1995-4fd7-8f99-212614d5557a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: b9db2e7a-add9-4e66-8af3-2c8fa2640c0f
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 671c80ef-b4cc-4da4-b190-1ca67f82c69e
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: d159b97b-52bd-4f77-ade1-ed48e27d5b4e
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: eb025c54-33e9-4836-94de-931272ce289a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: cea2cd25-696a-4c5d-9d17-130b5d0f272b
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 25e41ef2-44f7-4e83-a14d-124eefd06302
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: b2a7b39b-6ef3-4588-b096-de8f9878ed84
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 475e2686-1fe3-49c5-b123-7d01750cd4a2
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 4f5c4763-36c2-4826-923f-14f559b7773a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: a3360514-cce3-4dcc-8867-d86f201e1846
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: edb46d9a-bc62-48f5-9b02-8c8c2be85dd7
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: ce06cd9a-91f8-4955-a938-240cf0765cfe
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: df1ee993-5c80-4e57-a7ff-0f4716616a37
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: c0dedcc3-b0e3-41e7-a700-d11c06fb60c3
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: cca5428f-8f30-4d9f-bd14-5642b1e22df4
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 39dd3cc6-9f6f-4067-8ae3-f6ebc4e7ab4b
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 482a63ea-f964-4d2d-990a-754af25c022e
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 077ffd4f-75c0-4a2a-ba28-d7d8d09cfb74
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: aa5c9779-3ecc-4c70-bf80-fd62741c18b9
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: af93bb37-159f-42f2-b3ef-f7c85a888a40
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 01fa94ce-7126-4f57-86f7-081b357448f7
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 1fa93fbf-999f-44be-aba2-fbfb0edf319c
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 7f5289e6-bb5b-412b-8632-8947faeb8cf0
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: d04c3a9b-db7d-4593-9174-d0803e383808
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: bf53777d-0d7b-406d-843f-9d7b86f8d037
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: ec5e8a40-23ec-45b8-af29-f547a1daf14e
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: c91da7cf-9904-4230-aa55-1d4abcf0c080
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: a3218a03-a3a4-45e0-9ea3-14019558073d
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 451b2fd9-c749-4d1d-ace4-320403262a6f
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 394d6547-8b06-4c0a-b55c-7b12e9ec8ff7
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: f39bcced-6816-4e68-a4fd-722d9a2516c7
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: e13141ad-d0b0-4e94-ab1a-f5c25e69a598
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 0cf89986-b746-447a-9e3c-001664fc6c58
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 36d3b9a1-dde5-442b-acd5-2d249e008c85
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: d6896ac6-f6ac-4374-8f3c-1aac226b370b
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: ccc2fd9e-5ae0-4eb6-a0ca-a376e273ee20
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 72560a45-bfb8-459c-9e92-0bbe9e4d29e9
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: f4e409b7-cb45-4cd2-a825-cee5d6e582df
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 4fba8b1d-9b3e-4875-925b-5b98d15821a1
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: ae7351fd-9a03-41ac-b1c1-182bd8535a0d
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: c2d28b1f-1571-43d6-b952-28882507351a
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 23a703c6-2b14-4218-b358-53dd64c995a9
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: ea52da24-27bb-4ac6-91d9-ad67f1746b37
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 46e11990-9c50-472c-8a08-46d689ca482f
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: c1b253f2-9771-485a-b470-6cabf95b2357
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: fe2a9775-6afe-4f70-a0d7-1d55e48352e3
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 2fd0845b-2d6c-4cc5-94df-143a359c8446
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 9970f57a-66bc-4559-80be-1fd2f6a01b4e
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 8a8ee08b-1e20-4cea-934c-89bab093efd0
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: c9f1da5f-7c58-4a0c-89f8-abc2d99e142b
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 00a359b6-4d57-49a6-9959-8a8b48c0ff06
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: f7290b04-4008-493f-a9bd-26f6fc2493fe
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 858a8e06-fc98-435c-af85-bf8c44dec3de
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 69997aca-97b0-4d48-9740-6ad8af94392e
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    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: 6a2f6315-2b31-43b4-9626-66bbd65302e0
    creation_time: 2023-01-27T16:29:28Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/egcd3-ll_valuebound1.c'''
    task:
      input_files:
      - ../plain/egcd3-ll_valuebound1.c
      input_file_hashes:
        ../plain/egcd3-ll_valuebound1.c: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/egcd3-ll_valuebound1.c
    file_hash: 40c004ecbeb3948e318f4c5fc8011bd289b059bb9dbb2959c45853a9680cf20f
    line: 49
    column: 19
    function: main
  loop_invariant:
    string: b != 0LL
    type: assertion
    format: C
