- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9212129-3b2f-4c0d-8997-3a4ee2e9016e
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 38867ce5-e316-464f-9a5c-77e8bd2386ed
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: d8077356-d3dd-4bc7-ab8c-88d75b69276e
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 568b007d-ffa0-46ff-941f-97b6557b0468
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 34eed72c-0d78-4a7c-8e22-cb50ea003852
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 8c208271-6f2b-4c27-aada-486799b7b877
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 8fed61e9-dfb5-4a41-b569-33dadc35c390
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: b85311b8-c255-4e33-bccd-737a02aa2108
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: ebdd9125-9e1e-45aa-990c-27dc27ee7846
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 5269530e-daad-4989-8d36-b2482215ae02
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: f329f7fc-4f1a-40a6-aed5-def047518560
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 2c74e8c3-5bb1-487a-8506-6682bc328007
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: e9fdd585-d178-4f2b-b53c-2d3b275767ca
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 8c98930b-27ef-4e8a-a94f-de0529ddb970
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 6393c669-dd32-461a-89be-b54a62a2e48f
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: b5341083-76cb-4889-b8fc-78e420b38274
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 48237962-9922-4a2e-ba2a-63156f96a7bf
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 184e2e10-549e-491e-9dc5-e440e39b524d
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 215bc990-c02b-4fb2-9b9e-ec8c3ed7792f
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 53a8decb-36b2-4fb1-9833-165f77cc686f
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: fed9027d-6d74-41f8-a313-e562e0caf064
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: e1b9cfa9-842a-4934-974c-aa7d44ca6681
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: a5e8c41f-7f2a-47da-9f9f-88b6e6959576
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 98bd80a2-1fa7-4741-ae90-cb54ec3ba0ad
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: dbe5e635-82b8-432e-9910-0ab8c7c936af
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: e9c2e3b5-8511-45e9-89f4-67f995b85007
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 19a42595-50ce-4d12-896a-eded3498e254
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 47881250-53f2-43dc-93ae-8d49bb403104
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 82cfadb1-3c63-4e2f-8544-0f3983240234
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: d0d1171f-7eac-4761-83be-93dacea2c81b
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: fc55c7af-1c99-46f2-8bb5-ce6f87d62f37
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 2a89895e-3058-439e-9899-f650d532f4fa
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 35c174be-2850-40d4-959c-788faeb76cb6
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 993d6c53-073d-4d25-83f3-7a8d9523dd31
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: c5c1f533-ef54-4207-8dcd-2e77304bdf30
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: da19d0fc-53d0-4a41-a08e-b60a865d197e
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: b1de3cab-dbd8-419c-9011-01e94b87b38e
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 49db04b5-d957-4574-9d9a-458cce8e3a2a
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 40836476-1467-4693-b3d7-dd1958b9b4b2
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 0b86c557-7acf-4380-824b-4c5b769f94c9
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: a803a7e1-3fa2-4993-a5ad-e8de9bd1384c
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: c986d486-3669-49f3-b609-9fa6158d49bd
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 5207b308-0f95-473d-ba75-cff6e633d746
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: df4ff0f7-0355-4993-ba76-d0fe48fdfd84
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: bd67468d-8aa1-489a-9907-e22f6d01e989
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 7974222d-751a-4758-a047-fee97b9724a7
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 67e3dc91-5777-4c32-aace-58ac3346ed19
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: f32ae184-62ad-4a1a-a948-6af0552652a4
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: a69841f9-e00a-4a82-84a9-dad9435e1e11
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 1cca3d5c-6457-4781-bddb-32a2ce89acfb
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 0e0b6c1b-e215-4e0e-8ad6-ede57d81b236
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 898def5e-b4c4-40ae-bd22-0325e3cf28c8
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: e92d81f1-1946-4b79-b361-16efe3e5f9f0
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 4521ae0e-3a76-4ba4-b5d7-7cfe2e9ec89c
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 19f4f899-9c96-4b87-b457-db6cf2d7c9c8
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: ce7854a5-54df-42f2-a16b-39a548348f58
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 0e704c34-8086-4663-8f29-140452850725
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 191aeb18-e566-4685-ab82-1d5856490cfd
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 0af31c82-902e-41ff-8461-b059b73c3788
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: b889c429-02b9-438e-90e3-50781bdb1840
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: d1663d78-5850-4d38-b878-c93d26650fee
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: d2d370da-5a6a-41b0-bd2a-cdeae9ba567f
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 14e6c16c-2411-46e4-a3a2-89840ce4331a
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 0153af15-3431-4378-8946-7d8466034a47
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 5d1e7915-2d93-4e40-9668-abf7904e3054
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 427ce73c-265b-44c6-9859-9408d6284ae4
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: f7b8008d-bb1c-4c5a-8ec4-89e7c0fdd47e
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 135e4ef9-53f7-4b3e-a084-7eb17c52ed0e
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 70992d27-cb28-41fc-81a6-2e41f9d28609
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 460dde93-e3dd-4012-a796-e1c8fdb9c1ee
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 06d19095-2032-4b9b-8e10-e4b083860ad1
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: f5ba79b0-d437-4960-bd9e-24f97ff911c4
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 1ab850c9-136b-4b3b-99e6-e93eae444240
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: e564f97a-825f-47ee-8ff6-80cd9062f096
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 03629874-cd5e-45a3-aa11-a67e0d329b40
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: e4272850-3a71-4bde-a74b-891027300152
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 206bd944-f7eb-4d5f-837a-c6b2e60cf967
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: f489fb78-7696-470d-b799-c1415f22ccfe
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 14227906-0c48-48f7-ab97-e9f0623c3dbd
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: a3d96d1c-3022-4a76-b829-8e45f053699a
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 30a4f19e-4576-4675-ad63-40690f604ffc
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: ad113064-485a-48ec-9a4a-5581cf0f2ef8
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: e90c70c4-3f11-47c2-ab95-1042fabfc6aa
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 1520b7c0-9d66-4eaf-b15c-80384706929f
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: b5632a75-a4d8-42ef-8702-c9c8284cd1f9
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 461fc619-a7cc-4ed2-a441-c8ee36c0e130
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 63c23985-de62-4a6b-8d91-ff828a707f61
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 7d67fdff-081c-46c2-acc2-20a031626f37
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 1382265c-8306-42da-bed8-d206f53210f9
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: c7ccb02f-2cff-42a2-9a35-5090bfbc6d04
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 3979d0b6-934c-47df-9bcd-664af31c46c3
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: f89d41d3-643c-4d7c-bc0a-0d3c51284633
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 924223d3-0a94-4366-9429-b8f1600fc182
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 7b6ec644-a70e-44d6-919e-2c20bde06ddc
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 77572dea-1f8d-4413-b3e0-860320d99094
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: cb5c1b2b-7189-451b-ba2f-c87c5e9c63b9
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: c223fa57-209d-4976-bcd5-14cb04272e24
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: bc859790-7ca4-4d40-9bf6-3b0d957da0b2
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: c19ae17e-4b3f-4aa7-bfcd-b4195b1a6298
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: d104c2d8-f1cc-4209-9280-e1f2935f2eb6
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    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: 33a94aad-832c-4b99-8e55-ddac9f437a24
    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_valuebound5.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound5.c
      input_file_hashes:
        ../plain/lcm2_valuebound5.c: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound5.c
    file_hash: 78ef731083faa503d4cf5e0ad0f2613cb9f5144cc63c5bca18c10075cc31f97f
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
