- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 69e595eb-8eea-4947-a6b0-f49414e4e159
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d6981a83-b0b2-4c8e-8bb8-cfded74389b7
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9266241b-a14c-43db-ae9d-9eb861c314b4
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 04640b15-c2e0-4c11-a07c-fbbf976c6f49
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 34
    column: 4
    function: main
  location_invariant:
    string: y <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d7a527b2-c085-4444-884d-2233a9651200
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 37
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 130966b9-f7f1-4609-8d9d-9496457e11f2
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 37
    column: 8
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb22bd63-8f09-409e-a948-30ee90998b63
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 39
    column: 12
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f4fc2893-72c3-4607-86e1-9c004377ca5c
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 39
    column: 12
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9df05c58-989c-4e5a-892c-b3418635027e
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 39
    column: 12
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cfcec49f-b3db-4e64-a7b4-d89f342e9fe3
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef6ee760-d079-43ab-bb35-af9ca98d8a67
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 42
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79e5600a-9850-480d-bda8-e6a8b178809f
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 42
    column: 8
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ea8ab790-d36f-44ee-ab47-d97c20748a48
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 42
    column: 8
    function: main
  location_invariant:
    string: (-1LL - c) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0eca5e0e-9e75-4d5f-8510-62ab426004f7
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 42
    column: 8
    function: main
  location_invariant:
    string: c != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dac00ab0-b23d-4859-af14-9803c41faacf
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 43
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ce237677-8f4a-4fdf-a600-fe9f5d3eaf34
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 43
    column: 8
    function: main
  location_invariant:
    string: 2LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bbec2da1-66d9-426f-916d-0e457b2da99b
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 43
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a8a6fec-746a-4294-81e0-800539803815
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 43
    column: 8
    function: main
  location_invariant:
    string: -2LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 619c2982-fd7a-4f94-abb4-0cfc8a50437d
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 43
    column: 8
    function: main
  location_invariant:
    string: (0LL - c) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a39bc6d-62fb-476c-b7ca-289f9697b8c0
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 43
    column: 8
    function: main
  location_invariant:
    string: c != 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d6c58d6a-74e6-4327-b067-16e348c69ea7
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 44
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a43edf2f-f4ef-482d-aac5-f961aa8b2ec5
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 44
    column: 8
    function: main
  location_invariant:
    string: -2LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 171a5ac1-847e-40b4-800e-c0291f87dc1a
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 44
    column: 8
    function: main
  location_invariant:
    string: (0LL - c) + (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8f26e2ec-5ddf-47e7-aebc-43fc00f58b81
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 48
    column: 4
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3adf1179-3a9f-46df-b40d-dd3ff76c1782
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 48
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b3e7ebe-ebf9-4bbb-9776-93848e484c66
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 48
    column: 4
    function: main
  location_invariant:
    string: c - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ce42436-55d8-4836-8a75-e4aac4549a7d
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 50
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d941544-a5b8-4e96-a961-fe7c40271346
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 50
    column: 4
    function: main
  location_invariant:
    string: c - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 994f6004-8fc4-4555-8165-ffc447405e34
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 51
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 49b75724-245d-4f6d-9212-ecdf47943d7e
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 51
    column: 4
    function: main
  location_invariant:
    string: c - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8eba9bb8-410d-4df0-bd04-c87aa474f6b7
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 0 <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e147a796-b264-4efd-8c52-10a9bf590536
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 05a56e9f-d814-4e6e-931a-d2a91f70d689
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b897190e-1994-48f8-bfb3-78c98085595b
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b6c9898-ad3f-40f4-844b-083e66f44ec9
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e134cc3-f1f6-42e9-b431-3a970959f2c9
    creation_time: 2023-01-27T16:29:31Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/geo1-ll_valuebound5.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound5.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound5.c: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound5.c
    file_hash: 5fecc0272e3d3edda13fe6ca0a651d95cf8d16c414f426c1f8f27e509220a775
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
