- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b60e5742-65df-4534-9809-dd5c52f897d1
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 34
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d21350af-a1d2-400f-b0e4-2560b34ef8d5
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 34
    column: 8
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c24a1dfe-b7d4-48d0-bd9e-7b107ea091c7
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 36
    column: 12
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d2caefd4-c17d-4074-bbdc-78bb184ef6b7
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 36
    column: 12
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73bf41d9-a697-4a92-88a3-6a75a8d22f17
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 36
    column: 12
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99d95f88-bb15-4ea3-813b-ee1bc6e7d5a7
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 39
    column: 8
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a217cb2-ba34-4e62-8497-a94599e238bf
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 39
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 06de2522-f904-4c0d-a8ac-594c40e2ddc2
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 39
    column: 8
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a980db7d-4948-492b-a003-87c9cb938cf6
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 39
    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: 6373daa5-2e99-45da-9148-546682fb90cd
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 39
    column: 8
    function: main
  location_invariant:
    string: c != 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 198499fa-9df9-4f82-811e-948fc61208cf
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 40
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d62544e1-3e3f-44c0-96c4-f2ea8de6a597
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 2LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97bb6649-c34e-4dc9-8e9e-5acf4af83d6f
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 40
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0b0a58f0-95fa-42f0-b997-80172afae707
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 40
    column: 8
    function: main
  location_invariant:
    string: -2LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b48dab6d-4259-49e6-8425-c1d11bd5b883
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 40
    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: fcb5973f-1a72-483b-bed2-033bf1269399
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 40
    column: 8
    function: main
  location_invariant:
    string: c != 1LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26a7ceb0-3faf-4c9d-91d9-e792e47b536e
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 41
    column: 8
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a4f02293-e078-4641-b8d6-e8055ed5124d
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 41
    column: 8
    function: main
  location_invariant:
    string: -2LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b075b0d3-b46b-4e62-b56f-a827df3ca00d
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 41
    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: e2efca84-53a0-4c2b-a399-81b863149920
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 43
    column: 4
    function: main
  location_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c7bae73-bc44-4a3f-8a8b-ad58a8bc65e9
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 43
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c607acf9-5391-42c1-ba38-06cc981654c0
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 43
    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: 55bf2c21-e60d-4b7b-8304-a29367ce3e7c
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 44
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e92990f3-b371-4c61-947f-d30121e142cd
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 44
    column: 4
    function: main
  location_invariant:
    string: c - (long long )k >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c5779a1-0bab-40bf-b74c-ec7b99a221e7
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: -9223372036854775807LL <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 469b5f53-3224-4368-9179-6107b5565be7
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 86d6e77f-9520-4197-988e-48657cd4dd41
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a90126c-475b-418e-842d-795f1d822807
    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/geo2-ll.c'''
    task:
      input_files:
      - ../plain/geo2-ll.c
      input_file_hashes:
        ../plain/geo2-ll.c: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo2-ll.c
    file_hash: e871fa33b0334d5a32c7b72bf8c566167ee8ba89fea0452fc9132a1c10a2cca9
    line: 33
    column: 11
    function: main
  loop_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
