- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d71e5596-0791-48c8-99b5-3957f00f5d19
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: c4587559-8e5b-4cbd-a3d3-2c9c80b5df07
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: 922a00bc-3ce0-43bd-9938-535b56188d91
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: 744e86a8-444a-445b-a3a8-96a9804cd6f9
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: df58418a-c71a-4b53-8023-ac0a9977abed
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: 32c23cb1-4b24-44db-8088-ea0d4fe23600
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: c3c27e29-32c5-4839-8db9-46428b231313
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: 2449578a-cbd8-4b22-bd28-ca0e1dae417e
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: e63c19f5-bb40-4db7-ac5e-8c9f8439dfdd
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: 9c626f89-fb40-4c53-88d1-d51acc453063
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: 646f2d0f-778c-437b-9c22-d75d920d050a
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: 6d0cd6c4-c9cd-4675-8d01-5e2679fa5668
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: 0659d71a-51da-40d5-ab05-f2bd39fc0f93
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: 983dc8d1-8537-453b-a504-2c667ee2a4ae
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: afcc9d90-8163-4d3f-b064-d76ddfd8707e
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: aa36a123-2a8a-4ddc-ac1e-ed646a4dbeb9
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: 5d250d0f-bb51-40ea-a4ff-768c71b98492
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: decc829a-3e9b-4103-9483-14c08c812a8c
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: 92b15a95-24b0-4756-8e79-a4f022a006b8
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: f1cf2b8b-f908-4c72-81e4-c3d58865355c
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: 41119d4e-c8de-41e7-9652-3945301da442
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: e2edc3c8-ad2d-4e98-ba4c-613ab1fa6f74
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: 27c69c24-efda-4382-adbc-af247971d2d9
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    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: 87eb46f0-1d5d-415a-bd44-8da5bc10d31f
    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_8.c'''
    task:
      input_files:
      - ../plain/mono-crafted_8.c
      input_file_hashes:
        ../plain/mono-crafted_8.c: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/mono-crafted_8.c
    file_hash: e1972ee33272415a52c6f0d8a1f799e9d488ad771872c0cf36a214b07ea597fd
    line: 11
    column: 7
    function: main
  loop_invariant:
    string: x <= 10000000U
    type: assertion
    format: C
