- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 28844903-1406-4127-8981-4d7b6ae21844
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 14
    column: 2
    function: main
  location_invariant:
    string: x <= 9999999U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b19b2a7f-648c-4e23-a506-b3d3ba3783f4
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 14
    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: 53f7d350-1a45-413c-8d18-ed8b08b1f020
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 16
    column: 1
    function: main
  location_invariant:
    string: -10000000LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 81e14cfb-fec8-4ce0-b7cc-e144211b962b
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 17
    column: 1
    function: main
  location_invariant:
    string: -10000000LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f77ed6d4-a2ba-4dbc-9aaf-b24b88e7b0da
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 8
    column: 14
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f8325dd3-4cac-4e37-bdef-8c14370f541b
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 8
    column: 14
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 87c1165a-c112-4947-b854-397de517000d
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 8
    column: 14
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2555e490-0fb5-4c11-9e91-c5917923d2a8
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 8
    column: 14
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d186468c-86e0-44e7-a281-937f0dc97961
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 8
    column: 14
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6634c00b-0c2c-4287-9e75-d12667d2caf9
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 8
    column: 14
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 58d0a9e7-8692-4912-9116-9124a12431ee
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 9
    column: 14
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: df5e7503-4763-45f6-a7cd-f99a596f157b
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 9
    column: 14
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10b73dff-25a3-458b-aec7-c5140f711ada
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 9
    column: 14
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 54042165-6f29-45ca-ba27-a2b099768f9a
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 9
    column: 14
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 538ad0c6-850f-4a87-ac53-c235a3ae1039
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 10
    column: 14
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 66e0aa38-d77a-40bc-9cbb-decafdb8d941
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 10
    column: 14
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ac2cd034-1d56-4010-8776-1f304da066bc
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 12
    column: 5
    function: main
  location_invariant:
    string: x <= 9999999U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bdaf0c3d-2088-4f5e-bd9b-9c6eb311b066
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 12
    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: 39d07e96-c6f2-441d-84b7-682141e9eeb7
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 13
    column: 3
    function: main
  location_invariant:
    string: 5000000U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f9607bea-8a01-425b-87f1-bc49356b19fb
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 13
    column: 3
    function: main
  location_invariant:
    string: x <= 9999999U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f6ce945d-96fc-424e-98fb-e0c3ba94f99c
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 13
    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: 60098749-673d-4052-a2ed-0be25c03f8eb
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 13
    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: ada073ad-7333-4619-98eb-4f9dcf8e46c8
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 13
    column: 3
    function: main
  location_invariant:
    string: x != 0U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 7a7375aa-d5af-4bd9-8ee7-4d6caa0d878d
    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_10.c'''
    task:
      input_files:
      - ../plain/mono-crafted_10.c
      input_file_hashes:
        ../plain/mono-crafted_10.c: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_10.c
    file_hash: 8c5f43b3e9ff1d4598a5a525fe9e716f863331c4c517b4b8adb0491943243286
    line: 11
    column: 7
    function: main
  loop_invariant:
    string: x <= 10000000U
    type: assertion
    format: C
