- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f829ffaf-4164-4434-9e4e-a5081b6a3cd4
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 1322385b-d7d3-4e0c-8aa3-a2a1945f826c
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 3c59a678-9e49-446d-9c4f-f7db81000829
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: e5fb3236-a25c-48cd-841b-4513b4897578
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: ae9f9633-a780-4f6a-bb1e-234d581cce73
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: cca3f193-35aa-4abf-ae4f-589f0ff03318
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 067f8d69-ab8b-423b-9b6a-835ec5779344
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 4e9ec75f-a980-4c07-8bed-15938c15f50d
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 001237b2-f026-4693-9cec-627be006b861
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 89bfe962-44f7-4049-a8e4-e32cf0a029a6
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: e506634a-a708-48f5-a775-8d0f833c88aa
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: c79d7679-e555-4cce-a983-4fd56ac2d6e3
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 333a1152-5661-4572-bd4e-2ee1fee2e631
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: b39dceb0-3c11-4ec2-b9f8-77d86e1694b5
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: e709ba3a-b493-4881-9a0c-6caaa0ecde58
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 5b019dad-666a-4cd9-8c62-1a903c00fc63
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 084a9f7b-3c0d-47f2-a6f6-607c857d2f9b
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 95293d37-4902-43af-874f-d90f49c764af
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 20828984-e391-4a54-9043-770cdb43c90c
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: fe43186c-8ef5-474d-9a29-743ad97e7cd0
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 1b753551-4eb1-4b97-b198-77befc0cdb46
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: c15fddb1-a8a5-4b93-b3dc-f7e9e5561fe7
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: c3018f77-2ff5-4555-80c0-5cb261234e69
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 63d526e5-7f9e-4ba3-b097-30a44ebcfe7a
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 0f4db9cf-be9a-4062-a4dc-092bb28d9290
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: bb16243c-f8ab-4cf8-a29a-6105ca600132
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: ced1b9c6-db9f-4d30-87b1-cb26d577aa60
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: df903931-9cea-4692-b29f-060362752681
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: a510edf1-4a91-4423-8d7f-ce7109242711
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 77ebc8f4-b8b8-4d41-bcc3-15ae72747f5b
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: fabec07e-dbae-4c0f-abe8-0e9cb588a282
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: ad05c507-65d5-4bcb-be90-2399976ed510
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: df91d682-7a5f-4650-81b8-971c97223fbc
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 7d62b454-c02e-4786-975c-474c012a61cb
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: a0569395-908b-4fac-84e2-c1dfcd8a5484
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 2c5ec73e-aa63-4464-8195-c27d75a33903
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 32724a34-b76c-4c67-bf76-1014b26fb4e7
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 7d54646d-e164-423a-9316-a1fc659b3ef8
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 9ca13419-2ec1-4a0d-a81a-66551a0d4d18
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: fbcc1478-ad45-4579-843f-fdeb656b8912
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: cfb67d9a-0f4c-40f4-9b53-a15d55365329
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 39438d9c-3976-4558-af92-72f24a4b1ef8
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: f008c934-d71f-4308-8a48-90f00d7ff2c2
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 7a795816-cfc3-47bd-8399-fc4fadc31d22
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: bb5a48eb-6163-40a6-a28a-085a1b90cce5
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: fe6e2295-5da0-4026-9a90-07390d8830ea
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: b170ff0b-61e1-45fe-82a4-0e5cc9447d58
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 749bfb6b-faf9-4f14-a4b0-865944e2aa32
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 834cb25c-ea2d-4a67-86ed-c0f2ad2b1106
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 8a649f96-a719-472f-90e9-290fb4099cc5
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 00efd72d-088e-4566-85a1-609af073ec2d
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: ab9c3f98-7e6e-448e-acb1-4185e53d9136
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 582dc53f-aa75-455a-95f3-53dfef5963c1
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 606103a1-721b-4178-ba42-8a13be054c07
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 26ac2588-1b76-4b18-ae84-2ac49a84facf
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: cc605b75-c602-4d4d-b932-227e04bae099
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 8834759d-4c78-4c58-af98-95a1aee8bbda
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 9a9ec7c4-fd20-4397-a623-7ded7a86eb3d
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: fbd134d4-27bf-4645-895a-fcae37369422
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: f50d45a9-4b31-4905-b760-dc66f0b531c4
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: d86becc3-533f-42af-9b04-a01e38345360
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 07bfc6f3-68e9-44d9-9267-63d722967b32
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 85360b12-b3e3-4f35-98fe-b9e27dd33de5
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 160871c7-483d-4814-98f1-746213d76c3c
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 5a9f7bb4-4450-4a39-b16a-49561802f13e
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: b7ce4c82-29bb-48b8-b7cf-5bd7fa6051c0
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: f424744b-32ef-4714-9b86-6112095a04d2
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: e0944c92-0b3f-4b42-a401-7f7e164c90fd
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 06d1494a-342c-4e96-96d6-60297940c3bb
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 34b756e5-2f30-4208-92a3-39ca28abe935
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 674a5e07-ebac-4dd2-82a4-2cb85aff76dc
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: beaa6f89-228c-4424-842e-5bd60790315b
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 697f6bdd-8d5d-471b-8a9a-52eea8f7863b
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 94080be5-4730-4fcb-8309-f9267f52adfb
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: a305b3c9-1987-4962-8625-a1fbe937a3b5
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 035bc7e5-fba6-4806-b39a-7959bb3bc067
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 97044bfd-7319-43aa-b5ba-08979f8d131b
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 6b018f0e-dd5e-41a2-afa8-ed3d37b5d8d9
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 20f084f0-8aaa-4f2d-9b8f-dc8bb09e8da6
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 8c0c26f1-3c37-4782-a51e-91fa8239f83a
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: d8b2c487-35e3-4cca-9bbc-c0304e4cee1f
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 0500b81c-4674-45b8-8aa0-d3aff478c797
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 62129e1a-27d7-4c23-b7a2-7477c298c4fa
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 769a0f31-8fec-4a2c-bb77-b19651e5d972
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 60e29a02-38b5-46ba-8394-a36c0e2f38ac
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 43acec59-26ad-4052-ad62-d86b08c9b938
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 009665b9-ae6b-48a6-a0cf-5c1378fcfbb5
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 712481e9-73d1-46cc-8a00-7d3c4061be0f
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 3999e578-effc-41cf-accf-c453d929519c
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: efea4a65-25ba-4d51-861e-c9c427501df8
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 707fb742-1fd2-4592-8c56-46ac17dd5e49
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: ff5ed1d4-e1cf-4c20-9ce3-6d89b0244e28
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: bd384b16-dcd9-4276-934f-3f4ac4d5e20f
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 65c81875-4b58-4021-ae16-462dc315073b
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 2faa2c5d-28d2-4fa9-bd66-ae5321aa244c
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: d07ec300-2300-4d20-91ba-5dbc2cf8f0d3
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 79a40bc9-a564-4986-9381-aa005f0f6950
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 74df32bc-0d3d-408a-8db1-2c2e5b6a7166
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: be4c80af-ac1c-44df-8ddc-569a8fa000d4
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: 1da938dd-b715-494e-ad1b-1d7bef6f755f
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    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: fb257292-cfe6-4caf-b646-9b7e8efe5319
    creation_time: 2023-01-27T16:29:43Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm2_valuebound10.c'''
    task:
      input_files:
      - ../plain/lcm2_valuebound10.c
      input_file_hashes:
        ../plain/lcm2_valuebound10.c: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm2_valuebound10.c
    file_hash: ee2daa1dfbe0d64b8ede4504c07bcca5b6f9048af3b92abbef97ab933225d42e
    line: 23
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
