- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 615e7379-a6a6-41fb-bcf8-4eb481bc5c26
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 4d53cbaa-caa7-42e7-9cda-aa86eeb95071
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 83d43881-49b1-4941-8051-6d28165ff04b
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: d104a933-7815-4d5c-a5f6-4fe2b8ad402e
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: b1d9198f-fd95-41ad-9920-72fc36c70667
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: a92b89ef-f6fa-4b2a-a414-7c7dc650bb80
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 7fae5dc9-216c-4647-903d-70e75a6747e0
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 6bfe4a53-1965-47cb-a383-60935ff390b4
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 1dca540c-6b1c-43bb-8458-06d5723af53e
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: cd59b6ad-4b4e-4977-a568-424c409aa682
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 260738a2-1d85-409f-9804-8792399f4661
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 7ec5e822-d22f-4bd4-98ef-49e59538c7ec
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: fbd3a322-7905-49b2-b3fc-16e32b2a2ccc
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: c8b4cff0-47fc-4994-b76a-d2f799bf89ab
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 69b94a5a-426a-485a-8861-6ca011b425a1
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: a2187f5c-574c-4b4e-926c-c05f9f094da7
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 63aefd08-fe32-44da-b531-010bcbd73eba
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: b20f6440-e754-4771-bb0f-a0b54ab13b76
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 32eb7f43-ed08-41fc-9cfc-654e5c0a65e0
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 34965ee5-1fec-4aa9-8ea0-025cdd0cd7d8
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 5205671a-0599-4ebf-adaa-ac9aa1064a94
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 47a8b44c-3604-44ef-a35b-d3e2a55fa400
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: cb6cf89a-802d-4ee0-bced-7cc1c739dab7
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 3d8e1bf0-8869-46eb-8ae3-6b513bcae516
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 162b9f26-337c-4ad2-b857-dbdd9625ed07
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: d8991692-d8c8-4b43-9381-5852b2b6847e
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 8af1a3ab-5cb3-4161-8171-59174ab6f848
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: ac422661-a6e7-460c-a968-050527ab0560
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 48107416-544d-4f06-a990-cd87382ee93d
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 14a38c80-7b24-46e2-8285-cf324076c11b
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 0aad19f6-4a8b-49d4-a8d3-7e1735e8b96f
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 360d22e5-9eaf-4e3b-9983-75cd225fae46
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: da263ee0-27a8-4ea9-a5b8-864e17b9c54a
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: d0b50e39-c353-4e5f-8394-64e92f3fe4de
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: 44eef22b-99dd-4804-8938-b957cb97724f
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    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: fa68a83f-d608-464e-bed3-ffbb1cf52448
    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_valuebound10.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound10.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound10.c: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound10.c
    file_hash: a634b7b2fdba4e1130af0357d8449857b1aa9910f5828bc3787bf2c95d83a46a
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
