- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6f888b2-518c-4597-a627-d14c76c34fbf
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 1a1e7327-b250-4e73-bea5-443902cd70c9
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 4c55a9a2-149f-4060-9f59-3977422cdb64
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: f1069794-08ea-46bf-84ff-bd1d7e3ff09d
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 9e2b6181-343e-4ced-b6d2-a1a063974ca4
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 7a76ef6d-d3f0-48ea-9b47-6a062d58f770
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 9eeb5299-eee8-4c24-b330-3b374b8c9c9b
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 03397981-7116-43f3-935b-9a0ba1f60e7a
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: a0724f4d-b233-4a34-b385-37becd1b82fa
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: b1a0e242-64f6-4695-ac59-fce4b36037b0
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 4008ef0e-4547-4bd2-9520-31a6930ba186
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 2c9df832-c87b-40f1-affa-c132be2d4bec
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 138f08ce-9da3-4f05-bb94-2d4e32089814
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: f6f08fb5-4d18-4cf0-82ca-4f6e9ec6e005
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 0a81fc3f-7b39-440a-9eb2-f1370377a56b
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 1c263138-d520-4138-ad37-984fbd934358
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: ae26a3a9-dbdf-47f5-968c-b1d34d89a404
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 3772beb3-8be1-406f-a3f8-b615464ec759
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 51258fa3-001f-43c8-93f9-3d1a352456ac
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 5687e036-a3c3-4ae2-9fd2-4f9f986bf298
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 83a6d463-e5f2-4ec2-81d4-35ee655261b3
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fc737e2f-6b78-4210-86f6-51e5caa3f443
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 68f5c8d8-ee1e-478f-a7d6-a1154bdf2d3a
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a793a908-1062-49cb-8c1f-0fb22abfb15a
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd4aa4f4-72a7-4a94-85cb-6e439804073b
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f2d6a8b-021a-4b3b-b955-b502d6c64b04
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 09bfc7a3-7bf5-4091-8c1c-8b2192c945be
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 06dacdae-4f5e-492d-a9f8-29d243db95cf
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2fb6bd23-81aa-4d56-aae7-d5ad1cf0f1a4
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 735f2e49-94c8-4bc9-ac09-a0d15433f7d6
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 06e2bff8-ed67-42e1-b945-f72164da3131
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: a3e1eadb-125d-4e4d-9cd7-4f39bb077689
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 4778792f-2a40-43b6-b771-4775e72e01d6
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: bbb3ebe1-c8ec-484a-a126-00354309007e
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 3863ee33-c61f-4df0-99a0-b90212954e77
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 97ef976c-d2d5-4fdf-915f-3725a2a4de8f
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 5f04978c-e4d9-421f-8c43-1de61bbe7168
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 32f0625e-5de0-4472-ba2f-e87d69197a79
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c63bff9-c7d7-4268-8c22-6a7cb522f8b6
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f8c86e0-3496-4324-b3b0-c2fc42f01ee8
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 29
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 69dda884-f7b6-4012-89d0-bfc3f5ece7e8
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63598f88-ddff-4b69-8918-cd13c41152d3
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8871342b-17f4-42cf-9fbb-2953fe2450a5
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cce04e70-1aa3-4c0b-bccf-27ef1617843f
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 29
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 332d1661-2cac-4453-93ee-d78f65739433
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 1a1a626c-52a6-4ddc-add5-4f3ac2573dba
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: a1d794d4-af7e-455b-9157-ee4272649585
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 2ced58f0-3d69-4aa1-8820-1d4b348b732c
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 88c3a2e4-ce14-429a-9d46-dc312543be77
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: b1086fac-a826-4fde-b93c-0d77844ad5cd
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: abcb681c-62ac-4c9e-b8dc-6e4631c8a34d
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 0f11469e-1119-4282-b722-66a8cb3c1bab
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 9d134f36-b594-4b41-bfc8-4b681b008245
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 32
    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: 33f76a66-044d-45b0-a9f9-92e11e429cd9
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 350d36ee-dd45-4af9-ae9d-3c845df3b264
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: e5a46514-351b-4306-a297-fe75a28013b8
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: d7e7ec25-1e0f-4ae6-a937-fcd29ec668eb
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 32
    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: 612505dd-c0c4-4cf1-8468-07da94ca3151
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 48987292-51b8-41db-83d5-b183fcd6e447
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 20094730-c67f-47fa-834a-29ee1ed69b96
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4ae2a9e0-b55c-4ab0-931a-537222875a2b
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 33
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 57308ee7-0612-4f96-bb11-8a65c8c615f0
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 33
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 27c92d5e-f905-4bbe-8140-75940339e049
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 06ffd68c-da99-413b-ac89-1060840768da
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 33
    column: 4
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5248debc-9cbf-4136-bb4b-4bd1f4f319d6
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 33
    column: 4
    function: main
  location_invariant:
    string: (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0c551d03-e78c-411e-8564-bc8aa81c9583
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 973bf75f-17c5-46f7-ad4c-5b11bdd376da
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 34
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 25136b77-4e9d-40d9-993e-0e6eb050d6b3
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 34
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7715f6f2-89f2-4251-af62-0d8ad53fc754
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3ee252a0-508f-4c66-85b0-4bc685e752cc
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 34
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8be3b58d-0e5e-41b7-94e7-e8236a21518b
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 35
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5cb8bbf1-0a7a-42bc-b401-e0958643ccd3
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 35
    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: e9b38987-4209-49ea-9228-4f65152213ad
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 44
    column: 12
    function: main
  location_invariant:
    string: 1U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aaa39c70-0c71-4435-928f-126842476dfa
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 44
    column: 12
    function: main
  location_invariant:
    string: y <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f1b22503-f08f-471f-bf13-03bae614f5af
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 44
    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: 0d9d8af2-7e12-4dcb-879b-da2fa53fd05b
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 44
    column: 12
    function: main
  location_invariant:
    string: x != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a210c9e-ca42-4fa9-8772-1a539005b0ed
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 47
    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: d4c67cb0-cf80-41d2-9f57-d5cbbeb30061
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: fde60568-0227-495c-b281-1750d99f38c9
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 80c2baa5-2d8f-43b6-836e-7ed264524297
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 98dc8397-03b5-4167-bca0-dbf798ea07b3
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 8293649a-abe8-45af-9166-fbed05fc7430
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 1114b552-2c86-4944-a4cc-2246f95d1564
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: a5a1a65f-0986-4c93-a3f8-cf396df7d06b
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: ba044f77-f376-4aa4-9b91-39cbc35ebad3
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 2b7c9698-b24a-4aa5-b240-92705593c114
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 61347e84-5b96-475f-999f-8f9b451bb9f4
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 80d40f0b-5ea7-4144-ad1e-0302f70097f3
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 51f741c9-e335-412f-b984-5b178bd64b5a
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 134ba611-a4cd-46a4-9e8a-9dd4d16f7836
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 612e3376-32de-4f2e-9d62-f576f68b115b
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 3fb054ca-7f4b-4511-9753-268ed97c7708
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 44a865e9-df66-442b-89c2-9147a58bff75
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: d70899de-0096-4061-952a-ca8e17611d5b
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 4a95bf9a-00c8-404b-95dc-0557f152f6f6
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: f75e5f8d-3e1d-4eba-9235-076f4efc76a5
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 9ab2fef6-e07d-4b32-9273-70a0b788510b
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 878fd0de-0beb-431d-be1f-db92984137ce
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 0adda657-060d-493b-81fe-6936b992de98
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 4a6d22a8-ecce-4211-b985-f17eb5a0e771
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    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: 1fa64754-398d-4445-bf8b-6522ae75b827
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound1.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound1.c
      input_file_hashes:
        ../plain/lcm2_valuebound1.c: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound1.c
    file_hash: 75b979445b16a7d0cbf48464bf7b748fed9f6cd2ca88a888f2b108d83230a494
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
