- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73a9f299-1514-49e7-8dc6-57138062c5f5
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 27
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f7efb0a3-4555-4e2a-860d-cd4fb901cdb6
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 45aa0b22-523e-47b6-9a9a-ff0c5a69eef9
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 426d5a88-6be7-4b88-b68d-b65c50d065e3
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 2cf5948e-7ac4-45f2-92ba-8277a73201ec
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 9313d92f-d8f8-467a-b91a-7e89df968b88
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 27
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6c850991-b721-474b-b5fb-2a9425b2ddd7
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 5ef37c1d-e17f-498e-82ae-f4268424cfd0
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: e9dc9e4d-90ef-4ba4-bb45-d3405f5b363f
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 2f555d67-1521-43f7-a66c-21dfc4298d59
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 1109cbd2-d681-48ed-ac8a-6ee40612e18e
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f95d020-29ed-4a10-b49f-50889ae04ed5
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7c78bd18-cb5e-47ba-adc4-ee9ab42c6adc
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 35823c8f-45bb-45d8-a47b-7fad085e127e
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c3e3486-4886-44e0-921d-a6f295a3bd42
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 28
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 593418cb-cf21-4b62-85d0-a3761454f4b0
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 206de14d-e1c3-4238-b1f1-ff8c6a05758f
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 591461f1-4cf2-4b71-a024-18a8c4025f72
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9fc86695-593d-4ba7-8a79-53f948137685
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 67b95d75-122c-4a48-818b-8e30dbdad647
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 28
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 37d3f89a-5355-496a-bab5-a7afe2cf7bef
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: d94bdc27-0b9a-47c6-a75a-9059d7b56da3
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 7146d855-96ce-4457-b780-14c98be0e53f
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: f107dc74-dfbf-4d9d-b911-e1f2d8440aa1
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 91f44d2c-0e22-435f-afd5-bc5f82b102c7
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 95c33af3-01e4-4d5e-bc30-d22a2132dc1d
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 2c7cf90d-a31a-48fa-be23-f9d7c9fb9f93
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 9f5c8d25-2da0-4147-89fc-9947c595d466
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: bfb70c65-93ca-49b6-94ba-e606451724fe
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 7e085681-6119-4916-a859-13865af46b5e
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 855a1ff1-067a-4074-9499-b099b09721ca
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 339aa71b-1790-4d6a-88b7-8b1413a29910
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: a269c858-8793-40e2-affd-aa49fbae566d
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 06daafee-f25b-4871-b8ad-b422887a2805
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: d36eb039-97cc-48e6-b3a4-abaf932b0be6
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: bef23fa3-1678-49c9-9836-d65bdbc49421
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: f221867a-5c03-4631-bd37-4cafbae259ce
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 49468c3c-3dc2-4d00-9c3b-8939818796a6
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 1f6d6bc7-9668-499b-aa83-2d29c3401962
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: f824b47f-6d7a-43aa-bdad-4275f2cb5486
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 9d0ddb68-d0c9-4f3b-80f0-df71ff9f20f2
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 9440f8af-f9b9-4421-beb0-2864e76d89a5
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: b5bb4a07-3916-46e8-ae13-8f344aee4ecb
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 12384c91-cd1f-4831-9d3b-6d5c363896ee
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: a8802919-60c7-4834-b244-1dd00ba856c8
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 33
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d9d0332d-bc80-4a7e-9712-2664416e8fd8
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 1079ac54-2453-4a2d-a807-a090cba4fe20
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 1e14fdfd-9cfb-41de-8230-06d56a0baab5
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: e3ebe3df-f80c-4715-9274-9f0c9516b7f0
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 33
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6d382ced-ceb4-4f1f-b251-4d62fead5f98
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 8613e316-eea3-48cd-a60d-0a9f36e92a92
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: e3d5a048-a1fd-4a68-abac-60f411c69333
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 18199dbd-7266-4692-88d4-7b98ee0d2471
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 35
    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: b7dc8d3a-4d13-4efc-90b0-8a007bf42136
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 35
    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: b3ed3d78-b903-4b1e-a434-7a6daad7aa83
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 35
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5971917a-98f3-4d1a-a113-d2fb5cf5adc6
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 3369efbe-cf63-4d8b-8f00-ca3d4f783e0f
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 35
    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: 2a0bc134-faf3-4681-93a8-9d067805f332
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 35
    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: 9847e205-b698-4f9c-a8a3-6c603f873ca4
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 35
    column: 4
    function: main
  location_invariant:
    string: (long long )u >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 165de093-d59a-4256-80c1-b21446a1bb6b
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 906ef8ad-bcf2-427e-9d0a-51833228ae42
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 36
    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: 41972863-5f35-4658-93a6-fda249bb2cef
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 36
    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: 9a9c1490-0aed-423b-b87c-c4711290cd82
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 36
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 54282bd8-7d27-4fca-afce-6f1c97ab2ee9
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 36
    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: ad0f97c5-94f5-4df9-9066-23b31e619c75
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 36
    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: f6913d83-16e4-469f-8709-15b66b8acbc9
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 36
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0addedfc-06ec-4db7-a4cf-c47c67462bf9
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 37
    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: e6ab82f9-668c-4aef-b55f-ff92f575d858
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 37
    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: 52facac1-9608-4e18-96b3-8a3df4c95845
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 37
    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: 54ca3f6e-dec3-4e60-a721-94490ef7493b
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 37
    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: 3946e22f-e531-461b-ae56-a801adc46b8a
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 38
    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: 2be44ba2-4e30-4af3-8420-35393c3d5bae
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 38
    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: 1a610f7a-3c23-4b4d-81ad-e9611980a956
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 41
    column: 8
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b495b077-b66f-4220-a3e3-505a728f5878
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 41
    column: 8
    function: main
  location_invariant:
    string: ((4294967295LL - (long long )a) + (long long )x) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b817419-78f2-4a9e-bd65-78294a367cdd
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 41
    column: 8
    function: main
  location_invariant:
    string: ((long long )a + (long long )b) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 04553027-5f35-445f-be45-e71840f5c983
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 41
    column: 8
    function: main
  location_invariant:
    string: ((long long )b + (long long )x) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 36cde8c9-5cc6-44cb-adee-46d6c132d376
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 41
    column: 8
    function: main
  location_invariant:
    string: (long long )b - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7b67ab15-eb37-4747-9e1e-f55b887b6e35
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 42
    column: 12
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c5aa006-c89b-4b6f-919c-22d0a25f2a72
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 42
    column: 12
    function: main
  location_invariant:
    string: ((4294967295LL - (long long )a) + (long long )x) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 08511b7a-2cb9-428a-8869-fa5dd71ab0b7
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 42
    column: 12
    function: main
  location_invariant:
    string: ((long long )a + (long long )b) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b7421394-5f38-418c-8299-86fd736f7f85
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 42
    column: 12
    function: main
  location_invariant:
    string: ((long long )b + (long long )x) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b323ae40-3a62-4733-b2b5-dd64f2ab7cca
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 42
    column: 12
    function: main
  location_invariant:
    string: (long long )b - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 006896f5-1b19-40ba-887d-fbef2a841870
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 46
    column: 5
    function: main
  location_invariant:
    string: (long long )b - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e5d7baf2-a3ce-4e62-a998-21c137751adf
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 47
    column: 16
    function: main
  location_invariant:
    string: (long long )b - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14cb89ba-1010-4537-9eab-ecbe0eb2141b
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 49
    column: 12
    function: main
  location_invariant:
    string: 1U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3cf33d1c-c90d-43fa-b091-31bbb330cab4
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 49
    column: 12
    function: main
  location_invariant:
    string: y <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c40c59dc-a148-43d4-80a4-1f93d97bd7f7
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 49
    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: ab52ca7e-8074-461d-b429-a90677103169
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 49
    column: 12
    function: main
  location_invariant:
    string: (long long )b - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee315e06-53ce-473d-8f3a-0e0706776460
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 49
    column: 12
    function: main
  location_invariant:
    string: x != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75caf000-a056-4a59-bf40-f1243b81e7a9
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 50
    column: 12
    function: main
  location_invariant:
    string: y <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2630e777-f742-4f48-9e7a-0a86820772c6
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 50
    column: 12
    function: main
  location_invariant:
    string: (long long )b - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c45d46d0-5276-4da9-a562-94e205a12339
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 54
    column: 5
    function: main
  location_invariant:
    string: (long long )b - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7dd89407-47bb-4106-8657-263497cb05a4
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 55
    column: 16
    function: main
  location_invariant:
    string: (long long )b - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e75f5098-6ee3-453c-8ffe-6f19542d0ce7
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 57
    column: 12
    function: main
  location_invariant:
    string: 1U <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 134112d3-d52c-407c-b0eb-ef0872831de5
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 57
    column: 12
    function: main
  location_invariant:
    string: x <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e2be725-db00-4538-a94b-43f94ea33e56
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 57
    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: 119d7c33-f9f4-4459-bf89-74ee2d3b5437
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 57
    column: 12
    function: main
  location_invariant:
    string: (long long )b - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43d33399-ff8e-4fa4-adf7-953c3c10c0fd
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 57
    column: 12
    function: main
  location_invariant:
    string: y != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc8bdcfa-5809-410e-a670-641ece366600
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 58
    column: 12
    function: main
  location_invariant:
    string: x <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fbd58cec-b21e-4bd2-a4a8-f15804e784b4
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 58
    column: 12
    function: main
  location_invariant:
    string: (long long )b - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 86b15118-e168-4f19-a016-1e9e2671f81b
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 62
    column: 4
    function: main
  location_invariant:
    string: (long long )b - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 53152aee-222a-4b6c-9355-0bbccd4a6915
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 63
    column: 4
    function: main
  location_invariant:
    string: (long long )b - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10b4fad7-eff2-48ee-aa5b-89488f152467
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 67
    column: 4
    function: main
  location_invariant:
    string: (long long )b - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cc0f8362-1aef-419e-8556-b5d48e6146e0
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be5dab6e-fabf-4535-a057-7925c4912fb5
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 7f4135be-abb9-4050-ac9e-0eec1a756de9
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: e7df71c5-8c52-4f44-882c-ac0065c1c97c
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 14b93e84-0e1f-4734-8aac-9e4e83460e05
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: c4e8b196-b389-4689-b6e7-881d98991f8d
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: fff229be-688c-487f-888a-53bd24ec358f
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39b6cbaf-10ca-4c2e-8aa3-b18f5b60be78
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: ba66e996-229e-43c7-90c1-d7d1c47fdd36
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: b7fe53d2-029c-422a-a2e2-5deef9f6687a
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: e43020e7-a831-487f-a16a-a8793bb473ea
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: d514bc36-03a1-4432-9c0a-3f5876ea6278
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: cdea1b7b-ede9-47e3-89bf-05a34ee5eed9
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a2d0b9df-6185-47f5-88ae-d816be26f544
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba588e7c-f33b-47d6-8c4e-4ad52699ae41
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: e0ef7556-0d73-4f03-8daf-3a8565a401ff
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 4563f181-e4a9-4679-ae90-ba94024294c8
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 69ddbd7f-7d48-4ab1-9c8d-f4eb2e2b8f05
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 942ea46e-fbe5-47a6-8290-9b7f1b6644c7
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )a >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f406d39-f357-4dae-9823-5db97358e9f4
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )b >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a843de8d-5b2a-48b7-89d5-99ca48413ca1
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 9272c5db-98a7-44c5-a177-1b6eeaeeea4f
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: de13ec81-6692-46bd-b2ee-e8c706a5fd7a
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    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: 6cb340c9-caa7-4766-833d-4e57dcd9d808
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )v >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 45d62870-9029-465f-90aa-bec24ec26a60
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 40
    column: 11
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e41f900e-34a9-4509-b942-a2714af660b5
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 40
    column: 11
    function: main
  loop_invariant:
    string: ((4294967295LL - (long long )a) + (long long )x) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cfe4d3f1-5051-4492-850a-653a3b3ee347
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 40
    column: 11
    function: main
  loop_invariant:
    string: ((long long )a + (long long )b) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 8904ca1c-576f-4a49-b329-62527a5df1b2
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 40
    column: 11
    function: main
  loop_invariant:
    string: ((long long )b + (long long )x) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 602df640-9134-4c40-83f4-86b61d145d0c
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 40
    column: 11
    function: main
  loop_invariant:
    string: (long long )b - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 80a9bed9-ae26-4270-ba5b-43ce58b497a3
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 45
    column: 15
    function: main
  loop_invariant:
    string: (long long )b - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 68491c74-c980-4912-8eb4-86ff1d17b343
    creation_time: 2023-01-27T16:29:42Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/lcm1_valuebound50.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound50.c
      input_file_hashes:
        ../plain/lcm1_valuebound50.c: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound50.c
    file_hash: 8934c7d58d71c9b3a06e793f6df8377fb9dcad08c89a636c2f08c1bbd4767b93
    line: 53
    column: 15
    function: main
  loop_invariant:
    string: (long long )b - (long long )x >= 0LL
    type: assertion
    format: C
