- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8e00dc67-d5cd-4bc2-8d35-2dadd5ed079a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 881c3c1e-18ca-4e38-8dc3-690bb7e9e32c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 7c284a45-6d31-40cc-b2e4-137079b57dc8
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: c7cb14d1-2bca-47d1-9e06-656d99088c88
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: e595caaa-76c6-4e6c-89b7-19f356a71551
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 4d40f353-dbad-40e1-9586-73d61fbd4ce3
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: ec47b33f-4273-4a0b-a8ca-a113f416e0e3
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: f77abab7-9397-4fdf-9721-9864cd1aaca6
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 54d7b8f0-debc-4674-8e2f-563d43619fc1
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 8e35c392-8760-4cd1-90f3-ca96fd63f3be
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 3ab1df5a-9341-4ce3-a47a-1a43146428d7
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 9951b0bf-15c1-4c17-8d11-db905c61f3b9
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: dfff7bed-5f7d-4a7d-b705-dd12818b0021
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 5a0c9844-e8eb-488c-a178-ab479b4ddf95
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 6c72a81e-0383-4dce-b5e5-21d9c85ebdcb
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 9e57344b-ac89-41fa-a53e-7abc4a72ac4e
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 48ff328d-8c8d-4f45-a11a-b5a79ad785f7
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 211f1ac3-9323-47de-85df-622c05f28440
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: ee34a37f-9313-43c1-8281-15f7d2f7ba27
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 56f8c755-eb54-4db7-b717-42bebb0ce45c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 6ecb8208-fa08-44f7-8ef6-4d5ee385d587
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: f27cb7fa-ea75-453c-9527-a44553dee421
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 43a0e8f9-14f4-4c9e-ad9d-68e27616a654
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 5bf71f19-7f97-4729-bf99-00f060ee4126
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: c54c473e-1d8f-4b1b-a40c-bf041d63d268
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 219ac756-fb4a-4d29-82d1-768de0a05f87
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 66b4ebc1-770c-4ef0-9938-83b341c00432
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 1587d174-0945-474f-a705-2bdfc17bd84a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 1b41f303-340c-49d5-b2f4-56bea25a67b7
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 9d8963d9-8a33-43d9-9900-ad166cf8af88
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 821ec918-389c-47ea-9234-d1d9c7cbe679
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 3a343a33-94d0-4546-bbf2-9888b4fc5768
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 58049c5e-9f61-4cf7-939e-b04f8c619863
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 5fd2a604-9cc5-4bfc-a4a6-ad4b7c419616
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 3342a22d-c08a-4739-b8cd-0cc8554501c9
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    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: 3f040dd0-a6f2-40e2-a796-f2da1d10e3d4
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound20.c: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound20.c
    file_hash: 8266a4ea95b9e4223f8b08ac8ccf14874ced037158e20412a04b64da93889ae0
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
