- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b769cde6-2daa-4840-a0a1-fc1a83f3f836
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 15
    column: 3
    function: main
  location_invariant:
    string: 500000 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f39600ce-ca41-49e8-a01b-bfc98ea8e0eb
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 15
    column: 3
    function: main
  location_invariant:
    string: 500001 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1aa20ba1-9fb4-4e5a-a533-5cdfaab6ef46
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 15
    column: 3
    function: main
  location_invariant:
    string: x <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a83a841d-02db-446e-9776-6a56e2c7151c
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 15
    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: 7a5072e1-5af1-4e2f-bbff-663e6b663532
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 15
    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: 3f2dda15-1946-4dac-a514-8e42bf2b2452
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 15
    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: 111ae1c2-d0de-45f5-8372-ea18eecc36d0
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 15
    column: 3
    function: main
  location_invariant:
    string: x != 1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1c84ea76-b270-46f8-82fa-8831ca58b560
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 18
    column: 1
    function: main
  location_invariant:
    string: 500000 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 56fa5297-70f4-4c58-8da6-0f2b168d7f1e
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 18
    column: 1
    function: main
  location_invariant:
    string: -1000000LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd97bedd-fddd-4b57-b3f8-d9d500a5f71f
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 18
    column: 1
    function: main
  location_invariant:
    string: -500000LL + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 14c57763-53fb-463a-afa6-516b6b9b6992
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 19
    column: 1
    function: main
  location_invariant:
    string: -1000000LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d59b7b21-5b84-4865-aeba-42b397813ff6
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 19
    column: 1
    function: main
  location_invariant:
    string: -500000LL + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1ae934e3-e422-49ba-96ec-9dc6019309da
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 11
    column: 6
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 51728bca-239f-42be-abe5-ccc1a53f1911
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 11
    column: 6
    function: main
  location_invariant:
    string: x <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 669bd975-fc2d-4dfc-94e6-5ea988d73032
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 11
    column: 6
    function: main
  location_invariant:
    string: -500000LL + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e56ef1fb-f2af-430f-a7fd-447f6340f732
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 11
    column: 6
    function: main
  location_invariant:
    string: 999999LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 174dfb27-debd-4c21-9c68-8990657d8cbd
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 12
    column: 3
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6faca6ad-6c5a-4515-8cce-6e7ca80fd467
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 12
    column: 3
    function: main
  location_invariant:
    string: 500000 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 547a6a8f-9ba5-4bdc-abdf-abf9b6f67062
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 12
    column: 3
    function: main
  location_invariant:
    string: x <= 499999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63d46dda-e27f-4f28-bfca-aee5fb5938c4
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 12
    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: 18a9062e-99b7-4cc3-91f4-07c7e70395a8
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 12
    column: 3
    function: main
  location_invariant:
    string: 499999LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 43f7415d-c2ec-4128-b399-016f68e0fdf5
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 14
    column: 3
    function: main
  location_invariant:
    string: 500000 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d1cece3c-a87f-4e99-8b98-00c4ff0ab65b
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 14
    column: 3
    function: main
  location_invariant:
    string: x <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9ca60466-91c9-485e-ab59-f8f1cf018482
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 14
    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: 1cda8c27-9e09-493a-8781-72b285eb08c8
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    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: eefdc1de-d09b-47d0-83c9-decc5286122e
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 14
    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: 1833b012-9cb6-454a-8396-fc325848a81a
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 14
    column: 3
    function: main
  location_invariant:
    string: x != 0
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a2f5f36c-d5ff-468c-9e2a-76c3fe7e0b26
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 10
    column: 7
    function: main
  loop_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5da2ac78-3b29-414f-8a76-ee144110a067
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 10
    column: 7
    function: main
  loop_invariant:
    string: 500000 <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0dd6671e-42aa-422f-b471-753e10ef5a32
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 10
    column: 7
    function: main
  loop_invariant:
    string: x <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f25698e9-bc0c-435e-b868-b8217dccea49
    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_9.c'''
    task:
      input_files:
      - ../plain/mono-crafted_9.c
      input_file_hashes:
        ../plain/mono-crafted_9.c: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_9.c
    file_hash: c6e51ff8c9564e836040d6d35580386edd1169ec75010fdbf7c4eee4bc9fc430
    line: 10
    column: 7
    function: main
  loop_invariant:
    string: -500000LL + (long long )y >= 0LL
    type: assertion
    format: C
