- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a8b87e9-90e0-442f-9ce5-caeef66ce5db
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 35
    column: 8
    function: main
  location_invariant:
    string: -4611686016279904256LL <= az
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5eedafd9-1c80-43b3-bab0-f3e52a38f071
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 35
    column: 8
    function: main
  location_invariant:
    string: az <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eea261c4-e470-40cf-8bee-0205d146c03f
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 35
    column: 8
    function: main
  location_invariant:
    string: 50LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4990ef5c-10b2-4028-b83e-edcd39e97d0b
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 37
    column: 12
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f0844c71-ead6-4f9c-a180-7612381f9bd3
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 37
    column: 12
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c3417d8-4ad3-40d8-9dda-4dbdd3de9411
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 37
    column: 12
    function: main
  location_invariant:
    string: 50LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 74fa8408-3650-4a51-b737-4ee54999b725
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fa3cdb55-3d46-4ce1-99ee-00581fac4603
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 40
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483646LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e8a73a9d-e20d-43bb-9b98-ecc30e95a0ac
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 40
    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: 9ca2f5f8-f700-49d1-ac23-e5f4ae2daa48
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 40
    column: 8
    function: main
  location_invariant:
    string: 50LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 83980fdd-3fdf-47cb-8432-a9cb6bab04aa
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 2LL <= c
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c35ef247-c5f7-42f9-9d2f-9ebed1baa1af
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 41
    column: 8
    function: main
  location_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d8fe6644-1705-4fb6-85e6-433f6286dfbb
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    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: 9ac8c3be-214c-4e1f-972c-49e1bf47295f
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 50LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8993a73c-b8ec-41d1-bb20-fb8dd2d5261a
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 42
    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: 8f316b0a-8dcc-4884-8a78-77eb5b048182
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 42
    column: 8
    function: main
  location_invariant:
    string: 50LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f57cb15b-e3e2-4bb3-a51a-2d7906884d7d
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 44
    column: 4
    function: main
  location_invariant:
    string: -4611686016279904256LL <= az
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7da457d0-9442-4d91-aafc-45eb793776f7
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 44
    column: 4
    function: main
  location_invariant:
    string: az <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 85ec462b-3cad-4d31-8806-061006f09965
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 30
    column: 4
    function: main
  location_invariant:
    string: (-0x7FFFFFFF-1) <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7633e36-abd1-4c74-9aba-38e33ade996c
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 30
    column: 4
    function: main
  location_invariant:
    string: x <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b101b575-8ba8-4703-bedc-d1b1cf283b1b
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: -4611686016279904256LL <= az
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c4b2b56d-714a-48d3-adbf-755ee422f705
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 0 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4be18a53-42a9-4a52-9913-815cece72db6
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 1LL <= c
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 157cc9d0-bb5c-4c84-a27b-86ca5eccc835
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: counter <= 51
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: fcbfe026-0e93-463f-8468-f621c64d4a65
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: c <= 2147483647LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 27f9e5fb-1b2b-4802-b8cc-ccf48c0e0355
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: az <= 4611686018427387904LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 309ed1cf-8e81-49f6-8203-20f837d63c52
    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_unwindbound50.c'''
    task:
      input_files:
      - ../plain/geo3-ll_unwindbound50.c
      input_file_hashes:
        ../plain/geo3-ll_unwindbound50.c: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/geo3-ll_unwindbound50.c
    file_hash: f865ce2403889b362eca5ba5c175d767c3667187f591deab49a0624f78852be2
    line: 34
    column: 11
    function: main
  loop_invariant:
    string: 50LL - (long long )counter >= 0LL
    type: assertion
    format: C
