- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a89a220a-5bd8-43a2-b4d6-4e7ebbc16077
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 36
    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: 1b7ddf85-6653-480c-bf2b-b9a874fde7c3
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 36
    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: 1d9053cb-6aed-429f-9d41-386e20d1ed31
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 36
    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: c322c994-b6af-44c3-9695-08f4f432efc6
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 36
    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: df5aafcb-d8e7-446d-a1cf-d256dc2ed05a
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 36
    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: fdda7b2b-613e-41c2-990d-5c34a7f7ddf3
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 36
    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: 2154f602-53bb-476a-ba47-ab325303a640
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 39
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 89024a6e-7e5f-4a99-b1dc-7e2832a6c79b
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 39
    column: 8
    function: main
  location_invariant:
    string: (4294967295LL + (long long )b) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a4101ab2-b24c-4b45-a4c0-a4ab985fc500
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 39
    column: 8
    function: main
  location_invariant:
    string: (4294967295LL + (long long )x) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ea2fc3f8-586e-4b61-9962-e99715b11eca
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 39
    column: 8
    function: main
  location_invariant:
    string: ((4294967295LL - (long long )a) + (long long )x) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: de542bc7-2c30-46f6-96c7-a1577a168ed5
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 39
    column: 8
    function: main
  location_invariant:
    string: (long long )b - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7af5ee00-3654-41e3-9537-8d33c91d981e
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 40
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f870adb2-ba49-4d15-877e-741fbca81517
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 40
    column: 12
    function: main
  location_invariant:
    string: (4294967295LL + (long long )b) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b6d0ec4b-6d37-4dff-97bf-9715fd4f1164
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 40
    column: 12
    function: main
  location_invariant:
    string: (4294967295LL + (long long )x) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9abe6432-c7c9-4d7a-a148-553bb5d7a05f
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 40
    column: 12
    function: main
  location_invariant:
    string: ((4294967295LL - (long long )a) + (long long )x) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 855bffb3-08ab-4975-9d28-41a23e185d70
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 40
    column: 12
    function: main
  location_invariant:
    string: (long long )b - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 09a54319-b669-4f95-9f3a-8c246f99286e
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 44
    column: 5
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c129917b-48aa-4a77-bb7d-ff168b90e809
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 44
    column: 5
    function: main
  location_invariant:
    string: (long long )b - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c215e6b-ef0c-4533-be97-c846b01af057
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 45
    column: 16
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd273b6d-8339-4ca2-912d-dca258f7e3fd
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 45
    column: 16
    function: main
  location_invariant:
    string: (long long )b - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0994817f-17d3-4a9f-8729-b3ff5d06407f
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 47
    column: 12
    function: main
  location_invariant:
    string: 1U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 61b4a849-882f-4cb0-80d0-4cc1a2573d14
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 47
    column: 12
    function: main
  location_invariant:
    string: y <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0656c09-db97-4502-b4ee-f6c403aaab8d
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 47
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ddf9175-e4da-4c91-82c6-1e7c39a826a2
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 47
    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: 9edaa379-8e95-465f-acaf-a45194185514
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 47
    column: 12
    function: main
  location_invariant:
    string: (long long )b - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d16a9f1-ee04-42d7-adcb-8ed1e2b344b8
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 47
    column: 12
    function: main
  location_invariant:
    string: x != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 72599fb0-9c2c-4bfa-a83f-144568cb53ce
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 48
    column: 12
    function: main
  location_invariant:
    string: y <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b24e377-6a12-43e3-bbc2-bbd23fe6f010
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 48
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 033e4426-ae16-4073-a158-971c7987ab0d
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 48
    column: 12
    function: main
  location_invariant:
    string: (long long )b - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bbae0b7e-ce9e-4fa1-9b7b-a3ec76395d91
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 52
    column: 5
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f5c9ec09-5edd-4c23-98bc-7110089c4692
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 52
    column: 5
    function: main
  location_invariant:
    string: (long long )b - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ea85a07-2e7c-4d8d-b918-b8d329952062
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 53
    column: 16
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a46c1db9-e1ce-4e60-8b6d-79c2e26b697c
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 53
    column: 16
    function: main
  location_invariant:
    string: (long long )b - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1534f076-ff7a-498f-9858-09abc66580cd
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 55
    column: 12
    function: main
  location_invariant:
    string: 1U <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f8efcd7e-221f-40b6-8274-35d7913f531b
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 55
    column: 12
    function: main
  location_invariant:
    string: x <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39e80435-3da1-4bc7-ac7d-43fc0fbc3a8b
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 55
    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: f1a795dd-b8f1-49ca-9a29-6cef9e2562c0
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 55
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b9eb5723-4587-44f5-a56d-90da808332f8
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 55
    column: 12
    function: main
  location_invariant:
    string: (long long )b - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a86360a-d72f-44b7-9aa4-8a34ad5fa3f3
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 55
    column: 12
    function: main
  location_invariant:
    string: y != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6bbac23b-e206-4ed9-8b57-12a9d19062d4
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 56
    column: 12
    function: main
  location_invariant:
    string: x <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 297c9f59-be6c-4d2a-bb9e-c2a8eb6e2e23
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 56
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39e52558-46e2-4564-84f9-12e185df42a2
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 56
    column: 12
    function: main
  location_invariant:
    string: (long long )b - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9c336d0a-d611-456e-93d1-a99453011c01
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 60
    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: 1e2d2e6f-cd26-4388-b0b2-00d450fc45fd
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 60
    column: 4
    function: main
  location_invariant:
    string: (long long )b - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4d2c09dc-85b1-478d-ac2f-39586bf0c07a
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 61
    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: a1e375d9-dce1-47f2-a056-3cb7e951f4ec
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 61
    column: 4
    function: main
  location_invariant:
    string: (long long )b - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 97bccb49-b940-492a-b93c-b00eae7ec876
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 65
    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: 20cbc10a-9e17-431f-a070-4e4a98384446
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 65
    column: 4
    function: main
  location_invariant:
    string: (long long )b - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd8dcccd-78f4-42f1-aa43-a24d522dc84b
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 9187af1e-045e-4729-bd72-b1c05f608044
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: adb7c481-0e10-48b8-92dd-c34801cabc3f
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: f7f69200-a2e2-4910-a37b-a4a942abf10c
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 29d2eff1-02ae-4baf-adb2-530bc28f6950
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 63aaee28-a1d3-4471-866f-c1b2c34f5499
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 4b731e7b-5bf3-495d-a22b-f5b5949e8f4f
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 20782370-0d61-43b9-b333-9778dda198da
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 37281a77-94a6-4e63-a865-4c70c71547ee
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 41fc8254-b0d3-4736-b3de-922829237bb9
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 28d83f3c-7007-4300-8b73-fcf04a8c5008
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 4fdebf37-23e3-450c-9fe5-75b3c1ee770f
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: e8206168-777c-4db2-97cd-a4218b5554d9
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 3507f4a5-8633-4c21-a6eb-24f93461191d
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 78d1e653-cafc-4578-a20f-4b09a8f762d4
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 85c08325-ff30-4d0d-8563-274ca0228e79
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: dd631b5a-7913-4bae-a9df-c8a5364c46e4
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: a07b9ec6-39b3-4f83-984e-d8bc79144c11
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 99878d61-2ec2-4308-b1ab-1320ab46a565
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 75015d9d-9b9a-421c-b4ec-7f89b23a4c23
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 6a19dcd7-81ba-4f82-99a8-8f98386e7a61
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 95acd3b2-308b-4b2a-9972-2dffadb39aa8
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: d357d60a-87fe-4c5d-8a5e-894fa1b71846
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 26059f16-f31a-417f-8707-58b7d92d0d53
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 8018123c-0ec1-4893-8919-e703e0742dc8
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 27
    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: 103790b6-cb59-4d06-a4ab-e52694770287
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 27
    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: d5e3788d-180d-47e6-84e4-e1dd48b231b2
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 27
    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: 50c53fe4-25e7-486c-a510-54e2a8794192
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 27
    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: 532441a4-9189-4499-a5d5-d606d89d94b2
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 27
    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: b7cd4396-3361-4d26-a29e-2ea1b29e6e3f
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 27
    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: 7b54b41c-b4ac-4842-8dfa-4015cc215d03
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9be17bd8-b84a-4c44-b674-e987e3539af5
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 27
    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: 8533a284-1404-42b3-b08a-3ae192956cf1
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 27
    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: 020a5b5c-4c3e-403c-a384-70b4b10bfbee
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 27
    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: 6b979061-175c-4020-bb99-e14eaf041c2b
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 27
    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: 1fcbe7e7-db04-482d-874d-483e7ea3dc7a
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 27
    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: 84766733-200e-4b30-bd5f-927a8eb81a53
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 33e7e221-fa88-4dbc-919d-2c22bd9ba895
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: e3badb6d-5989-4502-a725-589e33b42925
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: c81596c0-9be4-4ae7-a621-15585c0e3864
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: abbc73f3-caf1-4998-b2b5-8ac44b80c8ee
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 897fa92f-7f94-4f2b-b5d6-4532196a8d81
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 5c5cba62-2fb2-4192-8194-f7bc42e61084
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: b58692b8-fbe6-4ccc-bd84-c3a230c297ae
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: b99f333f-071a-4c9a-b8dd-f9b0d6638e22
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: a6bc1731-2df2-42fd-9634-c642d1196187
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 3c2fc99e-9878-4d21-b118-3aca332e84c6
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 666543bf-9fb7-445d-8dde-26a964fe3f6c
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: b368f083-5643-4c16-92cd-decf519370d8
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 30
    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: f63e301c-e01b-42c9-9420-3f6bb877db55
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 30
    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: 58c48686-3b18-4a33-b229-2fee3908e23a
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 30
    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: 47df578d-8709-48b2-95e2-7cc4804603c0
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 30
    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: e606ad64-ae5d-4bcf-826e-be4731a45db5
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 30
    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: cf2279c8-94f5-4951-a634-af13210daae8
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 30
    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: e2f2ec61-64d7-4455-badb-06c3fda05e00
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 30
    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: 2678f22f-464a-4aa2-bbbd-1586f7a2edda
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 30
    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: 7c126178-f178-477c-9070-de7dfa4851c1
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 30
    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: 1b6a0edf-77d0-4cc6-a99f-438116ab5f47
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 30
    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: 65253993-a664-43bf-a88c-8485d3bc7a9d
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 30
    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: fd1d2c6c-79bc-4ae7-9c61-d420864289f9
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 30
    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: 8b2783ff-d208-4724-a985-16c0937e9e53
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: b8c40ac1-b30a-4759-ac6f-7989f71d8032
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 45bab30d-9a6a-4730-bcd4-f547f1248fba
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 3ac8b884-186c-47ad-8fe6-8e11d1e7dacb
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 376a7e31-ba2e-45d5-aada-13c1ad913fbc
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 5a90eb68-8203-45b4-a454-c3c15f756786
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: b971bebd-6dcd-49be-8290-1eb57cb9a06e
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 19664b23-b683-4e35-b724-e9d569c2e3b8
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 859cf61e-3284-47df-b039-aec1eaa09738
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: ffdf77cc-6e1d-492f-bfa5-f032ba4b736e
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: bfe912b0-e33a-471a-921c-030861565fa7
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: cbe39256-63f4-4d98-ae07-1a91e84148b3
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 0a4bd18b-25c9-430c-b6dd-464d883c44af
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: e8288e27-00b6-4a51-9b8a-7985150e7224
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 0381e214-b562-43c8-b718-13ef0a968fb6
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 33
    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: c8a2a82a-9aa6-458c-a349-31f352826076
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 33
    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: b4fed129-6c16-4e56-9b38-fee07b7873e7
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 16191c84-5160-4c15-80f4-125184d33c57
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 6019ab36-0155-4fb9-bb49-b2ce46093e41
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: cc4b98f5-5a12-49ee-bb39-6420751a164e
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 690479d3-efff-4244-b35a-5302d35e5879
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 33
    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: 42a09a73-86e3-403d-97b6-a98caa8735fa
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 33
    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: 325aeefc-61c6-49b8-8c73-30d72040292f
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 7532eea0-3ee5-4a9b-b22e-a75f7c4fa933
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 33
    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: 2c80aa82-1961-4192-8a8b-ce4f5fc0466b
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 4dc248d9-00fb-47c8-9073-25e444faac2b
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: daf0e091-9e1f-4a70-b639-313aadd57c49
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 34
    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: f9774e68-0cb1-4dce-acbe-e12d3222f291
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 34
    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: 5213fccc-ab4e-4311-a956-d90af803fe77
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 8c488396-3343-4b44-9688-977775b086bd
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 6f7f0d25-dbbc-4175-8c53-c5ce00e95bad
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: c16f8327-b248-4036-bb5b-4ece468430be
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 34
    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: f9cb3c55-77c4-4ec7-8154-c906e4b871a7
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 34
    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: 9da3a8e1-d914-4e26-8980-e197df216861
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    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: 5ac492ff-51e1-464e-95da-f569d228c02b
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 35
    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: 36f80616-62e4-4c2d-b6bf-11a2e757d1e0
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 35
    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: d17ffe49-8008-4ce5-914e-e26898bf812c
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 35
    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: 379ed945-0ea3-4792-96eb-795a08243090
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 35
    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: 2336c56f-d8ed-4c2d-8b36-a6f886eb0376
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 35
    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: d0bab17a-4ff7-46e6-a72f-ee2978e57e57
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 35
    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: 01aa7ddd-f7d5-464e-8dda-78ca4fa6f08f
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 35
    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: 25ab865b-d3c3-4d89-89b5-a9fcbffaf294
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 35
    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: a0503e08-3247-4074-97db-56a79566a356
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 77f8c791-159e-430c-8963-6ca5cf32caaf
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: (4294967295LL + (long long )b) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: bc33e721-10da-4991-a658-cfb015c85ee8
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: (4294967295LL + (long long )x) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a3af0b4-0c93-45be-9c29-ed5b0217f2a3
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: ((4294967295LL - (long long )a) + (long long )x) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: b64f8509-0c62-4613-bcb7-e70cc2d0a330
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 38
    column: 11
    function: main
  loop_invariant:
    string: (long long )b - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c60fdd6c-2b8f-4248-af22-a6fe4d697cec
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 43
    column: 15
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 17332ae6-5ee1-45a1-861d-c1bae37ae125
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 43
    column: 15
    function: main
  loop_invariant:
    string: (long long )b - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d98cfbd8-d0b5-4fb9-8f4b-44f1e957ab45
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 51
    column: 15
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a96a8b35-83de-4f16-9140-c8b8d0b4206d
    creation_time: 2023-01-27T16:29:41Z
    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/lcm1.c'''
    task:
      input_files:
      - ../plain/lcm1.c
      input_file_hashes:
        ../plain/lcm1.c: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1.c
    file_hash: 127eafc67dbf4c09ebdb87b122412adad2353ff20b5e6bda1f5cac7c627afccd
    line: 51
    column: 15
    function: main
  loop_invariant:
    string: (long long )b - (long long )x >= 0LL
    type: assertion
    format: C
