- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7af33816-5ecf-4f4d-8149-b41571bbfb58
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 9f0808ea-ba87-48d8-8691-8504d4c66684
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 8fb36056-7afd-4693-a2a6-568ae00dc98e
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: defe9328-04c6-41da-9233-0298f16813b0
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 4059d623-63f9-4279-aa1b-ed9acadf2bfa
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 6c6219c3-6658-47c8-8601-317bb36d3a04
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 70b1c790-a921-431d-8fa7-3e87738aa820
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 92cf5839-9968-4cb3-83da-6ec0fc84672d
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 1b2520c8-e865-4785-b98f-858790113557
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 82cad831-9e7f-40bd-b072-5eed4beaf5c5
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: ace10b70-85ce-473f-8cdc-4f1c758d480b
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: aaeddc75-c0e8-4810-b9b0-0ce172ec690c
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: c70caa56-6c4f-496b-893b-a7327b05fbf7
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 34d4e4e7-4956-41bb-ae3f-bf3cbb7c9a8b
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 2b2c544b-29e6-409b-b91c-680e81ee9440
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 90b003ac-2dd2-429d-bbb9-6c463d3e1246
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 6d28b884-4864-423b-8d87-ffb18fbd4479
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: b8bc093b-97fe-4a8f-b867-279f23978593
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: f0db6106-a612-4608-9c47-be42382c9fa8
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: ff1c310f-bd4a-4880-aad9-db41d0d06e12
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 27569064-cad3-49f0-a19b-447e6852f446
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 35226f03-36d2-4ce5-bf09-22b22efa9848
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: cb336bce-e8a0-4990-8bf8-7029faeb279c
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 0786d912-2959-4eaa-b4d2-a5bae22c7f1b
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: a96755ef-25b8-49b2-84e5-d140023bd2c3
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: ced41952-4617-4696-81d9-b2805acacc10
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 00c3addc-8362-48e4-9583-403dd9828dae
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 596f45c2-6ad3-4c40-9abd-d1a399df0aa8
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 3a058af9-ca69-4d61-b150-c82b1c08c28d
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 0b782814-2cec-4818-ab70-17080bd2568b
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 6438d9b4-24a0-4284-84ff-930bb6a2a514
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 0f1a7436-9fed-4932-87e2-5b0b420576a1
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 0433a305-f97f-49d6-a78d-8499b23ada21
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 67e24b2b-58e6-4e57-b863-447fb7bdcc35
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 102e034f-2ee3-4ea9-829d-0f1033f58b37
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    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: 66f5b1ee-9de0-4ec4-9d11-be6b7252dcce
    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_valuebound100.c'''
    task:
      input_files:
      - ../plain/geo1-ll_valuebound100.c
      input_file_hashes:
        ../plain/geo1-ll_valuebound100.c: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo1-ll_valuebound100.c
    file_hash: 9510036636a06bbbe217d25abc7d9d86c957b5947d577c099943a8ac8bd54815
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
