- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 565c6181-b89c-4117-a9ec-ae17d6b650b9
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 22
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec9f5c30-99fe-486f-938a-7041e3d58c04
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 22
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 21c0e1d2-5f0d-4fdb-bfa8-c4840cc47569
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 22
    column: 2
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd106f25-009f-4217-bc87-082c42beb4a9
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 22
    column: 2
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 36a3f673-f840-45a0-a6ba-ca39ba76d80d
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ead6d142-8015-4178-87d1-ae0a0d9aa2d0
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )n) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ecd8c181-1564-46ce-b6ef-fd12a2ac05d2
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    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: 498056d8-4415-43d5-84ac-507b612de89a
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 1U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc3bad3f-67f0-40e1-bd77-101f1c97e7e3
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 1U <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3cf1b7d2-ce83-49e4-b89a-85d33c97bf93
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 26
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4beb6b53-85d8-4fb9-99da-8fb3ab6517e6
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d6a2383-8f6e-4645-ba6c-c492a76567c6
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99706d18-72c0-49e7-b99f-d429d3d394a6
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 26
    column: 4
    function: main
  location_invariant:
    string: z != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a92b80e-e063-479c-92ed-d96db914f6ca
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 1U <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e6abff10-3c4c-4a48-acee-f816bacec7c5
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 31
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c870fa5-e9f8-4e85-a089-4e1555fc964a
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 31
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b76aab95-6b81-46ce-a756-87bce7295c7c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 31
    column: 4
    function: main
  location_invariant:
    string: (long long )n - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0bbf73bf-7f87-4458-8d7f-6c630e71a579
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 31
    column: 4
    function: main
  location_invariant:
    string: y != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ac46a36a-b582-4fef-ae1e-11540102206e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 32
    column: 4
    function: main
  location_invariant:
    string: y <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63e2b451-f9a8-470d-8458-74a70971609d
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 32
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26bc3cb4-7a83-4f08-82d7-d10a2b90ce4d
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 32
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )n) - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10b16578-0ce8-4f5a-a8c4-883435b41c3b
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    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: c8b47c3f-fa19-4bed-91d7-4551feec2cae
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 32
    column: 4
    function: main
  location_invariant:
    string: y != 4294967295U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fbece317-3134-4cba-9e1f-5c945240f1b4
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 37
    column: 4
    function: main
  location_invariant:
    string: 1U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d60bf5b9-2607-4fff-b2a2-5c62d82546cc
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 37
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 041a6478-1e01-47af-94e7-a11b12437ecf
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 37
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 64243dc8-a535-4249-9f04-d2192ccea575
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 37
    column: 4
    function: main
  location_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7bb853ae-1ce7-4d55-b763-6f04acb28fb1
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 37
    column: 4
    function: main
  location_invariant:
    string: x != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1efa2175-3404-4e9d-9879-8657e6b6f377
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 38
    column: 4
    function: main
  location_invariant:
    string: x <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dbf41960-a266-4b0f-aa50-4501215ec9c0
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 38
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e972d18-059e-4dc8-937e-7bb9accdd475
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 38
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )n) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7d88c3af-94e7-4081-a9f5-d2b11232e95f
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 38
    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: 8180d0e3-3025-4516-9a6a-be8139862267
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 38
    column: 4
    function: main
  location_invariant:
    string: x != 4294967295U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 692a66b5-b26d-4093-8ff4-2caa615c265a
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 43
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 859e0e27-2b56-4a2a-9c54-6025ccc64c9b
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 43
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )n) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7831e99-1b21-4346-ad45-c386286b5fed
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 43
    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: e5da08c9-b52e-4cbd-82ec-3fc990be297c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 44
    column: 4
    function: main
  location_invariant:
    string: 1U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 429a904e-2ef9-45f5-9098-b9a021a16188
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 44
    column: 4
    function: main
  location_invariant:
    string: 1U <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a183f31-9db7-4231-9c94-942416711ceb
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 44
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 23619ed3-5e6a-4346-982c-f4d8dae3a9d9
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 44
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef4e4302-4175-4041-a47b-9b2d75be008d
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 44
    column: 4
    function: main
  location_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 98325dd5-88bc-4c5a-869a-9cf5f190629e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 44
    column: 4
    function: main
  location_invariant:
    string: z != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d375a89c-6ff0-465e-b6ab-0160ff71bcf0
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 47
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: acfc0833-cbb5-4a69-a098-b792d23fde88
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 47
    column: 2
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ccb281ff-caac-4bc5-9191-e4dbf5f06370
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 48
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a389bf5d-8cf4-40f7-9fb2-ca73f8ba3276
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 48
    column: 2
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 715da46f-6a64-4952-ae86-38cda3067262
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 14
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee677467-e88b-4e91-8e75-fc272b5b216e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 14
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b2384f1f-a4a1-4f99-9708-aa19cda2c987
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 14
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b09e9dc-99c0-4272-a75f-4aa5ae289fbd
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 14
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 16eabb9e-11ec-4949-84f7-a0866cc87fcf
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 14
    column: 15
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 47bfdda5-ca34-48b0-9507-903428898e85
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 14
    column: 15
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c3a87044-e660-46c8-9004-014a78c93d42
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 14
    column: 15
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 49d84b8d-d764-43ac-9493-8d04756eca1b
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 14
    column: 15
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c56ad2e8-0305-4698-b03c-5930dbe9e255
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 15
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 903a0f05-d495-45a9-a42b-a547553b171f
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 15
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4f47b05b-76b0-4696-b9c4-b6afef5ba8e2
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 15
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec2c1bb2-2942-42ea-9650-6d80ab96ad8a
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 15
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76ed9a2b-91fc-41da-955b-5de82f5c7ce6
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 15
    column: 15
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f47a1461-7ced-401f-abe0-0ebb6030d9fc
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 15
    column: 15
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d924ee9a-0493-4949-bd63-4f45eb81b998
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 15
    column: 15
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e63f7c22-4cfb-4850-9acb-362d986daa24
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 15
    column: 15
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 72dea000-12e5-4c15-ac7e-40caec3f4d75
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 15
    column: 20
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 828b4c33-137c-4872-922e-4338c936b2ed
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 15
    column: 20
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 066378fa-c4ff-40d1-a624-8af9d0cbb54b
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 15
    column: 20
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a5165d7-7e19-41e1-a1b8-463fbbf8aab6
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 15
    column: 20
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 70370be8-f883-4d55-ae30-388eb88a530a
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 15
    column: 20
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fedf8a36-b62c-48ac-a210-b208bb92e87a
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 15
    column: 20
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f51cd25-08e3-4ee1-9362-529c29d76b77
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 18
    column: 4
    function: main
  location_invariant:
    string: 1U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad621da5-1c49-4c03-8d6f-d9595e9f9caf
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 18
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9368707f-df65-4b04-aca5-0e8c85bac7cd
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 18
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77704ff8-55f8-402e-bee2-6826a4c8fd53
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 18
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 90f66ca6-8306-4745-a7c4-ba8dc8a542dd
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 18
    column: 4
    function: main
  location_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b7e8e51c-f26f-4039-8434-6d83fdf14d30
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 18
    column: 4
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 770696ce-6449-48a0-8136-26092c894117
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 18
    column: 4
    function: main
  location_invariant:
    string: x != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 86dae4a7-271d-4f67-9241-d3ff3fa5fca9
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 19
    column: 4
    function: main
  location_invariant:
    string: x <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e5002f6a-e789-4b70-8c98-ac3d6007303c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 19
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3605d365-69d3-423a-9f86-30bd9af36fae
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 19
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec335eca-ac99-4663-8994-b8517f4d6d43
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 19
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )n) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ca2e0ae9-f0c8-4004-b355-c2ba5d44e474
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 19
    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: ff92322a-23df-47d3-b6d3-22e194c59ddb
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 19
    column: 4
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: df7fa3f0-b94a-4ab9-abcc-2b06c78dd90d
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 19
    column: 4
    function: main
  location_invariant:
    string: x != 4294967295U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 611a50c5-5627-499b-99c9-f2a73c752db4
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 23
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cf3218eb-88d9-4fbb-9a2d-8ebb4ed6ff77
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 23
    column: 8
    function: main
  loop_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1697f3f8-25ce-4f05-bbe1-06f091aa91af
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 23
    column: 8
    function: main
  loop_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cf4985a4-9353-4889-9127-ef14814b0e75
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 29
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 654f43b7-ba4f-4798-aa64-b2c613c8d43e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 29
    column: 8
    function: main
  loop_invariant:
    string: (long long )n - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 96dc8146-672d-4166-8652-f7da2c333803
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 29
    column: 8
    function: main
  loop_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 031340dd-8323-47fa-88dc-575864e60aeb
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 35
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 20e838a0-dfb1-4952-a91d-9204addb3492
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 35
    column: 8
    function: main
  loop_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d1a63af7-87bc-4a15-937b-90bf3e4bed06
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 35
    column: 8
    function: main
  loop_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 844295f0-6c64-4d6c-8e67-7681bcb4b35c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 41
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ebf41a52-098e-4b63-8287-7bb32b409921
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 41
    column: 8
    function: main
  loop_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 37591667-33a9-45dd-bb30-20168f6c01e1
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 41
    column: 8
    function: main
  loop_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 163651e7-9b19-4d93-91b1-b19a2b2e57dc
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 14827617-0e07-44b8-94c0-b835af3c985c
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f9db4a79-3a8e-4978-9caf-ab1cfcdbdab3
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 52564c40-fde4-4a7d-98d1-162d7b3e5dfb
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3b392041-5c48-42b7-825b-852bb4aeda2e
    creation_time: 2023-01-27T16:29:39Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/in-de51.c'''
    task:
      input_files:
      - ../plain/in-de51.c
      input_file_hashes:
        ../plain/in-de51.c: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de51.c
    file_hash: 6b650e50691cb35e1bdf008faa87d25716bf83c58902e8bffb444ab81952ff19
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
