- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d89f739d-e5a9-4016-8cb7-b09b5f1f1f59
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 0 <= a
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dd754d59-2376-49e7-a3e2-222e86646c56
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 498d8009-672f-4c1c-9c8e-5e3a12d49756
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 0 <= k
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b874667a-9dfd-4aea-b2fb-e3bf4603965d
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    line: 29
    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: cdf95f5b-9457-49a5-92af-39855132712d
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a1b44a20-d367-4202-93b2-c907b09c743c
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    line: 32
    column: 4
    function: main
  location_invariant:
    string: x <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2bb45a9b-2ec0-4429-89c0-37882b5b52ce
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    line: 37
    column: 8
    function: main
  location_invariant:
    string: -4611686016279904256LL <= az
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 01a3a3cf-e34d-42ac-bbb2-829080bf594b
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    line: 37
    column: 8
    function: main
  location_invariant:
    string: az <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 87d682b3-29a5-455f-8399-f6d585799392
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    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: 6fcf158f-aca1-4dd4-b2d2-ebb6f14abf2d
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    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: 5f3690c6-27fb-4236-9761-84086302bffa
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    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: 35cdb536-9af4-4130-bf8a-188311e90a09
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    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: 3ab24670-d7d0-4391-8711-e357469cec81
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    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: 9c5b4120-0ad3-4ce1-8e71-acd8c45619d7
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    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: 00c0dffe-7380-41a6-8825-89ffdff96ce3
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    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: 6d8cfdc6-636d-443b-bf5c-db58241e291f
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    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: 78e2b798-09f8-41d1-86d9-c4371121719f
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    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: e5aeb1be-fb75-4363-8b5a-2cc5b573c5df
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    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: 13accd10-9694-4421-8f8a-532c92a29e91
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    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: 70589855-85e6-4c7e-80a3-c9bdf7255957
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    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: 93a6aa99-6c81-4acb-9446-6c5d17d4b80d
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    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: b4197e4c-b4f8-4603-9bc5-f144bfdd141f
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    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: 53ec42ae-7cac-4fc7-a193-1051ebad401a
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    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: 9451425e-8682-4550-ab0d-59b5a0c8af37
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    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: 543beb51-b6a0-43f6-b307-41ed4eaa3f69
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    line: 46
    column: 4
    function: main
  location_invariant:
    string: -4611686016279904256LL <= az
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bc51f55e-cc18-44f7-85aa-6f7c83c323db
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    line: 46
    column: 4
    function: main
  location_invariant:
    string: az <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bde3f157-0a18-44bd-aac8-5c0d6b8a8a36
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    line: 46
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ef01e3c-2376-461e-8d8e-bd28d612b35e
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    line: 46
    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: 09ce2602-e8b8-4a14-8ad7-d89f498422cb
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    line: 47
    column: 4
    function: main
  location_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 58c61896-e7d6-4484-8410-d6739ffb4f32
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    line: 47
    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: 2890219f-c0d1-4ccf-9459-6aa3ff664ba6
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 0 <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb0fe248-be76-4f1f-8813-854fc2433b91
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    line: 25
    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: d9f4910c-98ea-4965-a0cf-0901883a178a
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: -4611686016279904256LL <= az
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: da22a4cf-6ccb-4c13-87b7-8674796b7df0
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    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: 3fb01b4d-54a9-4347-96f5-11d377a14b81
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    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: 750643b0-7cb9-4485-88ef-17755f809908
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: az <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d84d36c-5c3a-4d94-926b-414cdd2ddbda
    creation_time: 2023-01-27T16:29:32Z
    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/geo3-ll_valuebound20.c'''
    task:
      input_files:
      - ../plain/geo3-ll_valuebound20.c
      input_file_hashes:
        ../plain/geo3-ll_valuebound20.c: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_valuebound20.c
    file_hash: 6c3a02723ba5c1d451bdbd3459a030afd92ce200d85c0df9c54e7e40eb695af7
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: -1LL + c >= 0LL
    type: assertion
    format: C
