- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 06d1e098-56d9-4b89-abb4-fd584e30fa1c
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 0ed5336a-6877-4349-bd76-0a8a8861f064
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: d4bc30a6-4f65-43f9-9d1e-5a452dce9682
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 5b36d79d-57bc-4592-ab1a-0ca0cdf822d2
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: a9743972-9c1b-445a-b45e-99aff8c7a1e8
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: b82c7736-fdb0-4489-8b32-e92e33e0bce2
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 8f4940e1-affc-4d62-b31d-345eff7cd3e6
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 42
    column: 12
    function: main
  location_invariant:
    string: 1U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82e2e30e-5e3c-41c1-ae35-2535ba3e0c27
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 42
    column: 12
    function: main
  location_invariant:
    string: y <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8fa22718-dda2-4002-8697-a656f10f2a2e
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 42
    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: 07aef076-675c-4168-90ba-a11a186bc675
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 42
    column: 12
    function: main
  location_invariant:
    string: x != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 07338ef9-0d0b-46ce-af35-d384da2a1f55
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 45
    column: 12
    function: main
  location_invariant:
    string: (0LL - (long long )x) + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a7b9f455-8350-4fd2-90b1-aed280192050
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 22
    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: cdb750fa-b1b7-4f38-ab26-07f6a5954d64
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 22
    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: b1a36539-3249-4905-ae7d-961863f3b93c
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 22
    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: 645dbe26-fae3-469f-bbf7-aebf649f90c3
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 22
    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: e1a29e6f-4a0c-44b6-b5c5-f519b369d300
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 22
    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: 67a2852b-303f-4a85-b140-f4f368b33bbd
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 22
    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: b09e609e-69f1-4fd0-b2a0-8417b12baf67
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 22
    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: a83223d3-158d-45d0-ade7-dc77e0450bcd
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 22
    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: dc0603c1-8008-433a-bfc9-ef646ea65691
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 22
    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: b9ea84da-c41a-4c86-a7b4-85ab0f1a8eda
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 22
    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: adf688cb-b0a9-4b48-b380-df40a0202f08
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 22
    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: 92ba73b1-25d6-4405-aae2-ed4ac10d27b9
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 22
    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: 02759895-5018-4ecb-8a8f-f8b1461a6d15
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 23
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 570bb4cd-646c-47e5-9492-23e14ad01b1d
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 23
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 842a3b09-01e7-4e43-be78-b7f82d8ff531
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 23
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4934f726-3591-4e86-b28a-10a467ef8810
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 23
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f37c33d3-26c8-4268-bdf1-9d38e992625d
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 23
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e6a6ea23-2465-4f7a-b7c6-5a189319f328
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 23
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: deeb15c3-8a25-4d5b-bb38-f542703ecb13
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d1c0a17-8cbc-41f2-b72d-5c4901ca2cdc
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d7075f48-ef55-499e-b6b5-6c0288d17c08
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6282a17-e5a0-4c77-82b5-70cf2a31e36f
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1dcb0ca6-a209-4fe3-bd08-b6c2b2ab68a2
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63d20078-f702-4df1-bab3-5d1a0d758aa8
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3b3410b4-5082-45b2-811d-493c83c5488d
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 553ed23b-1df1-4573-8004-74eb5beb3d33
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 851020f8-3cf0-43e7-8b79-665c1d5c8c98
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a857080-4ff2-4e8d-aad6-3e9c9e033088
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d4166451-ef71-4407-9669-64e49bcfa7db
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 318e9b38-5d26-4bbe-b82f-f838249ce320
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 24
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0c42a52-c0cc-4d9d-9c7e-def51e136e5f
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d957799-2d28-4bc0-bcd2-5d848c456264
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f55b9586-f5c0-496e-96f2-60b4a497448d
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a3637723-287a-407d-8c58-a85a89ea1941
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 945a9a3a-0e67-423d-bea3-cf1d76d97744
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d40f18d7-de1d-4fea-bc7a-6fe0b2bd83b1
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 24
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 285fdef9-e11b-4fc5-aec4-4094dac92652
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: f96f0e0e-d267-4f7b-86a7-8e0af0b91e25
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: c4e9987c-ab87-431e-b3cc-fff19064e92c
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 1aa439f6-52e9-452f-a691-de79f477fb64
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 56cf24b9-b7c0-44dc-bb3d-5f77c76b0997
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 4b091b18-d0e4-456a-9b5d-fce899825212
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 9b462cac-8c06-4bd7-abb4-795c5186fe3e
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 25ae137b-65cf-4f73-b5c4-c8374c264f7d
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: c18827ef-1113-43f7-b003-307c55eafed1
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 8187cb55-b2a0-4a18-84f6-b83907b8df38
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: c3740a1e-ae42-42ad-9132-30d6f01cfd78
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 40f6c339-eb36-4bea-9494-250938c619ec
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 4482ba9c-1894-4624-8134-95f5a4337376
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: c3288b92-599b-4682-9331-cf6e552d1e79
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 6d21c9b5-db10-4b2b-b9a3-f15ef8a76dba
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 55a11234-3f8c-4a16-85f0-ff8dbd24489e
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 2c4283cd-44ef-4285-9e0b-3f8eccb21b03
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 8dbf4cf1-82ca-48fb-a69f-b040e6abf676
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 3d9a14b8-e789-4405-acdd-5c6080bb4f22
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 3eff5da9-3a9e-4d81-965d-cbe486b94e27
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: b90023bd-d369-4ecf-9fd1-c95daaa92d31
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 322fe774-4f55-43d9-9b71-bce4e01c8236
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 8e946150-2dba-47ad-87d9-14954305a7b8
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 61858314-d8e0-4d15-8ab7-5ffa44e4a75c
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: cc9f43be-f3af-4a43-b819-5970328a67f9
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: c3438cf6-da6e-49e0-b7dd-8fc955734941
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: a3c82dea-3faf-43d1-84c3-69588feeb748
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 67739306-74d6-41fe-a15a-94783e6ff8e3
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 20f69183-172c-4b38-8ecd-6a01c0c090ba
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: e652c80b-6d0d-4927-8ab5-3d81371b4a67
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: c85b4083-dae1-4248-8151-7b2fa012ba59
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 14fa3565-17f6-41b6-b9ac-38358839f386
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 86707d18-1883-4cbe-8fb1-6bd0a486e6c5
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 4edda8aa-a04d-42b4-984d-eb9b9e992df7
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 6b69693a-ce72-4e93-85ce-8b1f124faf1c
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 5e5a0191-4678-436a-8186-6692e7c7e230
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 24ab33c2-36af-4a7e-bab8-7113a7ee87e1
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 6122d307-3ae5-4838-b6db-5f023c27e2d0
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 6dfa1694-e453-4306-ae73-1725f0dac388
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 06bcc5ec-f4d4-42e9-b06d-b8cd0dac2059
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 1f4aeb7a-d676-445c-a883-b02306a77679
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 6f78e3e0-34e3-43d9-9497-f39526793741
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: f02a64a1-c229-406c-a3e3-e7af40ab0d2e
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 0d52267f-3a56-44c0-b8eb-500580e6e901
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 3fae2928-9b64-4f4c-ac32-3f8811b164e7
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 39f2d53b-8a38-417d-a8c3-600480077b2a
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 66b358b7-9063-40e4-855c-ddee6a781837
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: a9242a46-af92-4f43-aeed-54ea3ee22708
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 99634003-6549-4dc4-969d-897f1f0fab11
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 782889aa-367a-4090-82ad-6de2db2bcf08
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: f0bd203c-a3fe-4719-a009-1d1540ebb76a
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 7d31e9b1-c84c-4283-890d-e9b4c9077bf9
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: e0a2325f-e83b-438a-b528-5774835616ac
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: fa61395a-e753-42c3-a392-7af12d00eb6c
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 425a480e-9e96-4bdf-8550-9ae11d707a21
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: d8bf55b7-c3ed-4404-ac69-b928bf1e5fc3
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 0efb281b-4859-48a5-b066-5f328924926a
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 181e6124-c24c-4097-9825-2a7d7861c700
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    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: 2b1e2839-52c5-41b3-b1d5-90716739b08b
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b00f26ff-c682-4929-a885-dd3fb2899c3f
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5595ddec-90c2-439f-9e4b-04c02cc6ae26
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5ddf8a17-6354-4dc0-b5cc-0a13a9a4d029
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c1f412c6-c375-44a2-9255-426130679782
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 830d6d76-069d-41b4-95ea-a313a9807f24
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ab62167e-057c-420b-85e5-3f9c039163d4
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 03e6c0b3-adbc-4bdc-8f17-1d0ea34daed3
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2.c'''
    task:
      input_files:
      - ../plain/lcm2.c
      input_file_hashes:
        ../plain/lcm2.c: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2.c
    file_hash: e0d433468442fea01fd6f51a5fcaea8db7e3b564878994442665eb482321c037
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
