- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6b2569e8-22d4-4474-90e0-ff14d3fe739a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 1f7e8803-8a2e-445f-8340-0dee92aad15e
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: e9194fc5-76ca-48c9-82f1-a919806a3645
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 02fb2f41-af9e-415e-aadd-7def0f07e255
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 9bf82f23-1d63-4bfd-a5ff-8929890ac545
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: f9a9ef42-4cf7-4d83-8882-1a5c6a3dc0ec
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: b8e1a6a6-c2c1-4270-8a3e-9592705bfe7f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: eca7bb55-249a-4cf7-b130-92cee9692ad6
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 4365911a-b54f-4175-b506-a2e2204c64dd
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 959559da-21de-4523-8484-f1a13e76800a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: aa9f09a8-3bf0-4c23-af2c-2f5582becdaf
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 276bb5f3-ccc3-45be-9e2c-f7965519d604
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: d76a05c1-6bd5-4f04-a503-cf55d13f71cf
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: e19925bd-1e86-4f1d-8f16-4416b1fc082f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 2dd1d894-1430-4765-9b92-cd7016a9d276
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 03d642bb-b2bc-4ec9-bb21-68530dfc6e84
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 71b4e7ee-eb00-4e2f-b5be-0a7c966c2b6f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 7291cfde-2d77-4668-800b-59439d5279d5
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: c5acad2a-8f9f-49b0-819c-67c8ec387ca7
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: ba348fe3-4e75-422c-a525-281b3790808e
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 9cc456fd-f2b6-43b5-bc98-210ed1430521
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 74166ac1-1133-43ef-bdde-eb26a42622bd
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: a4ef775a-81ab-429f-bc18-f8cc1324549b
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: f4d94038-fda4-4ff4-ac30-46acdc98b76c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 626f156f-cb33-4444-98a5-e3b94d64e61b
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 9f78c149-49bf-474b-9ee1-42aa3bd1f7ad
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 90645258-7713-40d1-af14-1ffda51d8c55
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 74d58855-026b-4bf6-88cf-3d5075585a13
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 8f4ef481-1def-4ac2-b38c-04e4b54a3ce9
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 2b480c22-69e0-44e8-9199-0cc91d7f0e84
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 61a1df44-be8a-46ad-b9f0-5b5cdc7347dc
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 6ae08c83-6b78-4ef4-93e1-e063b286ab5c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 59c45a58-7685-4549-bd56-fff1b8453963
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 32457eb7-5634-49d6-881a-63c0e361a810
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 43eda2ce-4b99-4b63-b74e-357f699d9f22
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: ac582990-1340-416a-9d0e-c4a1e770bb39
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: a0fc42a3-ea9e-4088-849f-cd582c2d418a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: d840c6c2-57a0-4a49-bd80-97db87feed07
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 2232fba9-c6c5-4d4a-9d46-c395cb5750cc
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: cbb136b6-626d-4c92-ace3-38b7d0adf3cc
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: dd58c363-5683-4bae-9ce5-a53d6cb480ed
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 1cc47a03-17b4-4941-8a04-9cb6ea37eac3
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 221a4224-68bb-48a0-a4cc-7fee51540589
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 914ebf2a-b74b-4419-98ae-9f3839ddfcea
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 274d0bcd-882f-4c7b-a6e1-28142a2535dc
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 90b94a96-fdcf-472e-93b1-a2074dd645f3
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: a0259f75-6c03-4fc7-a964-4757cd16f0a5
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 3dea61c7-ae19-4c8d-aeb6-818730c9f974
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: c104abf1-71e2-457b-86e8-5278547ed459
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 30bb9a38-1585-456e-92fd-0ea779f78b05
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: d99c77df-af78-4551-b86c-6839b2d6fef6
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 1035d2f6-0fce-4936-94e3-75601d57a13a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 56b7c3b7-3c53-40b9-a970-9f704f7f5391
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 27c0ab5d-521d-4879-907b-997608d688b9
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 93c35bf1-bbf6-4006-9e20-829f2130583f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 07a7ecfb-43ca-47a0-9bf6-ad7b2734dd55
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 22bfcf66-9a47-4c06-9961-1b58b93e98a5
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: b91c3a8a-a1d5-43c9-8374-1576b08c47c3
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: cb245727-66dd-4c51-8ef3-d43da16868c4
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 1a96a61a-328e-40d5-be3a-70e7cf173d62
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: c57403b5-d8e0-4058-93b9-05a699792a27
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 23dc36e4-5665-4548-a0b0-32c5a884671e
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: f78ad81c-cf9d-49a2-b07d-bd7f7e7212f4
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: f65ce360-598d-4c37-9d12-752cc494d441
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 71836c0c-7774-4e98-8de1-76b9fbaacc5a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 0688770b-529d-4923-bf52-10745ca0310f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 3d09a4ad-b8cd-4262-accf-8ed1e0397cef
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 4fe6848b-767e-45ee-aeb7-808d6971544e
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 1e3b098a-2cae-4ee4-ac43-b3192e4ad641
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: ea188b2f-c3c0-4bb6-8b4c-625cb3dda988
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: e2d72e7b-b5fa-4cd6-9cb1-e491b18ee85d
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 9ccfd4c3-6058-475c-bc0b-a3d3eb899e83
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 58eb0d2b-6009-4a05-b369-0031781344ff
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 5e7a5857-b522-4b45-96f4-3b6836f3975d
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 3dab879c-9496-42c3-bc3e-231d0848f46f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 45c59fed-8fff-45cd-89a4-3775480d2f0e
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: ae102801-2acc-40b7-9c07-0b410e85b2c0
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 0f670640-88a2-4d37-8330-e736ecdc50db
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: e569daf1-618c-4024-b818-8a85d27186c6
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 613a12e3-a606-4d49-a7f9-d54522862878
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 7876306f-6e48-4d4f-8de1-f81df200c090
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: d54701ba-7a9a-46c5-9241-e46156c665a6
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: b8dd8376-7180-4343-ad35-6f7cf394df91
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: ffab733d-c70f-405c-b0f1-a268a8fa7aeb
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 9955622f-1ffd-4c3f-a656-c8984e7d1730
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: c3713ffe-cea8-49c0-89e5-295f011e4192
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 793dc66f-0630-4938-8613-80c829064600
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 60a120ee-71cd-4973-a282-a51150690517
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 810d7616-6626-46ac-b7a1-6782214cc4ce
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: ccfbb4f8-0d00-4875-a8df-99dfc314ef6e
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: dc25f87e-fc68-4b89-b418-d380784ed3c6
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 80a64734-e087-4247-97b0-a1d8d72a3592
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 1ada5932-b860-473b-ac48-14a0694629d0
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: eadd33cf-12a1-4c43-b7a7-3ceb753ae3e1
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: f9c29fa6-d485-4f5a-a657-c9164a62f20c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 5a2401f5-1ab2-4a24-8e64-c8f62d17faf3
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: b0e0f1d6-f4a0-4542-b4e2-92c919f1cc0a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 44046ae3-ac77-456f-89f3-0722daa725d8
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 99333704-4c27-4e94-ba3a-0641987da580
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: bfddebf7-435a-4686-b4b4-08c5c888c344
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: bdddf8e5-d09f-4f07-88b4-1f1a1bde01b9
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: c3322ac5-206a-4288-af33-85bcdc16d5f4
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 989a73e5-c079-4022-bda5-4213babdecab
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: cce4007d-bcca-4110-81f5-8b1c5d4e60aa
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 07b60e6a-46d8-415c-b5f3-6392b040277a
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 97431268-b271-4e40-ad9b-238efe6abed5
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 1469daa5-f8aa-4208-8e35-6802e2360b0f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: b7990687-27cb-471d-b603-fd584d7685e7
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 26f92481-47eb-4850-99b4-815e7fea4392
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 6fdf3ee7-3028-4e06-bbf7-d05c8d09c4dd
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 108809fb-f968-4106-a5fb-e035bcec64f5
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: cd57ba91-14b2-416b-8666-9148b60191b7
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 9808e5d8-8944-4d44-a22c-30ab117fd1d6
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 9ca97da4-5a80-43c3-95cc-0d2dbdba54f9
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 51ccbea3-b5ef-4091-aa3c-775d11d0d429
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 5d48a7e1-2517-472d-b324-8c86a7119107
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 5221d387-3a7b-4a51-ae95-8c9cf94bee91
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 6d5ef489-5065-4fa0-8049-1a7e48c85dc5
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 4f518624-30b0-48de-b48c-418d79a62bf9
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: facf1631-f168-4800-bd0f-02064cf8874f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: b9d8bc49-fde6-48be-9cac-c0e3c98037ef
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: eab11158-4210-4ff5-ac20-f850e078e69c
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 545f85db-3585-41ef-91a0-0c924b8e27b1
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 869a8c33-e838-41de-b17c-954d5b99581f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: f86e8904-ac06-4ced-adfc-bd104afce272
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 7fc5fbad-8506-48b5-a22d-e04320d2c675
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: d297fa9b-fed3-4f7d-bc21-735454d274d1
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 7c10646c-ec8c-4e9e-9dd7-9c8c1a444072
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 52fb1fe2-afea-4c7b-a17f-9f59e9d4ec10
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 720252ae-ca3c-46f7-b574-7a6df63b7454
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 39efd025-60f2-4522-a9bb-08ee48b6af99
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: 974be1cc-c2e2-4b5d-b432-c795f7606d0f
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: b6271221-da0a-4e7e-8c1f-ccbd01ec47f1
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    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: ce30d147-46e9-4b53-8f8d-9930232baecb
    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_valuebound20.c'''
    task:
      input_files:
      - ../plain/lcm1_valuebound20.c
      input_file_hashes:
        ../plain/lcm1_valuebound20.c: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/lcm1_valuebound20.c
    file_hash: 21cdb68b157f5f8b7463533f545ac6ba72a59d04f7166c24abe2ffbb265d260d
    line: 53
    column: 15
    function: main
  loop_invariant:
    string: (long long )b - (long long )x >= 0LL
    type: assertion
    format: C
