- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 677d73db-9d11-4112-bf55-d819cd91963e
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 34
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8857b1c5-7f1c-4fc6-b782-7c11de6db520
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 34
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2716fa6-0df3-4160-ae68-eba0c7277e61
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 34
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8299d401-e9ca-4fd1-8e06-c5a8ec04b4a2
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 34
    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: 62566ef8-ef5f-430f-8000-0d58109b41d1
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db4635f5-9986-4e5f-8878-7ebf00dc1377
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b80f0e0-905d-454c-8f9d-61b152a24375
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 37
    column: 8
    function: main
  location_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad1d3d6c-8b9b-4c02-86ee-8787a08be56d
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 39
    column: 12
    function: main
  location_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a75f0331-b861-4b04-ab74-e849795d1773
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 42
    column: 12
    function: main
  location_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d492e1df-ccef-4c47-a8de-63f2a18102ba
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 43
    column: 12
    function: main
  location_invariant:
    string: 1U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db15acdd-07cf-47f6-829f-a2fef540830d
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 43
    column: 12
    function: main
  location_invariant:
    string: y <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ae4ed9a6-e446-4402-beef-5e614510423f
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 43
    column: 12
    function: main
  location_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aececef5-ff0c-4dbd-8c13-da6a7bcf5173
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 43
    column: 12
    function: main
  location_invariant:
    string: (-1LL + (long long )x) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3de7e35b-2b30-4ce3-abf3-86b1b5affc01
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 43
    column: 12
    function: main
  location_invariant:
    string: x != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7207b5bd-48ce-4b07-babf-26c360ed031c
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 44
    column: 12
    function: main
  location_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 86c9a4cd-8241-4fee-9ccc-fc96eefe4773
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 46
    column: 12
    function: main
  location_invariant:
    string: (0LL - (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c400bfc5-af32-4e38-8080-4daba07e0c6d
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 46
    column: 12
    function: main
  location_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 908d4698-df36-43f1-a381-a8a44101a2ba
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 47
    column: 12
    function: main
  location_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ea5cc020-5a6a-4ff6-b3ed-943eb46561e9
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c
    file_hash: 202bef7949e13bb96f32c25afbfc6c3ab25ae2d31d5e937a54fdffa4785c5a47
    line: 43
    column: 127
    function: __VERIFIER_nondet_uint
  location_invariant:
    string: 4294967295LL - (long long )val >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fad29561-9f45-406c-889f-182a6de4bc28
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c
    file_hash: 202bef7949e13bb96f32c25afbfc6c3ab25ae2d31d5e937a54fdffa4785c5a47
    line: 43
    column: 127
    function: __VERIFIER_nondet_uint
  location_invariant:
    string: (long long )val >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d5948743-d4a4-4110-b427-32ed60a8db1a
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 23
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: df31f64c-d173-4bc4-a122-e4e9c23d1cfc
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 23
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7c1c070-e505-4de2-8c9e-9199c55deddf
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 23
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb3b2d73-8d53-4653-a0f3-106dfd77fcb4
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 23
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c9a1683f-88f0-4616-8a4e-f199a3442bb6
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 23
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1f064b2-1b64-4b7b-9a5e-6c3a00064889
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 23
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4bf28a97-17c9-4e23-bea1-a1ad15313cd4
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 23
    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: ab1b36a1-e128-4884-8b51-c16bc362f72f
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a8899b88-a1f7-4250-a067-ae99e0923980
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc3cc2fa-9597-4762-997b-e886a776d5e6
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e987293a-41ae-49a7-af27-093fbbd54bcc
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f54a9324-c509-4abc-af42-9677bf140d1b
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 23bb2494-c3fe-4c6b-803a-ad1d64dfba11
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c965019-013c-4685-a480-ba1d171f4ca3
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d66bc908-17ef-41cb-8394-08b564267995
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e224b08-c5b2-4a0d-92e4-88f71e2dba5d
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2d78c98-a38d-44b0-b49f-1ad2270f8844
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9ebeb58d-625c-4c60-b866-ab6458c79d93
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c436b3d0-9c4d-4415-8815-c0e1fd0ffe93
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 24
    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: 5f9b21c5-3748-4859-9668-ea05614d5897
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 19e026cf-0161-4c76-9b92-d7663c7f7c4b
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 761d5044-63f9-47b8-b9ec-bb439f5e47eb
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5a815eb-9c96-4743-94e6-23185f2fe642
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: adff2828-82b4-44f8-9d9c-096fca8a106a
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb29f5c6-37ef-4267-891d-08302cdf26a1
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: daff4467-b210-4b8f-abcc-5005cd1074f6
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 69b94c26-a5d9-41d3-aee5-e964b1040c9a
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2823db00-c1dd-49ee-8c02-149314cbc5e3
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4a90d28-0b72-4267-b003-42bc3eeb9cf2
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b8793f6f-9c76-4539-ad97-74f49a19665e
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b056f9c-613d-4118-b9a0-d9757e5580c3
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 25
    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: 28819b9b-01a6-43e2-a644-e80709d07c18
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f013c4b8-1c46-47ca-bb91-95248548b79c
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ca421718-c071-4c49-8ea7-01ef61437757
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82e38b0e-2cc2-441e-afa8-7bc7cdccc0a8
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 731cc98f-b12e-45d2-8eb9-7e73c353153c
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f5e4bcd-b77f-4c36-8c2e-8e196deaea74
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee7c2d4e-2675-475f-b2e7-8f45f6ec1ea3
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9e3b3a0c-d5a1-42a0-b31f-5a60a660fc68
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93466aeb-4d89-4e97-bcc3-b304e6ec7d54
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18d196ef-7f02-413d-a2c3-36164395452c
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 33aea7ff-7d06-4093-8f51-083738d40587
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3fbd29c9-5ff1-4bbe-a3fc-6749375e8585
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 26
    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: e6888d99-9973-4c25-83b8-0a8d6cd8f192
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fae5e8bc-fbab-415a-a07c-a390819ddffd
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8b4c37a7-722c-4bf4-aef5-04579180df8e
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f970e09d-82c5-48c4-af39-81af868a1c7f
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 688a1e06-6627-452f-8cac-94abbef232ad
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f903628c-e39e-430f-8e47-811df3545ada
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 09c183eb-5d2f-4f52-8fb9-cd885e6b88d5
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 81d9b3ee-3372-4945-bebf-5f646290ffd5
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f8ce4e8a-cc39-4bd3-9d35-6309399ab1bd
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 063dcdf8-eee6-4231-a7d4-cde47155c00d
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 453c4d2c-ea0f-44b5-8862-8f82e3f23f44
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a362b90-9dd5-49b0-b69b-a99db3590186
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 28
    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: 59c018c5-bc2f-4a35-afda-d2da3a6b5b5c
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2622bb3b-4ce0-4cd1-b729-779750e039f1
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7469589-5114-455d-ba06-bb90bced14b8
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1548721a-a3f4-4121-8f9b-7bd492c01f1f
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b71121da-1fec-4d34-8231-91c655e4d2bd
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4405c016-945a-4ee5-8956-a33dfa141f89
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a5f5243-f48a-481f-987c-8faf3c63cf10
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 512b72b5-eef4-4a18-8a82-43e462114b0e
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 512e83f0-357c-4bab-9c25-e248781056ca
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5cf40a4b-3282-47cb-aa05-84a37e6ef9d6
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c551e43-aff6-4385-84bb-95cbe4eac6db
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 287e3b0c-c2ef-4738-8e6e-2dbf910e8756
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 29
    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: 58ab98c7-ab32-420d-a01e-02b2cc6fe02d
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ca57b5e4-7c86-44f5-85f4-afa83e31e91a
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4f56a65b-d177-4016-aad1-f773b8a24f97
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f8dbcd38-14f7-4b80-9a63-13a15b687c3c
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3bdcbc65-e978-4e24-ad06-9ac2b5aad56d
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 463bd57f-72c6-4d1f-803e-7ff1aa9083a2
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d581aa08-9a8d-45e4-ac2d-76ff8013f3da
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 365c9cc7-8d31-4b89-91a2-68396dc0f908
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c0fda8f-8828-4039-9ad7-fbc14f66618f
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9bec214a-8bc4-4cbf-90cf-8c4048fe7537
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aebacc5a-9eac-44a4-ac57-a6de97a8570c
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2219611c-e707-4c9c-bd90-c8c20aeff0d8
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 31
    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: 60fae3d3-fe30-48ff-bb8e-3d926ca7e09b
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 46314a79-2d14-4eca-b65e-29015b0b8304
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dde4ab69-23d1-4a1c-aaec-3bdd3264308c
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 866b5c05-d69a-487c-8a91-5e7f853714b6
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bf72c01f-2d93-4a79-a5dc-2b900237703a
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b8e8d34-b3ee-420e-a815-7e9511dcaae5
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 20354622-8815-4d54-a9a1-9935fcfd8675
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0babbccd-b972-40ad-9904-10a9ae8f64ea
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 21f1e521-7070-4020-abf3-5d74343a3f6a
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d046c4ce-0909-47b7-952d-413e2907c291
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 48cf27c1-59c8-45a1-b8bd-5b4ce71a7ddb
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 32
    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: d834bbfa-8cbe-4516-9e42-2c9c812583ad
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0817dd86-625a-46f3-93e6-3e69fca4cc00
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a5a316f-ce8d-47d6-aaa5-ae7b3774ca3a
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eb550732-c780-4b9a-ba01-cf94789582ea
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fadc0fd2-7357-4b39-8ce6-343b3078bb63
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 33
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: df1fa86d-8216-45db-ae6e-4631cf37f3cc
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 33
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a1102704-bdd0-493a-8f2e-584f3e2a2bf7
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 33
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a0587bd5-d04f-4b27-9f67-6aa395cedbe6
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 33
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 04f2a793-caa1-47a4-b2c1-eb50dae8afa1
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 33
    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: 9a814bc8-5f10-47ef-b0f4-c1d92ad6560a
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 33
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dbb928bd-36d8-458f-b331-b381cd4fa70b
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 33
    column: 4
    function: main
  location_invariant:
    string: (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 899899c7-ac66-4386-a3c4-4267f06bc87c
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 33
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 00e48a26-7381-41fe-9da3-0f9b2afd1c3f
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 0 <= counter
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7451dc0c-2709-4d98-b576-fe8b9ede64d0
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: counter <= 6
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ce3c5743-b928-411a-92cc-70383a81dac4
    creation_time: 2023-01-27T16:29:43Z
    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/lcm2_unwindbound5.c'''
    task:
      input_files:
      - ../plain/lcm2_unwindbound5.c
      input_file_hashes:
        ../plain/lcm2_unwindbound5.c: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_unwindbound5.c
    file_hash: 6518e3283e254ed16f96ad802609fc9f9c972959c7f4631066de203a846c5b0d
    line: 36
    column: 11
    function: main
  loop_invariant:
    string: 5LL - (long long )counter >= 0LL
    type: assertion
    format: C
