- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 492ad129-c5b0-45e4-8d96-42d7ebbf11b1
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 22
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e6662983-5816-4dbb-a6a1-80b5d321c60c
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 22
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 740c3f73-61f3-4338-bad4-671d7d8b1e8e
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 22
    column: 2
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8ff7e0b-6caa-4e84-ac8d-3625f5a09d93
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 22
    column: 2
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 28cffb8a-44f2-49ea-b0e1-a598ad32a5f2
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 25
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 237a6396-288a-43fa-940e-da7316247e44
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )n) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fcc1444e-ceac-4472-a504-f12e783f77d2
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 25
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 04ff782f-3428-4b97-8e63-8d5b8972128c
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 1U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99433f68-22a9-4621-bbb2-b9666e6fcd40
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 1U <= z
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5ba31688-f5ff-4029-80ea-9d9c4d2ebd11
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 26
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bd120c0d-2ce6-44ca-b574-36b1b5cc0d82
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 26
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fe1c8f4e-3f14-4678-90bf-ccc5fa9973c7
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 26
    column: 4
    function: main
  location_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6cabf381-1a5b-40f6-9b6f-2d16d812f484
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 26
    column: 4
    function: main
  location_invariant:
    string: z != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ecdee57e-606c-4d54-9508-90a3e0187117
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 29
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e18be89d-afe9-43fa-a2af-df57a75aef01
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 29
    column: 2
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fe0f4ef1-e708-4c7a-a1d7-a5bf97d04340
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 30
    column: 2
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e88b7e54-3b96-4cfd-993a-c0358b5a23fa
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 30
    column: 2
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0a443252-eb3b-4aae-bc43-05a3370c41cd
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 14
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 73c6458e-df1b-4611-9e7e-e83ff99f3564
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 14
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8fc80e5f-018f-40ba-9912-26c376ff7421
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 14
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: bbbab071-81e8-49c6-a499-8787fd0d15b9
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 14
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9014930d-3c34-41c1-915c-3f1a8d72cf19
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 14
    column: 15
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f5d7b2d-cb92-4dc4-8dfa-62c0355aae52
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 14
    column: 15
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9ca58a93-5e8d-4e4d-b55b-69c01b1895bc
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 14
    column: 15
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 21ac26e3-26b2-4bec-9be7-abcb5e01a910
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 14
    column: 15
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2af0641b-78f8-454a-b3b1-6e00ba80b578
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 15
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5c31b9ba-a2b9-44db-bb58-8e773158d73d
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 15
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f844f4da-4f29-41fe-8a76-f4e7e7995787
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 15
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e45df08e-48b7-46dd-a90e-9871326f1303
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 15
    column: 15
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2a196d29-85a6-4eb1-addc-758c5409e47f
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 15
    column: 15
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1b85ea78-adb5-4e99-9439-d8c35eab2c80
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 15
    column: 15
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 60cbeaa7-714d-45ef-9a11-80cfae7c0073
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 15
    column: 15
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3f8d1971-6ded-4783-85ff-f8f3e5003a4b
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 15
    column: 15
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 009b7533-1087-4f9c-be4a-8cd1ac4e9a3a
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 15
    column: 20
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: df2c9478-bc7d-45e5-9ca3-209f2ab0f2ee
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 15
    column: 20
    function: main
  location_invariant:
    string: 4294967295LL - (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 51afc128-401f-450a-8a6d-52743b773e65
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 15
    column: 20
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1370f91c-fde2-40cb-825e-24b7f3586ad7
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 15
    column: 20
    function: main
  location_invariant:
    string: (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 83b12500-6ea4-446d-a0ca-db6543d891ec
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 15
    column: 20
    function: main
  location_invariant:
    string: (long long )y >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f8b7ea01-dd42-4a6c-92e4-e17fe792496d
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 15
    column: 20
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 29a9069d-e32c-4ffc-991e-1f017dfbe7af
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 18
    column: 4
    function: main
  location_invariant:
    string: 1U <= x
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c0532e1d-b23a-4a1f-9299-f37cf82996aa
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 18
    column: 4
    function: main
  location_invariant:
    string: -1LL + (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f87335d0-5c77-48bb-a979-f7cbcbfda5bb
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 18
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a5302ec8-e146-47fe-8b0e-639e0da1ca66
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 18
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9d644bf5-1e13-4a81-8a6d-9d60b0dc9c8e
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 18
    column: 4
    function: main
  location_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad87ec1c-c871-4884-8827-cf3491300222
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 18
    column: 4
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 139a9e93-6584-4788-bb87-4d8549cffc6b
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 18
    column: 4
    function: main
  location_invariant:
    string: x != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3c5fabe2-934d-412c-a41f-8d8ad46aa45d
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 19
    column: 4
    function: main
  location_invariant:
    string: x <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a11a3efc-7018-4e9a-9abb-9b7a6d5049a3
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 19
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f6d09a7-9ed2-4145-b8ac-2269523b21fa
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 19
    column: 4
    function: main
  location_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b61e3aa1-418e-4c5a-ac03-f5e25430ab1d
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 19
    column: 4
    function: main
  location_invariant:
    string: (-1LL + (long long )n) - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cc37f53f-6b19-4c0c-b1e7-9096a4ca2d41
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 19
    column: 4
    function: main
  location_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8758223-4cd9-49a9-aafe-77fd7f7721f4
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 19
    column: 4
    function: main
  location_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fadf7b18-bc22-4091-8b0d-45f8ea8a4390
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 19
    column: 4
    function: main
  location_invariant:
    string: x != 4294967295U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 5f8e9b64-fc84-4df7-897f-7b1dc93c50d4
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 23
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e5077b27-8c1c-462b-8c0c-70b55cfff0e0
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 23
    column: 8
    function: main
  loop_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c48104c6-e6ab-4921-9569-5d909425fc76
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 23
    column: 8
    function: main
  loop_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: afb78564-9d79-41d4-b7f2-669230607710
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )n >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6ca0c5ba-09d0-4d61-ae6b-662bd3e2b8dd
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: 4294967295LL - (long long )z >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c30e52dd-5094-45af-ba77-bef87a954d8e
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: (long long )n - (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6cfd5706-2d6e-4ebd-95a8-a774d2b64bc3
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: (long long )x >= 0LL
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: f6f2d98c-4909-4773-938f-111161a06e7a
    creation_time: 2023-01-27T16:29:39Z
    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/in-de20.c'''
    task:
      input_files:
      - ../plain/in-de20.c
      input_file_hashes:
        ../plain/in-de20.c: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: ../plain/in-de20.c
    file_hash: cfe6fce904e7772b92437e018e53dfef745de1dd85f6147cfc72edd062333cfd
    line: 16
    column: 8
    function: main
  loop_invariant:
    string: (long long )z >= 0LL
    type: assertion
    format: C
