- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 23cb1757-f0fd-4b0d-bba6-6294619b3dd8
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 13
    column: 3
    function: main
  location_invariant:
    string: 500000 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 42a2a36b-76eb-4a64-ae83-b6c1f962b9e3
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 13
    column: 3
    function: main
  location_invariant:
    string: x <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3e6c1c86-c518-4590-a730-e8d7f2de01ec
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 13
    column: 3
    function: main
  location_invariant:
    string: -500000LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d2a5108-21ca-4875-b9b2-ad5bf7adfc99
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 13
    column: 3
    function: main
  location_invariant:
    string: -500000LL + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 013e4a4e-5163-4d30-8d01-41abe093f664
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 13
    column: 3
    function: main
  location_invariant:
    string: 999999LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9b667305-6123-4c6f-a92d-fbbfe5a54e68
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 13
    column: 3
    function: main
  location_invariant:
    string: x != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cb0795c4-334d-455f-ab5f-ed33af355dbf
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 14
    column: 3
    function: main
  location_invariant:
    string: 500000 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2d7aab1d-c03c-458d-90db-ebd462835eb5
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 14
    column: 3
    function: main
  location_invariant:
    string: 500001 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd2d8a50-04f7-40fe-a2fa-c97e230660b7
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 14
    column: 3
    function: main
  location_invariant:
    string: x <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 843e02ae-5f04-40db-8827-dc7ae023d5f4
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 14
    column: 3
    function: main
  location_invariant:
    string: -500001LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 56ae714c-cf19-4bca-8248-0b0d30450beb
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 14
    column: 3
    function: main
  location_invariant:
    string: -500000LL + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b30bbed-5671-4f15-8707-86058f96f8bd
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 14
    column: 3
    function: main
  location_invariant:
    string: 1000000LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 940a8a41-7e80-4037-84b7-03365950e292
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 14
    column: 3
    function: main
  location_invariant:
    string: x != 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7f2bddb1-3fc4-49a0-adf0-246ccecae84e
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 18
    column: 2
    function: main
  location_invariant:
    string: x <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9bdf99d9-4e54-4bb9-9ab6-a441f27776bd
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 18
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79f57cc4-8f65-45e4-8d60-459708706945
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 18
    column: 2
    function: main
  location_invariant:
    string: (-1000000LL + (long long )x) + (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f5b5b59-0f95-4bc7-b5fc-14812eb15898
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 18
    column: 2
    function: main
  location_invariant:
    string: (-500000LL + (long long )y) + 2LL * (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dcf216f9-6308-4437-9bb6-5e3eb6bb514e
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 18
    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: 273858b3-cac6-49c6-8159-6c0c1a87780e
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 19
    column: 2
    function: main
  location_invariant:
    string: 0 <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aec05ebf-2fd4-4da0-ac3a-8e18142bd985
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 19
    column: 2
    function: main
  location_invariant:
    string: x <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 688df549-3f9e-49b8-9476-303797c811e7
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 19
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c76b72c2-c496-468f-a7d8-70eb908aa4f3
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 19
    column: 2
    function: main
  location_invariant:
    string: (-999999LL + (long long )x) + (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d758259-b2cc-4d6f-a316-1bd98bab75ec
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 19
    column: 2
    function: main
  location_invariant:
    string: (-500000LL + (long long )y) + 2LL * (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6a2b535-7197-432e-b81b-0c710faf3049
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 19
    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: c27934dc-771c-4869-86bb-eb4328370b69
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 20
    column: 2
    function: main
  location_invariant:
    string: 1 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0fee328a-0fb3-4f73-98e6-78e82c0695d1
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 20
    column: 2
    function: main
  location_invariant:
    string: 1 <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 557b7a3e-1d5b-4c2b-a6a0-e3447fa0abdc
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 20
    column: 2
    function: main
  location_invariant:
    string: x <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5942bb1b-7b07-429f-8bc1-ab1707223329
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 20
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 81e60870-d98a-4d93-b968-2b8fccd631da
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 20
    column: 2
    function: main
  location_invariant:
    string: -1LL + (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d24b6b5-6d7c-4efb-b5ca-033d3593e11d
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 20
    column: 2
    function: main
  location_invariant:
    string: (-1000000LL + (long long )x) + (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec09ef63-a908-4d92-94b2-aa6ecf160aae
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 20
    column: 2
    function: main
  location_invariant:
    string: (-500002LL + (long long )y) + 2LL * (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ef66f54-2dd1-443c-8386-e3997d410614
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 20
    column: 2
    function: main
  location_invariant:
    string: y != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 693d9e1e-4011-4fda-83f5-cb26316eea72
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 22
    column: 1
    function: main
  location_invariant:
    string: 0 <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2c5212b0-f487-4a99-a591-22674d577af3
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 22
    column: 1
    function: main
  location_invariant:
    string: (-1000000LL + (long long )x) + (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1fcc6bad-57a0-4ba2-85f4-96fe77dace15
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 22
    column: 1
    function: main
  location_invariant:
    string: (-500000LL + (long long )y) + 2LL * (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 06543765-9cd2-431f-9529-684cf33a4d9e
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 22
    column: 1
    function: main
  location_invariant:
    string: 0LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb0b7b89-19a2-42e2-858f-817adfb00ba1
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 23
    column: 1
    function: main
  location_invariant:
    string: x <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5b29afae-13cb-498c-abcd-b47d05843e5a
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 23
    column: 1
    function: main
  location_invariant:
    string: (-1000000LL + (long long )x) + (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 65562183-b8a5-49b8-aa01-bde4fced595a
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 23
    column: 1
    function: main
  location_invariant:
    string: (-500000LL + (long long )y) + 2LL * (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6f599ba2-2b9d-443f-a35d-b3195ef99127
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 23
    column: 1
    function: main
  location_invariant:
    string: 0LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 121836d1-39e8-448e-b022-a4c4292ae095
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 24
    column: 1
    function: main
  location_invariant:
    string: (-1000000LL + (long long )x) + (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bb1f567b-fd3f-42fd-884e-7d8df87e66a1
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 24
    column: 1
    function: main
  location_invariant:
    string: (-500000LL + (long long )y) + 2LL * (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b5947d51-394c-46c6-b69f-85660dc383f3
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 24
    column: 1
    function: main
  location_invariant:
    string: 0LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7ddee06c-69c0-4889-8d09-97aefe225f78
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 10
    column: 5
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 75ace30a-4ba9-450e-9e4a-c8284f1452f0
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 10
    column: 5
    function: main
  location_invariant:
    string: x <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5d26901f-b13b-4442-8a20-3427d58dea73
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 10
    column: 5
    function: main
  location_invariant:
    string: -500000LL + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a57b918e-b408-48e6-9a62-50ce15df1ac8
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 10
    column: 5
    function: main
  location_invariant:
    string: 999999LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c3a19d4b-39f8-435b-978d-c16d2e2e8f99
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 11
    column: 3
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b5ca1e5f-a848-4dea-a206-0140a5099867
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 11
    column: 3
    function: main
  location_invariant:
    string: 500000 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f349381c-9786-4319-b36b-7d8406850a59
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 11
    column: 3
    function: main
  location_invariant:
    string: x <= 499999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c2d1b115-d880-4438-b9a8-5c29a8c1ab76
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 11
    column: 3
    function: main
  location_invariant:
    string: -500000LL + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a08a430-6078-45b5-84d3-df084a5e216b
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 11
    column: 3
    function: main
  location_invariant:
    string: 499999LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a593b617-79d1-4c87-b003-866c5bcf49b7
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 17
    column: 7
    function: main
  loop_invariant:
    string: -1 <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: be5cb50d-dbe9-4b28-aad9-7dc19a840722
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 17
    column: 7
    function: main
  loop_invariant:
    string: 0 <= z
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0878a21d-34df-4cee-bab1-df9e05248f1d
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 17
    column: 7
    function: main
  loop_invariant:
    string: x <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a1478f3-94e1-431d-a2e1-4e3eba91c5f6
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 17
    column: 7
    function: main
  loop_invariant:
    string: (-1000000LL + (long long )x) + (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 677fd7d7-82ed-4c5c-9ef8-b4677dea141c
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 17
    column: 7
    function: main
  loop_invariant:
    string: (-500000LL + (long long )y) + 2LL * (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 4bf2fff4-bcac-431b-9fc3-c87fe9be0f12
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 17
    column: 7
    function: main
  loop_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f20c4ef7-ccae-4867-b406-93ea31b407f5
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 9
    column: 7
    function: main
  loop_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f0816d07-05fe-4b08-bde2-ea6b7e875502
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 9
    column: 7
    function: main
  loop_invariant:
    string: 500000 <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 036c7d25-0f29-461d-a09f-5c70b864b35e
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 9
    column: 7
    function: main
  loop_invariant:
    string: x <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6defd129-ecf8-4d17-ad3d-3e558910f230
    creation_time: 2023-01-27T16:29:44Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g353653ad6-dirty
      command_line: '''/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint''
        ''--conf'' ''conf/svcomp-yaml.json'' ''--enable'' ''dbg.timing.enabled'' ''--set''
        ''ana.activated[+]'' ''apron'' ''--set'' ''ana.apron.domain'' ''polyhedra''
        ''--sets'' ''ana.specification'' ''../properties/unreach-call.prp'' ''--sets''
        ''exp.architecture'' ''32bit'' ''../plain/mono-crafted_14.c'''
    task:
      input_files:
      - ../plain/mono-crafted_14.c
      input_file_hashes:
        ../plain/mono-crafted_14.c: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_14.c
    file_hash: 538775af36be57be36a6cd470d0ff7a3d7714753249a7d4cb9a7b907cdacda78
    line: 9
    column: 7
    function: main
  loop_invariant:
    string: -500000LL + (long long )y >= 0LL
    type: assertion
    format: C
