- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a912ce1c-1ccc-4157-b619-6b39d4efaae0
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 13
    column: 2
    function: main
  location_invariant:
    string: x <= 9999999U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80597b06-4a60-4a9e-9638-85e48d2ffec6
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 13
    column: 2
    function: main
  location_invariant:
    string: 9999999LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 79f8f1da-9a5a-4553-a42d-c9bf9b74f60d
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 15
    column: 2
    function: main
  location_invariant:
    string: -10000000LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b874ad4f-7cc0-4a4a-9afc-ec752fc44b20
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 16
    column: 2
    function: main
  location_invariant:
    string: -10000000LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 842ba07f-8ac1-4d2b-9c5d-14c24749406d
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 7
    column: 13
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d5eb39c-1c66-4a8b-813a-b154d776841f
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 7
    column: 13
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f909df8e-189d-4fa0-8bba-505ccc8d9f38
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 7
    column: 13
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a98702b-e85c-4748-a8ee-258ad956e498
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 7
    column: 13
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a9968121-fcee-4f69-8334-9af5e5c91f60
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 7
    column: 13
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 30ce18ac-1138-418d-9fed-39876d906d68
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 7
    column: 13
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8961d7a0-aa76-4302-82a4-c227265389e2
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 8
    column: 13
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef7f7ea9-7a7f-44e8-9035-d1b70ea1ffb7
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 8
    column: 13
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 23791d0c-543f-4123-9651-228d48805993
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 8
    column: 13
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 03313002-33cb-4f6c-9c15-26ff899a89e7
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 8
    column: 13
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8d0d8403-1342-4668-aaf8-dbd8635e3b06
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 9
    column: 13
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: aa8b7ba1-58da-43d1-bd6e-4c533583ceda
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 9
    column: 13
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 09c7c21a-7e3d-442b-b5e5-27447b39ba45
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 11
    column: 5
    function: main
  location_invariant:
    string: x <= 9999999U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6becf380-981b-4c4e-af35-d02c025f4b47
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 11
    column: 5
    function: main
  location_invariant:
    string: 9999999LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2e506353-617a-4568-8942-65b12a7971e1
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 12
    column: 3
    function: main
  location_invariant:
    string: 5000000U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fd292729-2d1f-426a-9367-6554fbef0eea
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 12
    column: 3
    function: main
  location_invariant:
    string: x <= 9999999U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b4b5f949-1fbc-4485-a500-7ce9656c4ccc
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 12
    column: 3
    function: main
  location_invariant:
    string: -5000000LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0679863-36f2-43a4-96fc-9c06959fe717
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 12
    column: 3
    function: main
  location_invariant:
    string: 9999999LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: af5abfc4-4142-4afa-85b3-0eccf3c82c33
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 12
    column: 3
    function: main
  location_invariant:
    string: x != 0U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: eebe1287-4033-42a8-b2e9-3dd17d506e95
    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_12.c'''
    task:
      input_files:
      - ../plain/mono-crafted_12.c
      input_file_hashes:
        ../plain/mono-crafted_12.c: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_12.c
    file_hash: 8b3f0af40c26ea2441fd1db040e489b1eca9157048527a1847377fc5afef038a
    line: 10
    column: 7
    function: main
  loop_invariant:
    string: x <= 10000000U
    type: assertion
    format: C
