- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8d3c036-faca-4e91-b678-e6ff98ae5363
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 13
    column: 3
    function: main
  location_invariant:
    string: 50000 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fbad7081-ea30-40cc-94da-80160dfdd4aa
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    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: 0c7f0360-5aa1-437d-9c31-e2e55f0a28e5
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 13
    column: 3
    function: main
  location_invariant:
    string: -50000LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14dd9650-1872-4e8a-910b-a4929b9d68aa
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 13
    column: 3
    function: main
  location_invariant:
    string: -50000LL + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0648b862-0f9e-4600-bb81-fff0cfe1cce8
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    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: 9856462d-4bd4-4faf-a1f1-dc590d5dff3e
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    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: 427c0d1b-bdff-4561-8a69-7a55c632ed1a
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 14
    column: 3
    function: main
  location_invariant:
    string: 50000 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ced7c005-2533-49f6-bec1-0485957e8894
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 14
    column: 3
    function: main
  location_invariant:
    string: 50002 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: db09af9f-9b3a-4c50-9ddb-23f148001cc9
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 14
    column: 3
    function: main
  location_invariant:
    string: x <= 1000001
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b1817bda-bf05-4e2e-8e54-44938c3958eb
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 14
    column: 3
    function: main
  location_invariant:
    string: -50002LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ed8fbef6-47fe-432b-a36c-aff8cdd5ba12
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 14
    column: 3
    function: main
  location_invariant:
    string: -50000LL + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 92bce4d1-5011-44b7-86c3-baa68a8ba470
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 14
    column: 3
    function: main
  location_invariant:
    string: 1000001LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e5ec6fd3-663e-45e1-aa97-806c76772571
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 14
    column: 3
    function: main
  location_invariant:
    string: x != 2
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 009ad947-3262-4e78-9656-15d7210fb97a
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 18
    column: 2
    function: main
  location_invariant:
    string: 1 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8971133a-2221-4721-8da7-dee876c162f3
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    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: 38112012-9119-4ff7-ba40-052224266375
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 18
    column: 2
    function: main
  location_invariant:
    string: y != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ea415817-db92-4fb5-8539-db85790cdf0c
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 19
    column: 2
    function: main
  location_invariant:
    string: 0 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fa8edfa3-79e4-4a35-beba-8b158aed8ca5
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 19
    column: 2
    function: main
  location_invariant:
    string: x <= 1000001
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6748e9fe-11a3-45bc-a328-43752dff040b
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 19
    column: 2
    function: main
  location_invariant:
    string: y <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ec7a4d81-3514-41a5-ab0d-86669f15eeea
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 19
    column: 2
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 76fc4e4e-3119-4a63-a576-65b933182a62
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 19
    column: 2
    function: main
  location_invariant:
    string: y != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5483321f-591e-404c-82fd-c8ef0edbce36
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 21
    column: 1
    function: main
  location_invariant:
    string: x <= 1000001
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fb3142b5-9269-4dcb-969e-4d74c4663dea
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 21
    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: d2f944bb-f51d-4797-9511-65a330033ffb
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    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: 963f3ba7-7a4b-4171-bb68-b8904a5229a8
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    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: 937c071d-9d6e-4ea8-9edc-f2968447e192
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    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: 2cfc9693-8d68-4338-8472-1e919a8b1da9
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 10
    column: 5
    function: main
  location_invariant:
    string: -50000LL + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 18a42b64-5ec5-41d6-b592-f9dc76d5b51b
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    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: b0c5d7b1-ab26-4fdf-bb4c-f5e6283bfd69
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    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: ab321ebe-0be8-4468-ba1e-610a3f64ba3b
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 11
    column: 3
    function: main
  location_invariant:
    string: 50000 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2676d91f-754f-4057-8c88-d1dd07ce7135
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 11
    column: 3
    function: main
  location_invariant:
    string: x <= 49999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 95a421de-ad20-4d8e-9313-d453100bcfe6
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 11
    column: 3
    function: main
  location_invariant:
    string: -50000LL + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e16bc33-55b5-4ae0-968a-312a81f95dd1
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 11
    column: 3
    function: main
  location_invariant:
    string: 49999LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 06dbb7c3-3695-4d24-98fd-123e57600861
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 17
    column: 7
    function: main
  loop_invariant:
    string: 0 <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 9215f560-bbf5-4d4e-a4bd-8b807df80824
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 17
    column: 7
    function: main
  loop_invariant:
    string: x <= 1000001
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 96a90362-ad69-472a-8074-a0ed68b347e7
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    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: 44b8fe30-1348-41c6-8f51-42f00c19bf9a
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 9
    column: 7
    function: main
  loop_invariant:
    string: 50000 <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: aa31602f-328a-4118-8120-3f1dae5f5ab9
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 9
    column: 7
    function: main
  loop_invariant:
    string: x <= 1000001
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: cf8a4692-7481-4bff-90e7-aeaa0107cc9c
    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_13.c'''
    task:
      input_files:
      - ../plain/mono-crafted_13.c
      input_file_hashes:
        ../plain/mono-crafted_13.c: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_13.c
    file_hash: 7a1978d5df6cab978f117700980416150440efa7bda2d4cde0711b48b83f0666
    line: 9
    column: 7
    function: main
  loop_invariant:
    string: -50000LL + (long long )y >= 0LL
    type: assertion
    format: C
