- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 91d6a292-b4cc-40e5-9b74-35eb862e8cdf
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 14
    column: 3
    function: main
  location_invariant:
    string: 50000 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e96b38db-935e-4b0c-aea1-3dfa1c7a599e
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    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: 30fb41c7-e402-4c6b-bc62-53c7092a409e
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 14
    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: baec2a73-0917-4c3d-948c-25dab4514f23
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    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: a8419352-7cb0-4839-927c-d2b4a6397db6
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    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: c4b26852-4508-4200-8c77-069877b565fa
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 14
    column: 3
    function: main
  location_invariant:
    string: x != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7294f8c-300b-4251-8931-939f7210c2c2
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 15
    column: 3
    function: main
  location_invariant:
    string: 50000 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 15ab41a9-6221-465d-a29f-62b191cde1a2
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 15
    column: 3
    function: main
  location_invariant:
    string: 50001 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c7b2835d-d826-4598-8004-3eccac5af17e
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    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: ce7d4de3-e841-40a2-aae2-6c2e5359571b
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 15
    column: 3
    function: main
  location_invariant:
    string: -50001LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b5648d97-0ac5-4b5a-9fba-4c079686a672
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 15
    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: 0f8d584e-6735-403a-8dba-3de8fd342757
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    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: 5c668f9d-bdad-4ea7-b0d1-484b4e0de710
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    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: fdbd1ad6-8f44-4b1e-82c5-741ea98c0b30
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 19
    column: 2
    function: main
  location_invariant:
    string: 1 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 928f5444-bc9a-4094-9964-4c68b98f12d0
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    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: a3c0cc14-fafd-4113-a365-144a89a6a309
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 19
    column: 2
    function: main
  location_invariant:
    string: y != 0
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 22cec500-aa95-4c9d-a781-cbeb31027090
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 20
    column: 2
    function: main
  location_invariant:
    string: 0 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 849ce19c-bd63-49a3-9998-c8cd2c4eacc0
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 20
    column: 2
    function: main
  location_invariant:
    string: x <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39029c06-c9b0-4ae9-b15c-1059631646f1
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 20
    column: 2
    function: main
  location_invariant:
    string: y <= 2147483646
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c4c3a05c-9641-496e-9b94-82f071cf1928
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 20
    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: d5ad9b7d-7896-4bfb-bb9e-07d0b7a5afd4
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 20
    column: 2
    function: main
  location_invariant:
    string: y != -1
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ba34ed3d-cb91-4669-91b4-4a27fb9a07fc
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 22
    column: 1
    function: main
  location_invariant:
    string: x <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a7966768-35fb-4f3c-b964-d37e7f001589
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    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: c6f66c1e-5a8f-495b-898f-acf1e6d5c73d
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    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: 9b7e2814-92e0-4425-9d8e-25f2059d6e93
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 11
    column: 5
    function: main
  location_invariant:
    string: 0 <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dd808b10-803b-4ff4-82fa-8dd04d120a42
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 11
    column: 5
    function: main
  location_invariant:
    string: x <= 999999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bfe892e1-a799-487f-bedd-aa5628ae88c1
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 11
    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: eca2b2d0-de82-47cb-8e4c-5d5be64c968b
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 11
    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: 98981a37-54cb-4617-a9ce-c31b91213a40
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    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: 428bf8d1-bf1d-4e0f-aab7-9fa0f2c237d8
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 12
    column: 3
    function: main
  location_invariant:
    string: 50000 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9a010ce3-146a-4d77-a026-631400f50a2e
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 12
    column: 3
    function: main
  location_invariant:
    string: x <= 49999
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4441004d-f921-47f6-ba1e-43c3b2338522
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 12
    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: c9761ced-b324-4542-895c-e4a2d8456024
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 12
    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: 29581c5b-d8ad-45f0-b142-562ecc5d6e6f
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 18
    column: 7
    function: main
  loop_invariant:
    string: 0 <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6582e59a-f2a9-4f96-b0e3-77fab499e3ce
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 18
    column: 7
    function: main
  loop_invariant:
    string: x <= 1000000
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: d3be3658-1dd9-4afc-8b4d-430cbd3c1486
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    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: 0f5998a9-8147-4dd8-af0f-f83f74751642
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 10
    column: 7
    function: main
  loop_invariant:
    string: 50000 <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c216f641-e999-44ad-a5d6-cc4f47f15574
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    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: 7bc5b194-559f-42b9-8300-829c42313464
    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_1.c'''
    task:
      input_files:
      - ../plain/mono-crafted_1.c
      input_file_hashes:
        ../plain/mono-crafted_1.c: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_1.c
    file_hash: 00e8f12f1d0e3d2fc679744754ceeef2daa37b874cd8db07b5ab8c35684165c0
    line: 10
    column: 7
    function: main
  loop_invariant:
    string: -50000LL + (long long )y >= 0LL
    type: assertion
    format: C
