- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fec121f1-920a-4cc7-a1d5-e2189ff87d5b
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: abb6b2aa-0152-4358-9d10-97594fc23587
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: 8601679e-c4fc-459b-8d9e-23a701d8448b
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: 3215834f-51ac-42e6-949b-4406bc00715d
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: affb995a-9859-48ef-a32e-82208e61131c
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: 84fc1fab-f0a3-4b18-9961-9989c79ffc58
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: 7918f2c7-9793-4f45-bd3d-ef2250aa8ec8
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: 46167f46-f8da-470d-9731-258ed0d06129
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: fbab5339-4635-4972-81b1-78ab8c1efa9d
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: e2d1467e-8f83-482b-8515-141e3785c558
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: dad0c584-8c2d-4623-8186-dea32643f24c
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: 0bde086b-8f2a-4f82-8dc6-861800920623
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: a20f3634-1a44-411d-ada8-2a8d8cb14fd7
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: 1acad8da-da7b-4be3-8496-feb032fdd65b
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: 833eb549-fdff-4225-8de2-797a6d7923ea
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: a6999340-6aa0-437c-9cbe-054fa3752e53
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: 4a550498-c169-4798-8fed-c6a34d7e937f
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    line: 20
    column: 2
    function: main
  location_invariant:
    string: -1 <= y
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5965d2cb-759c-43c6-adcc-19a51631b1c8
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: 62391fff-0711-4c3a-b84b-69a978fbf8b5
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    line: 20
    column: 2
    function: main
  location_invariant:
    string: y <= 2147483645
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4a83153f-100e-4e4c-8c8c-f48b231da7d0
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    line: 20
    column: 2
    function: main
  location_invariant:
    string: 1LL + (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd2da0e5-cd38-4d72-8812-142d19ff42c6
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    line: 20
    column: 2
    function: main
  location_invariant:
    string: y != -2
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 02bb2f45-26c1-4963-b5f0-7e36e54844f0
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    line: 22
    column: 2
    function: main
  location_invariant:
    string: x <= 1000000
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f3175c6-e42e-4e1c-8488-f0b5ed58b270
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    line: 22
    column: 2
    function: main
  location_invariant:
    string: 0LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b8ffc7d-7f16-4ed6-901d-c76359cbfbed
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: c992dc41-149b-43e0-b19e-0ff97d6682d4
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: 91f49892-8015-4762-8bf2-87c1f96dba0d
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: 5e6a8a26-9840-4d57-898c-3ebab589616c
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: 871b6285-7c99-4ce4-a913-880c3efdcb64
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: a3552809-a711-4c96-bbb1-48c99e2161b6
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: 18aa3d34-970d-4da3-a6ca-7f8696c2450f
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: 4b7108e9-a2ea-4d8b-a0a0-8f6dc22cb34e
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: 4b02f584-c2d1-4608-bf93-29930b8720c0
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: cac8b6a7-904b-499f-b288-bf88718704a6
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: 8c9de048-0091-47a3-a104-8a9c01e1adae
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    line: 18
    column: 7
    function: main
  loop_invariant:
    string: -1 <= y
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 16f40b0d-d53e-48e7-bcc4-d8fb0a14c28c
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: 37493960-bed8-422c-9e36-1d9848e6106b
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: ca0348d4-f11d-4050-8995-725f9afd15d0
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: 04b9e783-9a35-48d7-a04e-10b948b30978
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    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: abdb2d55-4550-4797-a2a4-d3a7c6bc4dd6
    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_7.c'''
    task:
      input_files:
      - ../plain/mono-crafted_7.c
      input_file_hashes:
        ../plain/mono-crafted_7.c: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_7.c
    file_hash: ae51dc9203c351522c25ee3116b2cda704928bb61769972b6b90792bfdf57f19
    line: 10
    column: 7
    function: main
  loop_invariant:
    string: -50000LL + (long long )y >= 0LL
    type: assertion
    format: C
